Skip to content
Snippets Groups Projects
Select Git revision
  • 1bae23d83a84ad27da7e79d4257ac8bdd3d07e3c
  • master default
2 results

uml_test3.md

Blame
  • __main__.py 5.31 KiB
    #!/usr/bin/env python3
    import argparse
    
    from mc_openapi.app_config import app
    from mc_openapi.doml_mc import DOMLVersion
    from mc_openapi.doml_mc.domlr_parser.exceptions import RequirementException
    from mc_openapi.doml_mc.domlr_parser.parser import DOMLRTransformer, Parser, SynthesisDOMLRTransformer
    from mc_openapi.doml_mc.imc import RequirementStore
    from mc_openapi.doml_mc.intermediate_model.metamodel import MetaModelDocs
    from mc_openapi.doml_mc.mc import ModelChecker
    from mc_openapi.doml_mc.mc_result import MCResult
    
    parser = argparse.ArgumentParser()
    
    parser.add_argument("-d", "--doml", dest="doml", help="the DOMLX file to check")
    parser.add_argument("-V", "--doml-version", dest="doml_version", default="V2_0", help="(optional) the version used by the DOMLX file")
    parser.add_argument("-r", "--requirements", dest="requirements", help="the user-specified requirements file to check")
    parser.add_argument("-p", "--port", dest="port", type=int, default=8080, help="the port exposing the model checker REST API (default: 8080)")
    parser.add_argument("-v", "--verbose", dest="verbose", action='store_true', help="print a detailed human-readable output of everything going on. Helpful for debugging.")
    # Model Checker
    parser.add_argument("-c", "--check-consistency", dest="consistency", action='store_true', help="check on additional built-in consistency requirements")
    parser.add_argument("-S", "--skip-common-checks", dest="skip_common", action='store_true', help="skip check on common built-in requirements")
    parser.add_argument("-t", "--threads", dest="threads", type=int, default=2, help="number of threads used by the model checker")
    # Synthesis
    parser.add_argument("-s", "--synth", dest="synth", action='store_true', help="synthetize a new DOMLX file from requirements")
    parser.add_argument("-m", "--max-tries", dest="tries", type=int, default=10, help="max number of iteration while trying to solve the model with unbounded variables")
    
    args = parser.parse_args()
    
    # Print only when -v flag is true
    def printv(*_args):
        if args.verbose:
            print(*_args)
    
    printv("== Verbose: ON ==")
    
    if not args.doml and not args.synth:
        # Start the webserver
        app.run(port=args.port)
    else:
        # Run only it via command line
        doml_path = args.doml
        reqs_path = args.requirements
    
        # Try using the user-provided DOML version
        try:
            doml_ver = DOMLVersion[args.doml_version]
        except:
            # Suggest valid DOML versions
            print(f"Unknown DOML version '{args.doml_version}'")
            versions = [ ver.name for ver in list(DOMLVersion)]
            print(f"Available DOML versions = {versions}")
            exit(1)
    
        with open(doml_path, "rb") as xmif:
            # Read DOML file from path
            doml_xmi = xmif.read()
    
        # Config the model checker (setup metamodels and intermediate models)
        dmc = ModelChecker(doml_xmi, doml_ver)
    
        user_req_store = RequirementStore()
        user_req_str_consts = []
    
        if reqs_path:
            with open(reqs_path, "r") as reqsf:
            # Read the user requirements written in DSL
                user_reqs = reqsf.read()
            # Parse them
            try:
                domlr_parser = Parser(DOMLRTransformer)
                user_req_store, user_req_str_consts = domlr_parser.parse(user_reqs)
            except Exception as e:
                print(e)
                raise RuntimeError("Failed to parse the DOMLR.")
    
        if not args.synth:
            try:
                # Check satisfiability
                results = dmc.check_requirements(
                    threads=args.threads, 
                    user_requirements=user_req_store,
                    user_str_values=user_req_str_consts,
                    consistency_checks=args.consistency,
                    skip_common_requirements=args.skip_common
                )
    
                res, msg = results.summarize()
    
                if res == MCResult.sat:
                    print("sat")
                else:
                    print(res.name)
                    print("\033[91m{}\033[00m".format(msg))
            except RequirementException as e:
                print(e.message)
    
        else: # Synthesis
            printv("Running synthesis...")
            # Lazy load libraries
            from doml_synthesis.types import State
            from doml_synthesis.data import init_data
            from doml_synthesis.solver import solve
            from doml_synthesis.requirements import builtin_requirements
            from doml_synthesis.results import check_synth_results, save_results
    
            # Required files:
            mm = MetaModelDocs[doml_ver]
            im = {
                k: { 
                    'id': v.id_,
                    'name': v.user_friendly_name,
                    'class': v.class_,
                    'assocs': v.associations,
                    'attrs': v.attributes
                }
                for k, v in  dmc.intermediate_model.items()
            }
    
            # Parse
            synth_domlr_parser = Parser(SynthesisDOMLRTransformer)
            synth_user_reqs, user_reqs_strings = synth_domlr_parser.parse(user_reqs)
    
            print(user_reqs_strings)
            
            state = State()
            # Parse MM and IM
            state = init_data(state, doml=im, metamodel=mm)
            # Solve
    
            state = solve(
                state, 
                requirements=[builtin_requirements, synth_user_reqs], 
                strings=user_reqs_strings, 
                max_tries=args.tries
            )
            # Update state
            state = save_results(state)
            # Print output
            state = check_synth_results(state)