diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py index 96c0fd2ae84c0c2fd526ac0862ce502853278494..3ce069095a1d1f2cecafadd719dcc8868f5c5655 100644 --- a/mc_openapi/__main__.py +++ b/mc_openapi/__main__.py @@ -22,7 +22,7 @@ from mc_openapi.doml_mc.xmi_parser.doml_model import get_pyecore_model 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("-V", "--doml-version", dest="doml_version", 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.") @@ -52,14 +52,16 @@ else: 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) + doml_ver = None + if args.doml_version is not None: + 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 @@ -67,6 +69,7 @@ else: # Config the model checker (setup metamodels and intermediate models) dmc = ModelChecker(doml_xmi, doml_ver) + doml_ver = dmc.doml_version # Store of Requirements and unique string constants user_req_store = RequirementStore() @@ -99,7 +102,7 @@ else: exit(-1) if doml_ver == DOMLVersion.V2_2: - model = get_pyecore_model(doml_xmi, DOMLVersion.V2_2) + model = get_pyecore_model(doml_xmi, doml_ver) func_reqs = model.functionalRequirements.items for req in func_reqs: req_name: str = req.name diff --git a/mc_openapi/doml_mc/xmi_parser/doml_model.py b/mc_openapi/doml_mc/xmi_parser/doml_model.py index 288fb98d2e87dc3f0db114143e2e8cfa1b9c297e..0659bf67af5beadee8fe0fda9bb4cefc3cfeef1b 100644 --- a/mc_openapi/doml_mc/xmi_parser/doml_model.py +++ b/mc_openapi/doml_mc/xmi_parser/doml_model.py @@ -114,7 +114,7 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T def get_pyecore_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> EObject: if doml_version is None: doml_version = infer_domlx_version(raw_model) - + # TODO: See if its better replaced by the get_model() in parse_doml_version() return parse_xmi_model(raw_model, doml_version) from typing import Optional diff --git a/mc_openapi/handlers.py b/mc_openapi/handlers.py index a84048e70c3e3ad4fa16a9f5a4319349323257fc..99b3d8521ad36bf1ccef906f9b1d960a2f2c4d7f 100644 --- a/mc_openapi/handlers.py +++ b/mc_openapi/handlers.py @@ -1,4 +1,9 @@ import datetime +from mc_openapi.doml_mc.domlr_parser.parser import DOMLRTransformer, Parser +from mc_openapi.doml_mc.imc import RequirementStore + +from mc_openapi.doml_mc.intermediate_model.metamodel import DOMLVersion +from mc_openapi.doml_mc.xmi_parser.doml_model import get_pyecore_model from .doml_mc import ModelChecker, MCResult @@ -13,8 +18,30 @@ def make_error(user_msg, debug_msg=None): def post(body): doml_xmi = body try: + dmc = ModelChecker(doml_xmi) - results = dmc.check_requirements(threads=2, consistency_checks=False, timeout=50) + + user_req_store = None + user_req_str_consts = [] + + # Add support for Requirements in DOML + if dmc.doml_version == DOMLVersion.V2_2: + domlr_parser = Parser(DOMLRTransformer) + model = get_pyecore_model(doml_xmi, DOMLVersion.V2_2) + func_reqs = model.functionalRequirements.items + + user_req_store = RequirementStore() + + for req in func_reqs: + req_name: str = req.name + req_text: str = req.description + req_text = req_text.replace("```", "") + doml_req_store, doml_req_str_consts = domlr_parser.parse(req_text) + user_req_store += doml_req_store + user_req_str_consts += doml_req_str_consts + + + results = dmc.check_requirements(threads=2, user_requirements=user_req_store, user_str_values=user_req_str_consts, consistency_checks=False, timeout=50) res, msg = results.summarize() if res == MCResult.sat: diff --git a/tests/test_mc_openapi.py b/tests/test_mc_openapi.py index 7ab1ae0ab3942a552d0dc5d79f6c792c5f2608b8..506b33b37590ea0f4f0cbfff748747b41559d4c5 100644 --- a/tests/test_mc_openapi.py +++ b/tests/test_mc_openapi.py @@ -90,7 +90,7 @@ def test_post_faas_unsat_V2_2(): payload = r.json() assert r.status_code == requests.codes.ok assert payload["result"] is not None - assert payload["result"] == "sat" + assert payload["result"] == "unsat" def test_post_nginx_with_func_reqs_unsat_V2_2():