diff --git a/docs/requirements.rst b/docs/requirements.rst
index 0fb3c49c2298a4b3347a18c92c280bfd25f5e1a4..3af74b14d89b6c8c6c75f97c681fb009b3e84d2c 100644
--- a/docs/requirements.rst
+++ b/docs/requirements.rst
@@ -13,6 +13,8 @@ VM Network Interfaces
All virtual machines must be connected to at least one network interface.
+ID: ``vm_has_iface``
+
Virtual machines can communicate with other components of a deployment or with external clients
only through an appropriately configured network.
this check makes sure no virtual machines are isolated.
@@ -23,6 +25,8 @@ Concretization of Software Interfaces
All software packages can see the interfaces they need through a common network.
+ID: ``software_package_iface_net``
+
This check makes sure all exposed and consumed software interfaces at the application layer level
have been actually concretized through a network connection that allows the involved components
to communicate.
@@ -33,6 +37,8 @@ Duplicated Interfaces
There are no duplicated interfaces.
+ID: ``iface_uniq``
+
Checks whether two or more interfaces have been assigned the same IP address.
@@ -41,6 +47,8 @@ Deployed Software Components
All software components have been deployed to some node.
+ID: ``all_software_components_deployed``
+
Makes sure that all software components specified in the application layer have been
associated to at least one node in the abstract infrastructure layer
through the currently active deployment.
@@ -51,6 +59,8 @@ Concretization of Abstract Infrastructure
All abstract infrastructure elements are mapped to an element in the active concretization.
+ID: ``all_infrastructure_elements_deployed``
+
Makes sure all abstract infrastructure nodes are concretized by the currently active concretization layer.
@@ -59,6 +69,8 @@ Concrete Infrastructure Elements have a maps Association
All elements in the active concretization are mapped to some abstract infrastructure element.
+ID: ``all_concrete_map_something``
+
Makes sure each concrete infrastructure element is mapped to a node in the Abstract Infrastructure Layer.
Network Interfaces belong to a Security Group
@@ -66,6 +78,8 @@ Network Interfaces belong to a Security Group
All network interfaces belong to a security group.
+ID: ``security_group_must_have_iface``
+
Makes sure all network interfaces have been configured to belong to a security group.
This way, the user will be reminded to configure adequate rules for each network.
@@ -74,4 +88,6 @@ External Services are reached through HTTPS
All external SaaS can be reached only through a secure connection.
+ID: ``external_services_must_have_https``
+
Makes sure that an HTTPS rule is enforced for a Network Interface of a Software Component that interfaces with a SaaS.
\ No newline at end of file
diff --git a/docs/writing-requirements.rst b/docs/writing-requirements.rst
index 9d00a36e1f131b4f5262af2f8d3df0be80d87834..a9d87d7493bf4a0a9e21816be1decf89f10e390b 100644
--- a/docs/writing-requirements.rst
+++ b/docs/writing-requirements.rst
@@ -170,6 +170,17 @@ that the memory used by ``c1`` is less than the one used by ``c2`` (note that we
c1 has infrastructure.ComputingNode.memory_mb < c2 infrastructure.ComputingNode.memory_mb
+Flags
+=====
+You can alter the behaviour of the model checker through flags, which are simple parameters you can put at the beginnning of DOMLR.
+
+They are the following:
+ - ``%IGNORE <id of requirement>`` skips a specific built-in requirement.
+ - ``%IGNORE_BUILTIN`` skips all built-in requirements.
+ - ``%CHECK <id of requirement>`` enables an optional requirement.
+ - ``%CHECK_CONSISTENCY`` enables optional consistency checks.
+ - ``%CSP`` enables a Cloud Service Provider compatibility report, that is appended to the results.
+
Grammar
=======
See the `grammar.lark`_ file on GitHub, it's written in a EBNF-like form.
diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py
index e78350cb086387238235e481e662852a8a2d0250..4d7e3e897dd7ab7dd99fa3f5025f5a297228af98 100644
--- a/mc_openapi/__main__.py
+++ b/mc_openapi/__main__.py
@@ -2,25 +2,12 @@
import argparse
import logging
from logging.config import dictConfig
-import sys
-
-from doml_synthesis.data import init_data
-from doml_synthesis.requirements import builtin_requirements
-from doml_synthesis.results import check_synth_results, save_results
-from doml_synthesis.solver import solve
-from doml_synthesis.types import State
from mc_openapi.app_config import app
-from mc_openapi.doml_mc import DOMLVersion
-from mc_openapi.doml_mc.csp_compatibility._iec_check import check_csp_compatibility
+from mc_openapi.doml_mc import DOMLVersion, init_model, verify_csp_compatibility, verify_model, synthesize_model
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
-from mc_openapi.doml_mc.xmi_parser.doml_model import get_pyecore_model
+
from . import __version__
parser = argparse.ArgumentParser()
@@ -32,7 +19,7 @@ parser.add_argument("-p", "--port", dest="port", type=int, default=8080, help="t
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("-S", "--skip-builtin-checks", dest="skip_builtin", action='store_true', help="skip check on built-in requirements")
parser.add_argument("-C", "--csp", dest="csp", action='store_true', help="check compatibility with supported CSPs")
parser.add_argument("-t", "--threads", dest="threads", type=int, default=2, help="number of threads used by the model checker")
@@ -42,13 +29,6 @@ parser.add_argument("-m", "--max-tries", dest="tries", type=int, default=8, help
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:
dictConfig({
'version': 1,
@@ -73,11 +53,10 @@ else:
logging.basicConfig(level=logging.DEBUG, format='* %(message)s')
logging.info(f"DOML Model Checker v{__version__}")
- # Run only it via command line
doml_path = args.doml
- reqs_path = args.requirements
+ domlr_path = args.requirements
- # Try using the user-provided DOML version
+ # Validate user-provided DOML version
doml_ver = None
if args.doml_version is not None:
try:
@@ -89,145 +68,41 @@ else:
print(f"Available DOML versions = {versions}")
exit(1)
+ # Read DOMLX from path
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)
- doml_ver = dmc.doml_version
-
- # Check CSP Compatibility
- if args.csp:
- from mc_openapi.doml_mc.csp_compatibility import CSPCompatibilityValidator as csp_comp
- csp_comp.check(dmc.intermediate_model, doml_ver)
- # check_csp_compatibility(dmc.intermediate_model, doml_ver)
- exit(0)
-
- # Store of Requirements and unique string constants
- user_req_store = RequirementStore()
- user_req_str_consts = []
-
- synth_user_reqs = []
- synth_user_reqs_strings = []
-
- try:
- domlr_parser = Parser(DOMLRTransformer)
- if args.synth:
- synth_domlr_parser = Parser(SynthesisDOMLRTransformer)
- except Exception as e:
- print(e, file=sys.stderr)
- print("Failed to setup DOMLR Parser")
- exit(-1)
-
- user_reqs = None
-
- if reqs_path:
- with open(reqs_path, "r") as reqsf:
+ # Read DOMLR from path
+ domlr_src = None
+ if domlr_path:
+ with open(domlr_path, "r") as domlr_file:
# Read the user requirements written in DSL
- user_reqs = reqsf.read()
- # Parse them
- try:
- user_req_store, user_req_str_consts = domlr_parser.parse(user_reqs)
- except Exception as e:
- print(e, file=sys.stderr)
- print("Failed to parse the DOMLR.", file=sys.stderr)
- exit(-1)
-
- if DOMLVersion.has_DOMLR_support(doml_ver):
- model = get_pyecore_model(doml_xmi, doml_ver)
- func_reqs = model.functionalRequirements.items
- 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
-
- if args.synth:
- synth_doml_req_store, synth_doml_req_str_consts = synth_domlr_parser.parse(req_text, for_synthesis=True)
- synth_user_reqs.append(synth_doml_req_store)
- synth_user_reqs_strings += synth_doml_req_str_consts
-
- # Remove possible duplicates
- user_req_str_consts = list(set(user_req_str_consts))
-
- 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
- )
+ domlr_src = domlr_file.read()
- res, msg = results.summarize()
+ # Config the model checker
+ dmc = init_model(doml_xmi, doml_ver)
+
+ ####### END OF INIT STEP #######
+ if not args.synth: # Verify Model/CSP Compatibility
+
+ # Check CSP Compatibility
+ if args.csp:
+ verify_csp_compatibility(dmc)
+ # TODO: Do something with the results
+ else:
+ result, msg = verify_model(dmc, domlr_src, args.threads, args.consistency, args.skip_builtin)
print("[RESULT]")
- if res == MCResult.sat:
+ if result == MCResult.sat:
print("sat")
else:
- print(res.name)
+ print(result.name)
print("[ERRORS]")
print("\033[91m{}\033[00m".format(msg))
- except RequirementException as e:
- print(e.message)
- else: # Synthesis
- printv("Running synthesis...")
-
-
- # 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()
- }
- if user_reqs:
- try:
- ext_domlr_reqs, ext_domlr_reqs_strings = synth_domlr_parser.parse(user_reqs, for_synthesis=True)
- synth_user_reqs.append(ext_domlr_reqs)
- synth_user_reqs_strings += ext_domlr_reqs_strings
- except Exception as e:
- print(e, file=sys.stderr)
- print("Failed to parse the DOMLR.", file=sys.stderr)
- exit(-1)
-
-
- # Remove duplicated strings
- print(synth_user_reqs_strings)
- synth_user_reqs_strings = list(set(synth_user_reqs_strings))
-
- state = State()
- # Parse MM and IM
- state = init_data(
- state,
- doml=im,
- metamodel=mm,
- )
-
- reqs = synth_user_reqs
- if not args.skip_common:
- reqs.append(builtin_requirements)
-
- state = solve(
- state,
- requirements=reqs,
- strings=synth_user_reqs_strings,
- max_tries=args.tries
- )
- # Update state
- state = save_results(state)
- # Print output
- state = check_synth_results(state)
\ No newline at end of file
+ else: # Synthesis
+ synthesize_model(dmc, domlr_src, args.tries)
+ # TODO: Do something with the results
+
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/__init__.py b/mc_openapi/doml_mc/__init__.py
index 6eab5f4c22d7f8486a9ab4dc69b81ba0067aeb7a..62db218186b30bcc40496d93a14a162c71df83dc 100644
--- a/mc_openapi/doml_mc/__init__.py
+++ b/mc_openapi/doml_mc/__init__.py
@@ -3,6 +3,7 @@ from .mc_result import MCResult, MCResults # noqa: F401
from .intermediate_model.metamodel import DOMLVersion, init_metamodels # noqa: F401
from .xmi_parser.doml_model import init_doml_rsets
from .xmi_parser.special_parsers import init_special_parsers
+from .main import init_model, verify_csp_compatibility, verify_model, synthesize_model
__all__ = ["ModelChecker", "MCResult", "MCResults", "DOMLVersion"]
diff --git a/mc_openapi/doml_mc/common_reqs.py b/mc_openapi/doml_mc/common_reqs.py
index 033111e9688c3d678f64439412aec2f0d9831439..4d1dabba0bd16996c5c76e1ee3cddcfd615aeb1a 100644
--- a/mc_openapi/doml_mc/common_reqs.py
+++ b/mc_openapi/doml_mc/common_reqs.py
@@ -1,7 +1,4 @@
-from re import M
-from typing import Optional
-
-from z3 import And, Const, Consts, Exists, ExprRef, ModelRef, Not, Or, Solver, ForAll
+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver
from .error_desc_helper import get_user_friendly_name
from .imc import Requirement, RequirementStore, SMTEncoding, SMTSorts
@@ -14,7 +11,7 @@ def get_consts(smtsorts: SMTSorts, consts: list[str]) -> list[ExprRef]:
# Assertions
-def vm_iface(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+def vm_has_iface(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
vm, iface = get_consts(smtsorts, ["vm", "iface"])
return And(
smtenc.element_class_fun(
@@ -557,7 +554,7 @@ def iface_uniq(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
# All software components have been deployed to some node.
-def all_SoftwareComponents_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+def all_software_components_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
sc, deployment, ielem = get_consts(smtsorts, ["sc", "deployment", "ielem"])
return And(
smtenc.element_class_fun(
@@ -836,14 +833,14 @@ def ed_external_services_must_have_https(solver: Solver, smtsorts: SMTSorts, int
return "A Security Group doesn't have a rule to access an external service (SaaS) through HTTPS (port 443)."
-RequirementLists = {
+REQUIREMENTS = {
DOMLVersion.V2_0: [
- (vm_iface, "vm_iface",
+ (vm_has_iface, "vm_has_iface",
"All virtual machines must be connected to at least one network interface.", ed_vm_iface),
(software_package_iface_net, "software_package_iface_net",
"All software packages can see the interfaces they need through a common network.", ed_software_package_iface_net),
(iface_uniq, "iface_uniq", "There are no duplicated interfaces.", ed_iface_uniq),
- (all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed",
+ (all_software_components_deployed, "all_software_components_deployed",
"All software components have been deployed to some node.", ed_all_SoftwareComponents_deployed),
(all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed",
"All abstract infrastructure elements are mapped to an element in the active concretization.", ed_all_infrastructure_elements_deployed),
@@ -855,12 +852,12 @@ RequirementLists = {
# (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
],
DOMLVersion.V2_1: [
- (vm_iface, "vm_iface",
+ (vm_has_iface, "vm_has_iface",
"All virtual machines must be connected to at least one network interface.", ed_vm_iface),
(software_package_iface_net_v2_1, "software_package_iface_net",
"All software packages can see the interfaces they need through a common network.", ed_software_package_iface_net),
(iface_uniq, "iface_uniq", "There are no duplicated interfaces.", ed_iface_uniq),
- (all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed",
+ (all_software_components_deployed, "all_software_components_deployed",
"All software components have been deployed to some node.", ed_all_SoftwareComponents_deployed),
(all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed",
"All abstract infrastructure elements are mapped to an element in the active concretization.", ed_all_infrastructure_elements_deployed),
@@ -872,12 +869,12 @@ RequirementLists = {
# (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
],
DOMLVersion.V2_2: [
- (vm_iface, "vm_iface",
+ (vm_has_iface, "vm_has_iface",
"All virtual machines must be connected to at least one network interface.", ed_vm_iface),
(software_package_iface_net_v2_1, "software_package_iface_net",
"All software packages can see the interfaces they need through a common network.", ed_software_package_iface_net),
(iface_uniq, "iface_uniq", "There are no duplicated interfaces.", ed_iface_uniq),
- (all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed",
+ (all_software_components_deployed, "all_software_components_deployed",
"All software components have been deployed to some node.", ed_all_SoftwareComponents_deployed),
(all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed",
"All abstract infrastructure elements are mapped to an element in the active concretization.", ed_all_infrastructure_elements_deployed),
@@ -889,12 +886,12 @@ RequirementLists = {
# (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
],
DOMLVersion.V2_2_1: [
- (vm_iface, "vm_iface",
+ (vm_has_iface, "vm_has_iface",
"All virtual machines must be connected to at least one network interface.", ed_vm_iface),
(software_package_iface_net_v2_1, "software_package_iface_net",
"All software packages can see the interfaces they need through a common network.", ed_software_package_iface_net),
(iface_uniq, "iface_uniq", "There are no duplicated interfaces.", ed_iface_uniq),
- (all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed",
+ (all_software_components_deployed, "all_software_components_deployed",
"All software components have been deployed to some node.", ed_all_SoftwareComponents_deployed),
(all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed",
"All abstract infrastructure elements are mapped to an element in the active concretization.", ed_all_infrastructure_elements_deployed),
@@ -906,12 +903,12 @@ RequirementLists = {
# (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
],
DOMLVersion.V2_3: [
- (vm_iface_v2_3, "vm_iface",
+ (vm_iface_v2_3, "vm_has_iface",
"All virtual machines must be connected to at least one network interface.", ed_vm_iface),
(software_package_iface_net_v2_3, "software_package_iface_net",
"All software packages can see the interfaces they need through a common network.", ed_software_package_iface_net),
(iface_uniq, "iface_uniq", "There are no duplicated interfaces.", ed_iface_uniq),
- (all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed",
+ (all_software_components_deployed, "all_software_components_deployed",
"All software components have been deployed to some node.", ed_all_SoftwareComponents_deployed),
(all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed",
"All abstract infrastructure elements are mapped to an element in the active concretization.", ed_all_infrastructure_elements_deployed),
@@ -931,5 +928,5 @@ CommonRequirements = {ver: RequirementStore(
*rt[:-1], error_description=("BUILTIN", rt[-1]), flipped=True
) for rt in reqs
])
- for ver, reqs in RequirementLists.items()
+ for ver, reqs in REQUIREMENTS.items()
}
diff --git a/mc_openapi/doml_mc/consistency_reqs.py b/mc_openapi/doml_mc/consistency_reqs.py
index a562c2ff08cf41a137a4228e1b654419c15c61de..64d98422848ddfc2821852a44085dda75280a090 100644
--- a/mc_openapi/doml_mc/consistency_reqs.py
+++ b/mc_openapi/doml_mc/consistency_reqs.py
@@ -19,7 +19,7 @@ def subclass_cond(smtenc: SMTEncoding, subclasses: set[str], elem: ExprRef) -> E
)
)
-
+# TODO: CHECK WHAT IS WRONG ELSE SKIP IT
def get_attribute_type_reqs(mm: MetaModel) -> RequirementStore:
subclasses_dict = get_subclasses_dict(mm)
# A type validity constraint is added for every attribute:
diff --git a/mc_openapi/doml_mc/domlr_parser/__init__.py b/mc_openapi/doml_mc/domlr_parser/__init__.py
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..7e7d69b9817656cb7984292858fb371e41694891 100644
--- a/mc_openapi/doml_mc/domlr_parser/__init__.py
+++ b/mc_openapi/doml_mc/domlr_parser/__init__.py
@@ -0,0 +1,3 @@
+from .transformer import DOMLRTransformer
+from .synthesis_transformer import SynthesisDOMLRTransformer
+from .parser import Parser
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/domlr_parser/grammar.lark b/mc_openapi/doml_mc/domlr_parser/grammar.lark
index 1e7709a7978063f96999cf99cd7fbe020bfae8a0..896cf3a64f41f0743b44246c05acdbd7393e07b9 100644
--- a/mc_openapi/doml_mc/domlr_parser/grammar.lark
+++ b/mc_openapi/doml_mc/domlr_parser/grammar.lark
@@ -1,3 +1,13 @@
+start : (flags)? (requirements)?
+
+flags : flag (flag)*
+
+flag : "%IGNORE" CONST -> flag_requirement_ignore
+ | "%IGNORE_BUILTIN" -> flag_requirement_ignore_builtin
+ | "%CHECK" CONST -> flag_requirement_check
+ | "%CHECK_CONSISTENCY" -> flag_requirement_check_consistency
+ | "%CSP" -> flag_csp
+
requirements : requirement (requirement)*
requirement : FLIP_EXPR req_name expression "error:" error_desc
diff --git a/mc_openapi/doml_mc/domlr_parser/parser.ipynb b/mc_openapi/doml_mc/domlr_parser/parser.ipynb
deleted file mode 100644
index 2343825b84444eadb1b9a0902abed80dd57f1a64..0000000000000000000000000000000000000000
--- a/mc_openapi/doml_mc/domlr_parser/parser.ipynb
+++ /dev/null
@@ -1,350 +0,0 @@
-{
- "cells": [
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "# Parser Prototype"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 1,
- "metadata": {},
- "outputs": [],
- "source": [
- "from lark import Lark\n",
- "\n",
- "with open(\"grammar.lark\") as grammar_file:\n",
- " grammar = grammar_file.read()"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 2,
- "metadata": {},
- "outputs": [],
- "source": [
- "# vm, iface = get_consts(smtsorts, [\"vm\", \"iface\"])\n",
- "# return And(\n",
- "# smtenc.element_class_fun(vm) == smtenc.classes[\"abstract_VirtualMachine\"],\n",
- "# Not(\n",
- "# Exists(\n",
- "# [iface],\n",
- "# ENCODINGS.association_rel(vm, smtenc.associations[\"abstract_ComputingNode::ifaces\"], iface)\n",
- "# )\n",
- "# )\n",
- "# )\n",
- "\n",
- "expr_to_parse = r\"\"\"\n",
- "+ \"example requirement to test\"\n",
- " # Expr to parse\n",
- " not vm is class abstract.VirtualMachine\n",
- " and\n",
- " vm is not class abstract.Storage\n",
- " iff\n",
- " not exists iface, apple (\n",
- " (vm has abstract.ComputingNode.ifaces iface)\n",
- " or\n",
- " (vm has abstract.ComputingNode.os Os1)\n",
- " and\n",
- " (vm has abstract.ComputingNode.memory_mb 1024)\n",
- " and\n",
- " (vm has abstract.ComputingNode.architecture \"linux\")\n",
- " and\n",
- " (vm has application.SoftwareComponent.isPersistent !True)\n",
- " )\n",
- " ---\n",
- " \"Virtual Machine {vm} has no iface\"\n",
- "\n",
- "+ \"example requirement to test\"\n",
- " # Expr to parse\n",
- " not vm is class abstract.VirtualMachine\n",
- " and\n",
- " vm is not class abstract.Storage\n",
- " iff\n",
- " not exists iface, apple (\n",
- " (vm has abstract.ComputingNode.ifaces iface)\n",
- " or\n",
- " (vm has abstract.ComputingNode.os Os1)\n",
- " and\n",
- " (\n",
- " vm has abstract.ComputingNode.memory_mb Mem\n",
- " and\n",
- " Mem > 256\n",
- " )\n",
- " )\n",
- " ---\n",
- " \"Virtual Machine {vm} has no iface\"\n",
- "\"\"\""
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 3,
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "requirements\n",
- " requirement\n",
- " +\n",
- " req_name\t\"example requirement to test\"\n",
- " iff_expr\n",
- " and_expr\n",
- " negation\n",
- " equality\n",
- " const_or_class\tvm\n",
- " const_or_class\tabstract.VirtualMachine\n",
- " inequality\n",
- " const_or_class\tvm\n",
- " const_or_class\tabstract.Storage\n",
- " negation\n",
- " exists\n",
- " bound_consts\n",
- " iface\n",
- " apple\n",
- " and_expr\n",
- " or_expr\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.ifaces\n",
- " iface\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.os\n",
- " value\tOs1\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.memory_mb\n",
- " value\t1024\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.architecture\n",
- " value\t\"linux\"\n",
- " relationship_expr\n",
- " vm\n",
- " application.SoftwareComponent.isPersistent\n",
- " value\t!True\n",
- " ---\n",
- " error_desc\t\"Virtual Machine {vm} has no iface\"\n",
- " requirement\n",
- " +\n",
- " req_name\t\"example requirement to test\"\n",
- " iff_expr\n",
- " and_expr\n",
- " negation\n",
- " equality\n",
- " const_or_class\tvm\n",
- " const_or_class\tabstract.VirtualMachine\n",
- " inequality\n",
- " const_or_class\tvm\n",
- " const_or_class\tabstract.Storage\n",
- " negation\n",
- " exists\n",
- " bound_consts\n",
- " iface\n",
- " apple\n",
- " and_expr\n",
- " or_expr\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.ifaces\n",
- " iface\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.os\n",
- " value\tOs1\n",
- " and_expr\n",
- " relationship_expr\n",
- " vm\n",
- " abstract.ComputingNode.memory_mb\n",
- " value\tMem\n",
- " comparison\n",
- " value\tMem\n",
- " >\n",
- " value\t256\n",
- " ---\n",
- " error_desc\t\"Virtual Machine {vm} has no iface\"\n",
- "\n"
- ]
- }
- ],
- "source": [
- "parser = Lark(grammar, start=\"requirements\")\n",
- "tree = parser.parse(expr_to_parse)\n",
- "\n",
- "print(tree.pretty())"
- ]
- },
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": []
- },
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "We need the `ModelChecker` to import `SMTEncodings` and `SMTSorts` in order to create our Z3 constants programmatically.\n",
- "\n",
- "Now the model checker should expose the *intermediate model checker* which should provide us with those two collections."
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 4,
- "metadata": {},
- "outputs": [],
- "source": [
- "from mc_openapi.doml_mc import ModelChecker, DOMLVersion\n",
- "from mc_openapi.doml_mc.imc import IntermediateModelChecker\n",
- "\n",
- "# Import DOMLX as bytes\n",
- "doml_document_path = \"../../../tests/doml/faas.domlx\"\n",
- "with open(doml_document_path, \"rb\") as xmif:\n",
- " doml_xmi = xmif.read()\n",
- "\n",
- "model_checker = ModelChecker(doml_xmi, DOMLVersion.V2_0)\n",
- "\n",
- "intermediate_model_checker = IntermediateModelChecker(\n",
- " model_checker.metamodel,\n",
- " model_checker.inv_assoc,\n",
- " model_checker.intermediate_model\n",
- ")"
- ]
- },
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "The parser will now produce a Z3 expression to evaluate."
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 5,
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "[Requirement(assert_callable=<function DSLTransformer.iff_expr.<locals>.<lambda> at 0x7fe654129900>,\n",
- " assert_name='example_requirement_to_test',\n",
- " description='example requirement to test',\n",
- " error_description=<function DSLTransformer.requirement.<locals>.<lambda> at 0x7fe6541295a0>,\n",
- " flipped=False),\n",
- " Requirement(assert_callable=<function DSLTransformer.iff_expr.<locals>.<lambda> at 0x7fe65412ad40>,\n",
- " assert_name='example_requirement_to_test',\n",
- " description='example requirement to test',\n",
- " error_description=<function DSLTransformer.requirement.<locals>.<lambda> at 0x7fe65412aef0>,\n",
- " flipped=False)]\n"
- ]
- }
- ],
- "source": [
- "from pprint import pprint\n",
- "from z3 import Not, And, Or, Xor, Implies, Exists, ForAll\n",
- "\n",
- "from mc_openapi.doml_mc.dsl_parser.parser import Parser\n",
- "\n",
- "parser = Parser(grammar)\n",
- "\n",
- "reqs_store, user_value_strings = parser.parse(expr_to_parse)\n",
- "\n",
- "pprint(reqs_store.get_all_requirements())"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 6,
- "metadata": {},
- "outputs": [],
- "source": [
- "intermediate_model_checker.instantiate_solver(user_value_strings)\n",
- "ENCODINGS = intermediate_model_checker.smt_encoding\n",
- "SORTS = intermediate_model_checker.smt_sorts\n",
- "\n",
- "assert ENCODINGS and SORTS"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 7,
- "metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "And(Not(elem_class(vm) == infrastructure_VirtualMachine),\n",
- " elem_class(vm) != infrastructure_Storage) ==\n",
- "Not(Exists([iface, apple],\n",
- " And(Or(association(vm,\n",
- " infrastructure_ComputingNode::ifaces,\n",
- " iface),\n",
- " attribute(vm,\n",
- " infrastructure_ComputingNode::os,\n",
- " Os1)),\n",
- " attribute(vm,\n",
- " infrastructure_ComputingNode::memory_mb,\n",
- " int(1024)),\n",
- " attribute(vm,\n",
- " infrastructure_ComputingNode::architecture,\n",
- " str(ss_50__linux_)),\n",
- " attribute(vm,\n",
- " application_SoftwareComponent::isPersistent,\n",
- " bool(True)))))\n",
- "And(Not(elem_class(vm) == infrastructure_VirtualMachine),\n",
- " elem_class(vm) != infrastructure_Storage) ==\n",
- "Not(Exists([iface, apple],\n",
- " And(Or(association(vm,\n",
- " infrastructure_ComputingNode::ifaces,\n",
- " iface),\n",
- " attribute(vm,\n",
- " infrastructure_ComputingNode::os,\n",
- " Os1)),\n",
- " And(attribute(vm,\n",
- " infrastructure_ComputingNode::memory_mb,\n",
- " Mem),\n",
- " get_int(Mem) > get_int(int(256))))))\n"
- ]
- }
- ],
- "source": [
- "for req in reqs_store.get_all_requirements():\n",
- " print(req.assert_callable(ENCODINGS, SORTS))"
- ]
- }
- ],
- "metadata": {
- "kernelspec": {
- "display_name": "Python 3.10.7 ('.venv': poetry)",
- "language": "python",
- "name": "python3"
- },
- "language_info": {
- "codemirror_mode": {
- "name": "ipython",
- "version": 3
- },
- "file_extension": ".py",
- "mimetype": "text/x-python",
- "name": "python",
- "nbconvert_exporter": "python",
- "pygments_lexer": "ipython3",
- "version": "3.10.7"
- },
- "orig_nbformat": 4,
- "vscode": {
- "interpreter": {
- "hash": "d98256633358fe1daa4009223d54520a3e2548801398a173545d5698bb289e16"
- }
- }
- },
- "nbformat": 4,
- "nbformat_minor": 2
-}
diff --git a/mc_openapi/doml_mc/domlr_parser/parser.py b/mc_openapi/doml_mc/domlr_parser/parser.py
index 24036f181455600a28484e22fdba8611d0f1e0f8..2a2ab5e6db3e9d6535238fd8beb5302b96870f20 100644
--- a/mc_openapi/doml_mc/domlr_parser/parser.py
+++ b/mc_openapi/doml_mc/domlr_parser/parser.py
@@ -1,24 +1,17 @@
-import logging
import os
-import re
-from typing import Callable, Literal
import yaml
-from lark import Lark, Transformer, UnexpectedCharacters, UnexpectedEOF
-from mc_openapi.doml_mc.domlr_parser.exceptions import RequirementBadSyntaxException
-from mc_openapi.doml_mc.domlr_parser.utils import (RefHandler, StringValuesCache, SynthesisRefHandler,
- VarStore)
-from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
-from mc_openapi.doml_mc.imc import (Requirement, RequirementStore, SMTEncoding,
- SMTSorts)
-from mc_openapi.doml_mc.intermediate_model import IntermediateModel
-from z3 import And, Exists, ExprRef, ForAll, Implies, Not, Or, Solver, Xor, simplify
from doml_synthesis import State
+from lark import Lark, UnexpectedCharacters, UnexpectedEOF
+from z3 import Not
+from mc_openapi.doml_mc.domlr_parser.exceptions import \
+ RequirementBadSyntaxException
+from mc_openapi.doml_mc.domlr_parser.utils import StringValuesCache, VarStore
+from mc_openapi.doml_mc.imc import RequirementStore
class ParserData:
def __init__(self) -> None:
- # TODO: Replace with files api?
grammar_path = os.path.join(os.path.dirname(__file__), "grammar.lark")
exceptions_path = os.path.join(
os.path.dirname(__file__), "exceptions.yaml")
@@ -33,14 +26,15 @@ PARSER_DATA = ParserData()
class Parser:
def __init__(self, transformer, grammar: str = PARSER_DATA.grammar):
- self.parser = Lark(grammar, start="requirements", parser="lalr")
+ self.parser = Lark(grammar, start="start", parser="lalr")
self.transformer = transformer
- def parse(self, input: str, for_synthesis: bool = False):
+ def parse(self, input: str, for_synthesis: bool = False) -> tuple[RequirementStore, list[str], dict[str, bool]]:
"""Parse the input string containing the DOMLR requirements and
returns a tuple with:
- RequirementStore with the parsed requirements inside
- A list of strings to be added to the string constant EnumSort
+ - A dictionary of all the flags
"""
try:
self.tree = self.parser.parse(input)
@@ -51,9 +45,11 @@ class Parser:
transformer = self.transformer(const_store, user_values_cache)
if not for_synthesis:
+ reqs, flags = transformer.transform(self.tree)
return (
- RequirementStore(transformer.transform(self.tree)),
- user_values_cache.get_list()
+ RequirementStore(reqs),
+ user_values_cache.get_list(),
+ flags
)
else:
reqs = transformer.transform(self.tree)
@@ -70,547 +66,13 @@ class Parser:
except UnexpectedEOF as e:
msg = "Unexpected End of File:\n"
- msg += "Did you forget the `error:` message at the end of a requirement?"
+ msg += "Did you forget the `error:` keyword at the end of a requirement?"
raise Exception(msg)
except UnexpectedCharacters as e:
msg = _get_error_desc_for_unexpected_characters(e, input)
raise RequirementBadSyntaxException(e.line, e.column, msg)
-
-class DOMLRTransformer(Transformer):
- # These callbacks will be called when a rule with the same name
- # is matched. It starts from the leaves.
- def __init__(self,
- const_store: VarStore,
- user_values_cache: StringValuesCache,
- visit_tokens: bool = True
- ) -> None:
- super().__init__(visit_tokens)
- self.const_store = const_store
- self.user_values_cache = user_values_cache
-
- def __default__(self, data, children, meta):
- return children
-
- # start
- def requirements(self, args) -> list[Requirement]:
- return args
-
- def requirement(self, args) -> Requirement:
- flip_expr: bool = args[0].value == "-"
- name: str = args[1]
- expr: Callable[[SMTEncoding, SMTSorts], ExprRef] = args[2]
- errd: tuple[Literal["USER", "BUILTIN"], Callable[[Solver, SMTSorts,
- IntermediateModel, int], str]] = args[3]
- index = self.const_store.get_index_and_push()
- return Requirement(
- expr,
- name.lower().replace(" ", "_"),
- name,
- (errd[0], lambda solver, sorts, model: errd[1](
- solver, sorts, model,
- index,
- name
- )),
- flipped=flip_expr
- )
-
- def req_name(self, args) -> str:
- return str(args[0].value.replace('"', ''))
-
- # Requirement requirement expression
-
- def bound_consts(self, args):
- const_names = list(map(lambda arg: arg.value, args))
- for name in const_names:
- self.const_store.use(name)
- self.const_store.quantify(name)
- return lambda _, sorts: RefHandler.get_consts(const_names, sorts)
-
- def negation(self, args):
- return lambda enc, sorts: Not(args[0](enc, sorts))
-
- def iff_expr(self, args):
- return lambda enc, sorts: args[0](enc, sorts) == args[1](enc, sorts)
-
- def implies_expr(self, args):
- return lambda enc, sorts: Implies(args[0](enc, sorts), args[1](enc, sorts))
-
- def and_expr(self, args):
- return lambda enc, sorts: And([arg(enc, sorts) for arg in args])
-
- def or_expr(self, args):
- return lambda enc, sorts: Or([arg(enc, sorts) for arg in args])
-
- def exists(self, args):
- return lambda enc, sorts: Exists(args[0](enc, sorts), args[1](enc, sorts))
-
- def forall(self, args):
- return lambda enc, sorts: ForAll(args[0](enc, sorts), args[1](enc, sorts))
-
- def rel_assoc_expr(self, args):
- """An ASSOCIATION relationship"""
- rel_name = args[1].value
- self.const_store.use(args[0].value)
- self.const_store.use(args[2].value)
-
- def _gen_rel_elem_expr(enc: SMTEncoding, sorts: SMTSorts):
- rel, rel_type = RefHandler.get_relationship(enc, rel_name)
-
- assert rel_type == RefHandler.ASSOCIATION
-
- return RefHandler.get_association_rel(
- enc,
- RefHandler.get_const(args[0].value, sorts),
- rel,
- RefHandler.get_const(args[2].value, sorts)
- )
- return _gen_rel_elem_expr
-
- def rel_attr_value_expr(self, args):
- """An ATTRIBUTE relationship with a rhs that is a value"""
-
- rel_name = args[1].value
-
- def _gen_rel_attr_value_expr(enc: SMTEncoding, sorts: SMTSorts):
- elem = RefHandler.get_const(args[0].value, sorts)
- rel, rel_type = RefHandler.get_relationship(enc, rel_name)
- assert rel_type == RefHandler.ATTRIBUTE
-
- rhs_value, rhs_value_type = args[3]
- rhs_value = rhs_value(enc, sorts)
- op = args[2].value
-
- if rhs_value_type == RefHandler.INTEGER:
-
- lhs_value = RefHandler.get_value("x", sorts)
-
- return And(
- RefHandler.get_attribute_rel(enc,
- elem,
- rel,
- lhs_value
- ),
- self.compare_int(sorts, op, lhs_value, rhs_value)
- )
- elif rhs_value_type == RefHandler.STRING or rhs_value_type == RefHandler.BOOLEAN:
- expr = RefHandler.get_attribute_rel(enc,
- elem,
- rel,
- rhs_value
- )
- if op == "==":
- return expr
- elif op == "!=":
- return Not(expr)
- else:
- raise f'Invalid compare operator "{op}". It must be "==" or "!=".'
-
- return _gen_rel_attr_value_expr
-
- def rel_attr_elem_expr(self, args):
- """An ATTRIBUTE relationship with a rhs that is another element"""
-
- rel1_name = args[1].value
- rel2_name = args[4].value
- op = args[2].value
-
- def _gen_rel_attr_elem_expr(enc: SMTEncoding, sorts: SMTSorts):
- elem1 = RefHandler.get_const(args[0].value, sorts)
- elem2 = RefHandler.get_const(args[3].value, sorts)
- rel1, rel1_type = RefHandler.get_relationship(enc, rel1_name)
- rel2, rel2_type = RefHandler.get_relationship(enc, rel2_name)
-
- assert rel1_type == RefHandler.ATTRIBUTE
- assert rel2_type == RefHandler.ATTRIBUTE
-
- rhs_value = RefHandler.get_value("x", sorts)
-
- expr = And(
- RefHandler.get_attribute_rel(enc,
- elem1,
- rel1,
- rhs_value
- ),
- RefHandler.get_attribute_rel(enc,
- elem2,
- rel2,
- rhs_value
- )
- )
- if op == "==":
- return expr
- elif op == "!=":
- return Not(expr)
- else:
- rhs1_value = RefHandler.get_value("rhs1", sorts)
- rhs2_value = RefHandler.get_value("rhs2", sorts)
- expr = And(
- RefHandler.get_attribute_rel(enc,
- elem1,
- rel1,
- rhs1_value
- ),
- RefHandler.get_attribute_rel(enc,
- elem2,
- rel2,
- rhs2_value
- ),
- self.compare_int(sorts, op, rhs1_value, rhs2_value)
- )
- logging.warning(
- "Warning: Comparing attributes of two elements with {op} is experimental!\n",
- "Assumption: the attribute is an Integer."
- )
- return expr
-
- return _gen_rel_attr_elem_expr
-
- def _get_equality_sides(self, arg1, arg2):
- # We track use of const in const_or_class
- if arg1.type == "CONST" and arg2.type == "CONST":
- return (
- lambda _, sorts: RefHandler.get_const(arg1.value, sorts),
- lambda _, sorts: RefHandler.get_const(arg2.value, sorts)
- )
-
- if arg1.type == "CLASS":
- def arg1_ret(enc, _): return RefHandler.get_class(enc, arg1.value)
- else:
- def arg1_ret(enc, sorts): return RefHandler.get_element_class(
- enc, RefHandler.get_const(arg1.value, sorts))
-
- if arg2.type == "CLASS":
- def arg2_ret(enc, _): return RefHandler.get_class(enc, arg2.value)
- else:
- def arg2_ret(enc, sorts): return RefHandler.get_element_class(
- enc, RefHandler.get_const(arg2.value, sorts))
-
- return (arg1_ret, arg2_ret)
-
- def equality(self, args):
- a, b = self._get_equality_sides(args[0], args[1])
- return lambda enc, sorts: a(enc, sorts) == b(enc, sorts)
-
- def inequality(self, args):
- a, b = self._get_equality_sides(args[0], args[1])
- return lambda enc, sorts: a(enc, sorts) != b(enc, sorts)
-
- def const_or_class(self, args):
- if args[0].type == "CONST":
- self.const_store.use(args[0].value)
- return args[0]
-
- def compare_int(self, sorts: SMTSorts, op: str, a, b):
- # To extract the `int` contained in the attr_data_sort,
- # we need to call its `get_int` method on the `DatatypeRef`
- get_int = sorts.attr_data_sort.get_int
-
- a = get_int(a)
- b = get_int(b)
-
- if op == ">":
- return a > b
- if op == ">=":
- return a >= b
- if op == "<":
- return a < b
- if op == "<=":
- return a <= b
- if op == "==":
- return a == b
- if op == "!=":
- return a != b
- raise f"Invalid Compare Operator Symbol: {op}"
-
- def value(self, args):
- type = args[0].type
- value = args[0].value
-
- if type == "ESCAPED_STRING":
- value = value.replace('"', '')
- self.user_values_cache.add(value)
- return lambda enc, sorts: RefHandler.get_str(value, enc, sorts), RefHandler.STRING
- elif type == "NUMBER":
- return lambda _, sorts: RefHandler.get_int(value, sorts), RefHandler.INTEGER
- elif type == "BOOL":
- return lambda _, sorts: RefHandler.get_bool(value, sorts), RefHandler.BOOLEAN
- # elif type == "VALUE":
- # return lambda _, sorts: RefHandler.get_value(value, sorts), RefHandler.VALUE_REF
-
- def error_desc(self, args):
- def err_callback(
- solver: Solver,
- sorts: SMTSorts,
- intermediate_model: IntermediateModel,
- index: int,
- requirement_desc: str
- ) -> str:
- err_msg = args[0].value.replace('"', '')
- # Get list of free variables
- consts_name = self.const_store.get_free_vars(index)
- consts = RefHandler.get_consts(consts_name, sorts)
- notes = []
- try:
- model = solver.model()
- for const in consts:
- name = get_user_friendly_name(
- intermediate_model, model, const)
- err_msg = err_msg.replace(
- "{" + str(const) + "}", f"'{name}'")
- except:
- notes.append(
- "Model not found: it's not possible to show which element is causing the issue")
-
- # tell the user which variables are not free
- unused_free_vars = re.findall(r"{[^{}]*}", err_msg)
- if unused_free_vars:
- notes.append(
- "The following variables are not free and should be removed from the error description: " + " ".join(unused_free_vars))
-
- return (requirement_desc, err_msg, notes)
- return ("USER", err_callback)
-
-
-class SynthesisDOMLRTransformer(Transformer):
- # These callbacks will be called when a rule with the same name
- # is matched. It starts from the leaves.
- def __init__(self,
- const_store: VarStore,
- user_values_cache: StringValuesCache,
- visit_tokens: bool = True
- ) -> None:
- super().__init__(visit_tokens)
- self.const_store = const_store
- self.user_values_cache = user_values_cache
-
- def __default__(self, data, children, meta):
- return children
-
- # start
- def requirements(self, args) -> list[tuple]:
- return args
-
- def requirement(self, args) -> tuple:
- flip_expr: bool = args[0].value == "-"
- name: str = args[1]
- expr: Callable[[State], ExprRef] = args[2]
- return (
- expr,
- name.lower().replace(" ", "_"), # id
- flip_expr
- )
-
- def req_name(self, args) -> str:
- return str(args[0].value.replace('"', ''))
-
- # Requirement requirement expression
-
- def bound_consts(self, args):
- const_names = list(map(lambda arg: arg.value, args))
- for name in const_names:
- self.const_store.use(name)
- self.const_store.quantify(name)
- return lambda state: SynthesisRefHandler.get_consts(const_names, state)
-
- def negation(self, args):
- return lambda state: Not(args[0](state))
-
- def iff_expr(self, args):
- return lambda state: args[0](state) == args[1](state)
-
- def implies_expr(self, args):
- return lambda state: Implies(args[0](state), args[1](state))
-
- def and_expr(self, args):
- return lambda state: And([arg(state) for arg in args])
-
- def or_expr(self, args):
- return lambda state: Or([arg(state) for arg in args])
-
- def exists(self, args):
- return lambda state: Exists(args[0](state), args[1](state))
-
- def forall(self, args):
- return lambda state: ForAll(args[0](state), args[1](state))
-
- def rel_assoc_expr(self, args):
- """An ASSOCIATION relationship"""
- rel_name = args[1].value
- self.const_store.use(args[0].value)
- self.const_store.use(args[2].value)
-
- def _gen_rel_elem_expr(state: State):
- rel = SynthesisRefHandler.get_assoc(state, rel_name)
-
- return state.rels.AssocRel(
- SynthesisRefHandler.get_const(args[0].value, state),
- rel.ref,
- SynthesisRefHandler.get_const(args[2].value, state)
- )
- return _gen_rel_elem_expr
-
- def rel_attr_value_expr(self, args):
- """An ATTRIBUTE relationship with a rhs that is a value
-
- CONST "has" RELATIONSHIP COMPARISON_OP value
- 0 1 2 3
- """
-
- rel_name = args[1].value
-
- def _gen_rel_attr_value_expr(state: State):
- elem = SynthesisRefHandler.get_const(args[0].value, state)
- rel = SynthesisRefHandler.get_attr(state, rel_name)
-
- rhs_value, rhs_value_type = args[3]
- rhs_value = rhs_value(state)
- op = args[2].value
-
- if rhs_value_type == SynthesisRefHandler.INTEGER and rel.type == 'Integer':
- lhs_value = state.rels.int.AttrValueRel(elem, rel.ref)
- return And(
- self.compare(op, lhs_value, rhs_value),
- state.rels.int.AttrSynthRel(elem, rel.ref)
- )
- elif op != "==" and op != "!=":
- raise "You can only use == and != to compare Strings and Booleans!"
- elif rhs_value_type == SynthesisRefHandler.STRING:
- lhs_value = state.rels.str.AttrValueRel(elem, rel.ref)
-
- return And(
- lhs_value == rhs_value if op == "==" else lhs_value != rhs_value,
- state.rels.str.AttrSynthRel(elem, rel.ref)
- )
- elif rhs_value_type == SynthesisRefHandler.BOOLEAN:
- lhs_value = state.rels.bool.AttrValueRel(elem, rel.ref)
- return And(
- lhs_value == rhs_value if op == "==" else lhs_value != rhs_value,
- state.rels.bool.AttrSynthRel(elem, rel.ref)
- )
- else:
- raise f'Invalid value {rhs_value} during parsing for synthesis.'
-
- return _gen_rel_attr_value_expr
-
- def rel_attr_elem_expr(self, args):
- """An ATTRIBUTE relationship with a rhs that is another element
- CONST "has" RELATIONSHIP COMPARISON_OP CONST RELATIONSHIP
- 0 1 2 3 4
- """
-
- rel1_name = args[1].value
- rel2_name = args[4].value
- op = args[2].value
-
- def _gen_rel_attr_elem_expr(state: State):
- elem1 = SynthesisRefHandler.get_const(args[0].value, state)
- elem2 = SynthesisRefHandler.get_const(args[3].value, state)
- rel1 = SynthesisRefHandler.get_attr(state, rel1_name)
- rel2 = SynthesisRefHandler.get_attr(state, rel2_name)
-
- if rel1.type == rel2.type == 'Integer':
- return And(
- state.rels.int.AttrSynthRel(elem1, rel1.ref),
- state.rels.int.AttrSynthRel(elem2, rel2.ref),
- self.compare(
- op,
- state.rels.int.AttrValueRel(elem1, rel1.ref),
- state.rels.int.AttrValueRel(elem2, rel2.ref)
- )
- )
- if rel1.type == rel2.type == 'Boolean':
- return And(
- state.rels.bool.AttrSynthRel(elem1, rel1.ref),
- state.rels.bool.AttrSynthRel(elem2, rel2.ref),
- self.compare(
- op,
- state.rels.bool.AttrValueRel(elem1, rel1.ref),
- state.rels.bool.AttrValueRel(elem2, rel2.ref)
- )
- )
- if rel1.type == rel2.type == 'String':
- return And(
- state.rels.str.AttrSynthRel(elem1, rel1.ref),
- state.rels.str.AttrSynthRel(elem2, rel2.ref),
- self.compare(
- op,
- state.rels.str.AttrValueRel(elem1, rel1.ref),
- state.rels.str.AttrValueRel(elem2, rel2.ref)
- )
- )
- raise f'Attribute relationships {rel1_name} ({rel1.type}) and {rel2_name} ({rel2.type}) have mismatch type.'
-
- return _gen_rel_attr_elem_expr
-
- def _get_equality_sides(self, arg1, arg2):
- # We track use of const in const_or_class
- if arg1.type == "CONST" and arg2.type == "CONST":
- return (
- lambda state: SynthesisRefHandler.get_const(arg1.value, state),
- lambda state: SynthesisRefHandler.get_const(arg2.value, state)
- )
-
- if arg1.type == "CLASS":
- def arg1_ret(state): return SynthesisRefHandler.get_class(
- state, arg1.value)
- else:
- def arg1_ret(state): return SynthesisRefHandler.get_element_class(
- state, SynthesisRefHandler.get_const(arg1.value, state))
-
- if arg2.type == "CLASS":
- def arg2_ret(state): return SynthesisRefHandler.get_class(
- state, arg2.value)
- else:
- def arg2_ret(state): return SynthesisRefHandler.get_element_class(
- state, SynthesisRefHandler.get_const(arg2.value, state))
-
- return (arg1_ret, arg2_ret)
-
- def equality(self, args):
- a, b = self._get_equality_sides(args[0], args[1])
- return lambda state: a(state) == b(state)
-
- def inequality(self, args):
- a, b = self._get_equality_sides(args[0], args[1])
- return lambda state: a(state) != b(state)
-
- def const_or_class(self, args):
- if args[0].type == "CONST":
- self.const_store.use(args[0].value)
- return args[0]
-
- def compare(self, op: str, a, b):
-
- if op == ">":
- return a > b
- if op == ">=":
- return a >= b
- if op == "<":
- return a < b
- if op == "<=":
- return a <= b
- if op == "==":
- return a == b
- if op == "!=":
- return a != b
- raise f"Invalid Compare Operator Symbol: {op}"
-
- def value(self, args):
- type = args[0].type
- value = args[0].value
-
- if type == "ESCAPED_STRING":
- value = value.replace('"', '')
- self.user_values_cache.add(value)
- return lambda state: SynthesisRefHandler.get_str(value, state), SynthesisRefHandler.STRING
- elif type == "NUMBER":
- return lambda _: value, SynthesisRefHandler.INTEGER
- elif type == "BOOL":
- return lambda _: SynthesisRefHandler.get_bool(value), SynthesisRefHandler.BOOLEAN
-
-
def _get_error_desc_for_unexpected_characters(e: UnexpectedCharacters, input: str):
# Error description
msg = "Syntax Error:\n\n"
diff --git a/mc_openapi/doml_mc/domlr_parser/synthesis_transformer.py b/mc_openapi/doml_mc/domlr_parser/synthesis_transformer.py
new file mode 100644
index 0000000000000000000000000000000000000000..46de50cf0803ad26a82b2d4ff676141add729581
--- /dev/null
+++ b/mc_openapi/doml_mc/domlr_parser/synthesis_transformer.py
@@ -0,0 +1,248 @@
+from typing import Callable
+
+from doml_synthesis import State
+from lark import Transformer
+from z3 import And, Exists, ExprRef, ForAll, Implies, Not, Or
+
+from mc_openapi.doml_mc.domlr_parser.utils import (StringValuesCache,
+ SynthesisRefHandler,
+ VarStore)
+
+
+class SynthesisDOMLRTransformer(Transformer):
+ # These callbacks will be called when a rule with the same name
+ # is matched. It starts from the leaves.
+ def __init__(self,
+ const_store: VarStore,
+ user_values_cache: StringValuesCache,
+ visit_tokens: bool = True
+ ) -> None:
+ super().__init__(visit_tokens)
+ self.const_store = const_store
+ self.user_values_cache = user_values_cache
+
+ def __default__(self, data, children, meta):
+ return children
+
+ # start
+ def requirements(self, args) -> list[tuple]:
+ return args
+
+ def requirement(self, args) -> tuple:
+ flip_expr: bool = args[0].value == "-"
+ name: str = args[1]
+ expr: Callable[[State], ExprRef] = args[2]
+ return (
+ expr,
+ name.lower().replace(" ", "_"), # id
+ flip_expr
+ )
+
+ def req_name(self, args) -> str:
+ return str(args[0].value.replace('"', ''))
+
+ # Requirement requirement expression
+
+ def bound_consts(self, args):
+ const_names = list(map(lambda arg: arg.value, args))
+ for name in const_names:
+ self.const_store.use(name)
+ self.const_store.quantify(name)
+ return lambda state: SynthesisRefHandler.get_consts(const_names, state)
+
+ def negation(self, args):
+ return lambda state: Not(args[0](state))
+
+ def iff_expr(self, args):
+ return lambda state: args[0](state) == args[1](state)
+
+ def implies_expr(self, args):
+ return lambda state: Implies(args[0](state), args[1](state))
+
+ def and_expr(self, args):
+ return lambda state: And([arg(state) for arg in args])
+
+ def or_expr(self, args):
+ return lambda state: Or([arg(state) for arg in args])
+
+ def exists(self, args):
+ return lambda state: Exists(args[0](state), args[1](state))
+
+ def forall(self, args):
+ return lambda state: ForAll(args[0](state), args[1](state))
+
+ def rel_assoc_expr(self, args):
+ """An ASSOCIATION relationship"""
+ rel_name = args[1].value
+ self.const_store.use(args[0].value)
+ self.const_store.use(args[2].value)
+
+ def _gen_rel_elem_expr(state: State):
+ rel = SynthesisRefHandler.get_assoc(state, rel_name)
+
+ return state.rels.AssocRel(
+ SynthesisRefHandler.get_const(args[0].value, state),
+ rel.ref,
+ SynthesisRefHandler.get_const(args[2].value, state)
+ )
+ return _gen_rel_elem_expr
+
+ def rel_attr_value_expr(self, args):
+ """An ATTRIBUTE relationship with a rhs that is a value
+
+ CONST "has" RELATIONSHIP COMPARISON_OP value
+ 0 1 2 3
+ """
+
+ rel_name = args[1].value
+
+ def _gen_rel_attr_value_expr(state: State):
+ elem = SynthesisRefHandler.get_const(args[0].value, state)
+ rel = SynthesisRefHandler.get_attr(state, rel_name)
+
+ rhs_value, rhs_value_type = args[3]
+ rhs_value = rhs_value(state)
+ op = args[2].value
+
+ if rhs_value_type == SynthesisRefHandler.INTEGER and rel.type == 'Integer':
+ lhs_value = state.rels.int.AttrValueRel(elem, rel.ref)
+ return And(
+ self.compare(op, lhs_value, rhs_value),
+ state.rels.int.AttrSynthRel(elem, rel.ref)
+ )
+ elif op != "==" and op != "!=":
+ raise "You can only use == and != to compare Strings and Booleans!"
+ elif rhs_value_type == SynthesisRefHandler.STRING:
+ lhs_value = state.rels.str.AttrValueRel(elem, rel.ref)
+
+ return And(
+ lhs_value == rhs_value if op == "==" else lhs_value != rhs_value,
+ state.rels.str.AttrSynthRel(elem, rel.ref)
+ )
+ elif rhs_value_type == SynthesisRefHandler.BOOLEAN:
+ lhs_value = state.rels.bool.AttrValueRel(elem, rel.ref)
+ return And(
+ lhs_value == rhs_value if op == "==" else lhs_value != rhs_value,
+ state.rels.bool.AttrSynthRel(elem, rel.ref)
+ )
+ else:
+ raise f'Invalid value {rhs_value} during parsing for synthesis.'
+
+ return _gen_rel_attr_value_expr
+
+ def rel_attr_elem_expr(self, args):
+ """An ATTRIBUTE relationship with a rhs that is another element
+ CONST "has" RELATIONSHIP COMPARISON_OP CONST RELATIONSHIP
+ 0 1 2 3 4
+ """
+
+ rel1_name = args[1].value
+ rel2_name = args[4].value
+ op = args[2].value
+
+ def _gen_rel_attr_elem_expr(state: State):
+ elem1 = SynthesisRefHandler.get_const(args[0].value, state)
+ elem2 = SynthesisRefHandler.get_const(args[3].value, state)
+ rel1 = SynthesisRefHandler.get_attr(state, rel1_name)
+ rel2 = SynthesisRefHandler.get_attr(state, rel2_name)
+
+ if rel1.type == rel2.type == 'Integer':
+ return And(
+ state.rels.int.AttrSynthRel(elem1, rel1.ref),
+ state.rels.int.AttrSynthRel(elem2, rel2.ref),
+ self.compare(
+ op,
+ state.rels.int.AttrValueRel(elem1, rel1.ref),
+ state.rels.int.AttrValueRel(elem2, rel2.ref)
+ )
+ )
+ if rel1.type == rel2.type == 'Boolean':
+ return And(
+ state.rels.bool.AttrSynthRel(elem1, rel1.ref),
+ state.rels.bool.AttrSynthRel(elem2, rel2.ref),
+ self.compare(
+ op,
+ state.rels.bool.AttrValueRel(elem1, rel1.ref),
+ state.rels.bool.AttrValueRel(elem2, rel2.ref)
+ )
+ )
+ if rel1.type == rel2.type == 'String':
+ return And(
+ state.rels.str.AttrSynthRel(elem1, rel1.ref),
+ state.rels.str.AttrSynthRel(elem2, rel2.ref),
+ self.compare(
+ op,
+ state.rels.str.AttrValueRel(elem1, rel1.ref),
+ state.rels.str.AttrValueRel(elem2, rel2.ref)
+ )
+ )
+ raise f'Attribute relationships {rel1_name} ({rel1.type}) and {rel2_name} ({rel2.type}) have mismatch type.'
+
+ return _gen_rel_attr_elem_expr
+
+ def _get_equality_sides(self, arg1, arg2):
+ # We track use of const in const_or_class
+ if arg1.type == "CONST" and arg2.type == "CONST":
+ return (
+ lambda state: SynthesisRefHandler.get_const(arg1.value, state),
+ lambda state: SynthesisRefHandler.get_const(arg2.value, state)
+ )
+
+ if arg1.type == "CLASS":
+ def arg1_ret(state): return SynthesisRefHandler.get_class(
+ state, arg1.value)
+ else:
+ def arg1_ret(state): return SynthesisRefHandler.get_element_class(
+ state, SynthesisRefHandler.get_const(arg1.value, state))
+
+ if arg2.type == "CLASS":
+ def arg2_ret(state): return SynthesisRefHandler.get_class(
+ state, arg2.value)
+ else:
+ def arg2_ret(state): return SynthesisRefHandler.get_element_class(
+ state, SynthesisRefHandler.get_const(arg2.value, state))
+
+ return (arg1_ret, arg2_ret)
+
+ def equality(self, args):
+ a, b = self._get_equality_sides(args[0], args[1])
+ return lambda state: a(state) == b(state)
+
+ def inequality(self, args):
+ a, b = self._get_equality_sides(args[0], args[1])
+ return lambda state: a(state) != b(state)
+
+ def const_or_class(self, args):
+ if args[0].type == "CONST":
+ self.const_store.use(args[0].value)
+ return args[0]
+
+ def compare(self, op: str, a, b):
+
+ if op == ">":
+ return a > b
+ if op == ">=":
+ return a >= b
+ if op == "<":
+ return a < b
+ if op == "<=":
+ return a <= b
+ if op == "==":
+ return a == b
+ if op == "!=":
+ return a != b
+ raise f"Invalid Compare Operator Symbol: {op}"
+
+ def value(self, args):
+ type = args[0].type
+ value = args[0].value
+
+ if type == "ESCAPED_STRING":
+ value = value.replace('"', '')
+ self.user_values_cache.add(value)
+ return lambda state: SynthesisRefHandler.get_str(value, state), SynthesisRefHandler.STRING
+ elif type == "NUMBER":
+ return lambda _: value, SynthesisRefHandler.INTEGER
+ elif type == "BOOL":
+ return lambda _: SynthesisRefHandler.get_bool(value), SynthesisRefHandler.BOOLEAN
+
diff --git a/mc_openapi/doml_mc/domlr_parser/transformer.py b/mc_openapi/doml_mc/domlr_parser/transformer.py
new file mode 100644
index 0000000000000000000000000000000000000000..76aed5f2ae2309af385d00e13d632fbef13ec099
--- /dev/null
+++ b/mc_openapi/doml_mc/domlr_parser/transformer.py
@@ -0,0 +1,332 @@
+import logging
+import re
+from collections import ChainMap
+from typing import Callable, Literal
+
+from lark import Transformer
+from z3 import And, Exists, ExprRef, ForAll, Implies, Not, Or, Solver
+
+from mc_openapi.doml_mc.domlr_parser.utils import (RefHandler,
+ StringValuesCache, VarStore)
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model.doml_element import \
+ IntermediateModel
+
+
+class DOMLRTransformer(Transformer):
+ # These callbacks will be called when a rule with the same name
+ # is matched. It starts from the leaves.
+ def __init__(self,
+ const_store: VarStore,
+ user_values_cache: StringValuesCache,
+ visit_tokens: bool = True
+ ) -> None:
+ super().__init__(visit_tokens)
+ self.const_store = const_store
+ self.user_values_cache = user_values_cache
+
+ def __default__(self, data, children, meta):
+ return children
+
+ # start
+ def start(self, args) -> tuple[list[Requirement], dict[str, str]]:
+ if not isinstance(args[0], dict): # there aren't flags
+ args = [{}, args[0]]
+ return args[1], args[0]
+
+ def flags(self, args) -> dict:
+ return dict(ChainMap(*list(args)))
+
+ def flag_requirement_check(self, args) -> dict:
+ return { args[0].value : True }
+
+ def flag_requirement_check_consistency(self, args) -> dict:
+ return { '_check_consistency' : True }
+
+ def flag_requirement_ignore(self, args) -> dict:
+ return { args[0].value : False }
+
+ def flag_requirement_ignore_builtin(self, args) -> dict:
+ return { '_ignore_builtin' : True }
+
+ def flag_csp(self, args) -> dict:
+ return { '_csp' : True }
+
+ def requirements(self, args) -> list[Requirement]:
+ return args
+
+ def requirement(self, args) -> Requirement:
+ flip_expr: bool = args[0].value == "-"
+ name: str = args[1]
+ expr: Callable[[SMTEncoding, SMTSorts], ExprRef] = args[2]
+ errd: tuple[Literal["USER", "BUILTIN"], Callable[[Solver, SMTSorts,
+ IntermediateModel, int], str]] = args[3]
+ index = self.const_store.get_index_and_push()
+ return Requirement(
+ expr,
+ name.lower().replace(" ", "_"),
+ name,
+ (errd[0], lambda solver, sorts, model: errd[1](
+ solver, sorts, model,
+ index,
+ name
+ )),
+ flipped=flip_expr
+ )
+
+ def req_name(self, args) -> str:
+ return str(args[0].value.replace('"', ''))
+
+ # Requirement requirement expression
+
+ def bound_consts(self, args):
+ const_names = list(map(lambda arg: arg.value, args))
+ for name in const_names:
+ self.const_store.use(name)
+ self.const_store.quantify(name)
+ return lambda _, sorts: RefHandler.get_consts(const_names, sorts)
+
+ def negation(self, args):
+ return lambda enc, sorts: Not(args[0](enc, sorts))
+
+ def iff_expr(self, args):
+ return lambda enc, sorts: args[0](enc, sorts) == args[1](enc, sorts)
+
+ def implies_expr(self, args):
+ return lambda enc, sorts: Implies(args[0](enc, sorts), args[1](enc, sorts))
+
+ def and_expr(self, args):
+ return lambda enc, sorts: And([arg(enc, sorts) for arg in args])
+
+ def or_expr(self, args):
+ return lambda enc, sorts: Or([arg(enc, sorts) for arg in args])
+
+ def exists(self, args):
+ return lambda enc, sorts: Exists(args[0](enc, sorts), args[1](enc, sorts))
+
+ def forall(self, args):
+ return lambda enc, sorts: ForAll(args[0](enc, sorts), args[1](enc, sorts))
+
+ def rel_assoc_expr(self, args):
+ """An ASSOCIATION relationship"""
+ rel_name = args[1].value
+ self.const_store.use(args[0].value)
+ self.const_store.use(args[2].value)
+
+ def _gen_rel_elem_expr(enc: SMTEncoding, sorts: SMTSorts):
+ rel, rel_type = RefHandler.get_relationship(enc, rel_name)
+
+ assert rel_type == RefHandler.ASSOCIATION
+
+ return RefHandler.get_association_rel(
+ enc,
+ RefHandler.get_const(args[0].value, sorts),
+ rel,
+ RefHandler.get_const(args[2].value, sorts)
+ )
+ return _gen_rel_elem_expr
+
+ def rel_attr_value_expr(self, args):
+ """An ATTRIBUTE relationship with a rhs that is a value"""
+
+ rel_name = args[1].value
+
+ def _gen_rel_attr_value_expr(enc: SMTEncoding, sorts: SMTSorts):
+ elem = RefHandler.get_const(args[0].value, sorts)
+ rel, rel_type = RefHandler.get_relationship(enc, rel_name)
+ assert rel_type == RefHandler.ATTRIBUTE
+
+ rhs_value, rhs_value_type = args[3]
+ rhs_value = rhs_value(enc, sorts)
+ op = args[2].value
+
+ if rhs_value_type == RefHandler.INTEGER:
+
+ lhs_value = RefHandler.get_value("x", sorts)
+
+ return And(
+ RefHandler.get_attribute_rel(enc,
+ elem,
+ rel,
+ lhs_value
+ ),
+ self.compare_int(sorts, op, lhs_value, rhs_value)
+ )
+ elif rhs_value_type == RefHandler.STRING or rhs_value_type == RefHandler.BOOLEAN:
+ expr = RefHandler.get_attribute_rel(enc,
+ elem,
+ rel,
+ rhs_value
+ )
+ if op == "==":
+ return expr
+ elif op == "!=":
+ return Not(expr)
+ else:
+ raise f'Invalid compare operator "{op}". It must be "==" or "!=".'
+
+ return _gen_rel_attr_value_expr
+
+ def rel_attr_elem_expr(self, args):
+ """An ATTRIBUTE relationship with a rhs that is another element"""
+
+ rel1_name = args[1].value
+ rel2_name = args[4].value
+ op = args[2].value
+
+ def _gen_rel_attr_elem_expr(enc: SMTEncoding, sorts: SMTSorts):
+ elem1 = RefHandler.get_const(args[0].value, sorts)
+ elem2 = RefHandler.get_const(args[3].value, sorts)
+ rel1, rel1_type = RefHandler.get_relationship(enc, rel1_name)
+ rel2, rel2_type = RefHandler.get_relationship(enc, rel2_name)
+
+ assert rel1_type == RefHandler.ATTRIBUTE
+ assert rel2_type == RefHandler.ATTRIBUTE
+
+ rhs_value = RefHandler.get_value("x", sorts)
+
+ expr = And(
+ RefHandler.get_attribute_rel(enc,
+ elem1,
+ rel1,
+ rhs_value
+ ),
+ RefHandler.get_attribute_rel(enc,
+ elem2,
+ rel2,
+ rhs_value
+ )
+ )
+ if op == "==":
+ return expr
+ elif op == "!=":
+ return Not(expr)
+ else:
+ rhs1_value = RefHandler.get_value("rhs1", sorts)
+ rhs2_value = RefHandler.get_value("rhs2", sorts)
+ expr = And(
+ RefHandler.get_attribute_rel(enc,
+ elem1,
+ rel1,
+ rhs1_value
+ ),
+ RefHandler.get_attribute_rel(enc,
+ elem2,
+ rel2,
+ rhs2_value
+ ),
+ self.compare_int(sorts, op, rhs1_value, rhs2_value)
+ )
+ logging.warning(
+ "Warning: Comparing attributes of two elements with {op} is experimental!\n",
+ "Assumption: the attribute is an Integer."
+ )
+ return expr
+
+ return _gen_rel_attr_elem_expr
+
+ def _get_equality_sides(self, arg1, arg2):
+ # We track use of const in const_or_class
+ if arg1.type == "CONST" and arg2.type == "CONST":
+ return (
+ lambda _, sorts: RefHandler.get_const(arg1.value, sorts),
+ lambda _, sorts: RefHandler.get_const(arg2.value, sorts)
+ )
+
+ if arg1.type == "CLASS":
+ def arg1_ret(enc, _): return RefHandler.get_class(enc, arg1.value)
+ else:
+ def arg1_ret(enc, sorts): return RefHandler.get_element_class(
+ enc, RefHandler.get_const(arg1.value, sorts))
+
+ if arg2.type == "CLASS":
+ def arg2_ret(enc, _): return RefHandler.get_class(enc, arg2.value)
+ else:
+ def arg2_ret(enc, sorts): return RefHandler.get_element_class(
+ enc, RefHandler.get_const(arg2.value, sorts))
+
+ return (arg1_ret, arg2_ret)
+
+ def equality(self, args):
+ a, b = self._get_equality_sides(args[0], args[1])
+ return lambda enc, sorts: a(enc, sorts) == b(enc, sorts)
+
+ def inequality(self, args):
+ a, b = self._get_equality_sides(args[0], args[1])
+ return lambda enc, sorts: a(enc, sorts) != b(enc, sorts)
+
+ def const_or_class(self, args):
+ if args[0].type == "CONST":
+ self.const_store.use(args[0].value)
+ return args[0]
+
+ def compare_int(self, sorts: SMTSorts, op: str, a, b):
+ # To extract the `int` contained in the attr_data_sort,
+ # we need to call its `get_int` method on the `DatatypeRef`
+ get_int = sorts.attr_data_sort.get_int
+
+ a = get_int(a)
+ b = get_int(b)
+
+ if op == ">":
+ return a > b
+ if op == ">=":
+ return a >= b
+ if op == "<":
+ return a < b
+ if op == "<=":
+ return a <= b
+ if op == "==":
+ return a == b
+ if op == "!=":
+ return a != b
+ raise f"Invalid Compare Operator Symbol: {op}"
+
+ def value(self, args):
+ type = args[0].type
+ value = args[0].value
+
+ if type == "ESCAPED_STRING":
+ value = value.replace('"', '')
+ self.user_values_cache.add(value)
+ return lambda enc, sorts: RefHandler.get_str(value, enc, sorts), RefHandler.STRING
+ elif type == "NUMBER":
+ return lambda _, sorts: RefHandler.get_int(value, sorts), RefHandler.INTEGER
+ elif type == "BOOL":
+ return lambda _, sorts: RefHandler.get_bool(value, sorts), RefHandler.BOOLEAN
+ # elif type == "VALUE":
+ # return lambda _, sorts: RefHandler.get_value(value, sorts), RefHandler.VALUE_REF
+
+ def error_desc(self, args):
+ def err_callback(
+ solver: Solver,
+ sorts: SMTSorts,
+ intermediate_model: IntermediateModel,
+ index: int,
+ requirement_desc: str
+ ) -> str:
+ err_msg = args[0].value.replace('"', '')
+ # Get list of free variables
+ consts_name = self.const_store.get_free_vars(index)
+ consts = RefHandler.get_consts(consts_name, sorts)
+ notes = []
+ try:
+ model = solver.model()
+ for const in consts:
+ name = get_user_friendly_name(
+ intermediate_model, model, const)
+ err_msg = err_msg.replace(
+ "{" + str(const) + "}", f"'{name}'")
+ except:
+ notes.append(
+ "Model not found: it's not possible to show which element is causing the issue")
+
+ # tell the user which variables are not free
+ unused_free_vars = re.findall(r"{[^{}]*}", err_msg)
+ if unused_free_vars:
+ notes.append(
+ "The following variables are not free and should be removed from the error description: " + " ".join(unused_free_vars))
+
+ return (requirement_desc, err_msg, notes)
+ return ("USER", err_callback)
diff --git a/mc_openapi/doml_mc/html_output.py b/mc_openapi/doml_mc/html_output.py
new file mode 100644
index 0000000000000000000000000000000000000000..09d215cd474ad9d04c1594d7243f5fbd1314a7c9
--- /dev/null
+++ b/mc_openapi/doml_mc/html_output.py
@@ -0,0 +1,16 @@
+def html_template(
+ title: str,
+ content: str
+):
+ return f"""<!doctype html>
+<html lang="en">
+<head>
+ <meta charset="utf-8">
+ <meta name="viewport" content="width=device-width, initial-scale=1">
+ <title>{title}</title>
+</head>
+<body>
+{content}
+</body>
+</html>
+"""
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/imc.py b/mc_openapi/doml_mc/imc.py
index b07fa528a06b5ddcfa8ed0eaa53f1a5faafb26f7..68aaa87d8f83ee587d20fa2da251c7af4332dab3 100644
--- a/mc_openapi/doml_mc/imc.py
+++ b/mc_openapi/doml_mc/imc.py
@@ -62,6 +62,9 @@ class RequirementStore:
def get_one_requirement(self, index: int) -> Requirement:
return self.get_all_requirements()[index]
+ def skip_requirements_by_id(self, requirement_ids: list[str]):
+ self.requirements = [r for r in self.requirements if not r.assert_name in requirement_ids]
+
def __len__(self):
return len(self.get_all_requirements())
diff --git a/mc_openapi/doml_mc/intermediate_model/metamodel.py b/mc_openapi/doml_mc/intermediate_model/metamodel.py
index a3874b17ec3e3ef53f65f0fc8e1229293e496bc4..e44e6cb3593d7ff9ab24ff7eae87b3881fd7e163 100644
--- a/mc_openapi/doml_mc/intermediate_model/metamodel.py
+++ b/mc_openapi/doml_mc/intermediate_model/metamodel.py
@@ -27,6 +27,7 @@ class DOMLVersion(Enum):
return DOMLVersion[doml_ver]
def has_DOMLR_support(v: "DOMLVersion"):
+ """DOMLR is available in v2.2 and later"""
return v != DOMLVersion.V2_0 and v != DOMLVersion.V2_1
diff --git a/mc_openapi/doml_mc/main.py b/mc_openapi/doml_mc/main.py
new file mode 100644
index 0000000000000000000000000000000000000000..189bb72a7eb7a000736a534b2f934cd6ad818990
--- /dev/null
+++ b/mc_openapi/doml_mc/main.py
@@ -0,0 +1,160 @@
+import logging
+from typing import Optional
+
+import doml_synthesis as DOMLS
+from doml_synthesis import State, builtin_requirements
+
+from mc_openapi.doml_mc import ModelChecker
+from mc_openapi.doml_mc.common_reqs import CommonRequirements
+from mc_openapi.doml_mc.consistency_reqs import get_association_multiplicity_reqs, get_association_type_reqs, get_attribute_multiplicity_reqs, get_attribute_type_reqs, get_inverse_association_reqs
+from mc_openapi.doml_mc.csp_compatibility import \
+ CSPCompatibilityValidator as csp_comp
+from mc_openapi.doml_mc.domlr_parser import (DOMLRTransformer, Parser,
+ SynthesisDOMLRTransformer)
+from mc_openapi.doml_mc.imc import RequirementStore
+from mc_openapi.doml_mc.intermediate_model.metamodel import (DOMLVersion,
+ MetaModelDocs)
+
+
+def init_model(domlx:bytes, doml_ver: DOMLVersion):
+ dmc = ModelChecker(domlx, doml_ver)
+ logging.info("Parsed DOMLX successfully.")
+ return dmc
+
+
+def verify_model(
+ dmc: ModelChecker,
+ external_domlr: Optional[str] = None,
+ threads: int = 2,
+ consistency_checks: bool = False,
+ skip_builtin_checks: bool = False
+ ):
+ # DOMLR parser
+ domlr_parser = Parser(DOMLRTransformer)
+
+ # General req store
+ req_store = RequirementStore()
+
+ # Store of Requirements and unique string constants
+ user_req_store, user_req_str_consts = RequirementStore(), []
+
+ flags = {}
+
+ # Parse external DOMLR file
+ if external_domlr:
+ user_req_store, user_req_str_consts = domlr_parser.parse(external_domlr)
+
+ # Parse internal DOMLR requirements
+ if DOMLVersion.has_DOMLR_support(dmc.doml_version):
+ func_reqs = dmc.domlr_requirements
+ for _, req_text in func_reqs:
+ doml_req_store, doml_req_str_consts, doml_req_flags = domlr_parser.parse(req_text)
+ user_req_store += doml_req_store
+ user_req_str_consts += doml_req_str_consts
+ flags |= doml_req_flags
+
+ # Remove duplicate tokens
+ user_req_str_consts = list(set(user_req_str_consts))
+
+ # Built-in requirements
+ if not (flags.get('_ignore_builtin', False) or skip_builtin_checks):
+ req_store += CommonRequirements[dmc.doml_version]
+ # Skip selected requirements
+ req_store.skip_requirements_by_id([k for k,v in flags.items() if not k.startswith("_") and v is False])
+
+ # Consistency requirements (disabled by default)
+ if flags.get('_check_consistency', False) or consistency_checks:
+ logging.warning("Consistency checks are outdated and may break at any time.")
+ req_store = req_store \
+ + get_attribute_type_reqs(dmc.metamodel) \
+ + get_attribute_multiplicity_reqs(dmc.metamodel) \
+ + get_association_type_reqs(dmc.metamodel) \
+ + get_association_multiplicity_reqs(dmc.metamodel) \
+ + get_inverse_association_reqs(dmc.inv_assoc)
+
+ # Add user requirements at the end
+ req_store += user_req_store
+
+ # Log all requirements to check
+ logging.debug("Checking following requirements: " + ", ".join([k.assert_name for k in req_store.get_all_requirements()]))
+
+ # Check CSP
+ if flags.get('_csp', False):
+ logging.warning("The CSP compatibility check is not yet implemented via DOMLR")
+
+ # Check satisfiability
+ results = dmc.check_requirements(
+ req_store,
+ threads=threads,
+ user_str_values=user_req_str_consts,
+ disable_multithreading=(threads == 1)
+ )
+
+ res, msg = results.summarize()
+
+ return res, msg
+
+def synthesize_model(dmc: ModelChecker, external_domlr: str, max_tries: int):
+ logging.warn("Synthesis is experimental and might not be up-to-date with the latest DOML.")
+
+ synth_domlr_parser = Parser(SynthesisDOMLRTransformer)
+ mm = MetaModelDocs[dmc.doml_version]
+ 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()
+ }
+
+ user_req_store, user_req_str_consts = [], []
+
+
+ if external_domlr:
+ user_req_store, user_req_str_consts = synth_domlr_parser.parse(external_domlr, for_synthesis=True)
+
+
+ # Parse internal DOMLR requirements
+ if DOMLVersion.has_DOMLR_support(dmc.doml_version):
+ func_reqs = dmc.domlr_requirements
+ for _, req_text in func_reqs:
+ doml_req_store, doml_req_str_consts, doml_req_flags = synth_domlr_parser.parse(req_text, for_synthesis=True)
+ user_req_store += doml_req_store
+ user_req_str_consts += doml_req_str_consts
+ flags |= doml_req_flags
+
+ # Remove duplicated strings
+ user_req_str_consts = list(set(user_req_str_consts))
+
+ state = State()
+ # Parse MM and IM
+ state = DOMLS.init_data(
+ state,
+ doml=im,
+ metamodel=mm,
+ )
+
+ reqs = user_req_store
+
+ # TODO: Filter requirements according to flags
+ reqs += builtin_requirements
+
+ state = DOMLS.solve(
+ state,
+ requirements=reqs,
+ strings=user_req_str_consts,
+ max_tries=max_tries
+ )
+ # Update state
+ state = DOMLS.save_results(state)
+ # Print output
+ state = DOMLS.check_synth_results(state)
+
+
+def verify_csp_compatibility(dmc: ModelChecker):
+ csp_comp.check(dmc.intermediate_model, dmc.doml_version)
+ # TODO: Refactor CSP to output a datastructure/table to print via CLI or REST
+ exit(0)
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/mc.py b/mc_openapi/doml_mc/mc.py
index b675b6e4e4d65ba6356bfb9e3c2a92cc3b1d1d3c..315f186d8563d281aafd8027a13f8ec0823ee6bc 100644
--- a/mc_openapi/doml_mc/mc.py
+++ b/mc_openapi/doml_mc/mc.py
@@ -19,36 +19,21 @@ from .xmi_parser.doml_model import parse_doml_model
class ModelChecker:
def __init__(self, xmi_model: bytes, doml_version: Optional[DOMLVersion] = None):
- self.intermediate_model, self.doml_version = parse_doml_model(
+ self.intermediate_model, self.doml_version, self.domlr_requirements = parse_doml_model(
xmi_model, doml_version)
self.metamodel = MetaModels[self.doml_version]
self.inv_assoc = InverseAssociations[self.doml_version]
def check_requirements(
self,
- threads: int = 1,
- user_requirements: Optional[RequirementStore] = None,
+ req_store: RequirementStore,
+ threads: int = 2,
user_str_values: list[str] = [],
- skip_common_requirements: bool = False,
- consistency_checks: bool = False,
- timeout: Optional[int] = None
+ timeout: Optional[int] = None,
+ disable_multithreading: bool = False
) -> MCResults:
assert self.metamodel and self.inv_assoc
- req_store = RequirementStore([])
-
- if not skip_common_requirements:
- req_store += CommonRequirements[self.doml_version]
-
- if consistency_checks:
- req_store = req_store \
- + get_attribute_type_reqs(self.metamodel) \
- + get_attribute_multiplicity_reqs(self.metamodel) \
- + get_association_type_reqs(self.metamodel) \
- + get_association_multiplicity_reqs(self.metamodel) \
- + get_inverse_association_reqs(self.inv_assoc)
-
- if user_requirements:
- req_store += user_requirements
+
def worker(rfrom: int, rto: int):
imc = IntermediateModelChecker(
@@ -67,13 +52,14 @@ class ModelChecker:
yield rfrom, rto
try:
- with parallel_backend('loky', n_jobs=threads):
- results = Parallel(timeout=timeout)(delayed(worker)(
- rfrom, rto) for rfrom, rto in split_reqs(len(req_store), threads))
+ if disable_multithreading:
+ # Easier debug
+ results =[ worker(0, len(req_store) )]
- # Uncomment for ease of debug
- # Disables parallel parsing
- # results =[ worker(0, len(req_store) )]
+ else:
+ with parallel_backend('loky', n_jobs=threads):
+ results = Parallel(timeout=timeout)(delayed(worker)(
+ rfrom, rto) for rfrom, rto in split_reqs(len(req_store), threads))
ret = MCResults([])
for res in results:
diff --git a/mc_openapi/doml_mc/xmi_parser/doml_model.py b/mc_openapi/doml_mc/xmi_parser/doml_model.py
index 9359ddacce9ec300c533d58e18383971953d4830..03fd187e347f39d10959e64f2cbc624c0a34ba72 100644
--- a/mc_openapi/doml_mc/xmi_parser/doml_model.py
+++ b/mc_openapi/doml_mc/xmi_parser/doml_model.py
@@ -48,26 +48,9 @@ def parse_xmi_model(raw_model: bytes, doml_version: DOMLVersion) -> EObject:
resource.load()
return resource.contents[0]
+DOMLRRawRequirements = list[tuple[str, str]]
-def infer_domlx_version(raw_model: bytes) -> DOMLVersion:
- root = etree.fromstring(raw_model)
- if root.tag == "{http://www.piacere-project.eu/doml/commons}DOMLModel":
- if "version" in root.attrib:
- v_str = root.attrib["version"]
- try:
- return DOMLVersion(v_str)
- except ValueError:
- if v_str == "v2":
- return DOMLVersion.V2_0
- else:
- raise RuntimeError(f"DOML model is using an unsupported version: {v_str}")
- else:
- return DOMLVersion.V2_0 # Should be DOMLVersion.V1_0, but we use V2_0 because the 2.1 IDE doesn't fill it
- else:
- raise RuntimeError(f"The DOML version is unsupported or the model is malformed.\nLowest supported version is: {DOMLVersion.V2_0}")
-
-
-def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> Tuple[IntermediateModel, DOMLVersion]:
+def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> Tuple[IntermediateModel, DOMLVersion, Optional[DOMLRRawRequirements]]:
# if doml_version is None:
# doml_version = infer_domlx_version(raw_model)
@@ -132,10 +115,11 @@ def parse_doml_model(raw_model: bytes, doml_version: Optional[DOMLVersion]) -> T
reciprocate_inverse_associations(im, InverseAssociations[doml_version])
- return im, doml_version
-
-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)
+ # If there are DOMLR requirements
+ try:
+ domlr = model.functionalRequirements.items
+ domlr = [(req.name, req.description.replace("```", "")) for req in domlr]
+ logging.info("Found DOMLR requirements in DOML model.")
+ except Exception:
+ domlr = None
+ return im, doml_version, domlr
diff --git a/mc_openapi/handlers.py b/mc_openapi/handlers.py
index 7808d5925affc673a41ddf40e8070745a0d7c5fb..488b6a87fafbd59977e318003ec170af58702256 100644
--- a/mc_openapi/handlers.py
+++ b/mc_openapi/handlers.py
@@ -1,12 +1,11 @@
import datetime
import logging
import os
-from mc_openapi.doml_mc.domlr_parser.parser import DOMLRTransformer, Parser
-from mc_openapi.doml_mc.imc import RequirementStore
+from mc_openapi.doml_mc.html_output import html_template
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
+from mc_openapi.doml_mc import verify_model, init_model, verify_csp_compatibility
+from .doml_mc import MCResult
def make_error(user_msg, debug_msg=None):
@@ -17,58 +16,62 @@ def make_error(user_msg, debug_msg=None):
return result
-def post(body, version=None):
+def modelcheck(body, version=None):
+ return mc(body, version)
+
+def modelcheck_html(body, version=None):
+ return mc(body, version, isHtml=True)
+
+def mc(body, version, isHtml = False):
doml_xmi = body
+ doml_version_str: str = None
+ doml_version: DOMLVersion = None
try:
- doml_version = None
- try:
- doml_version: str = os.environ["DOML_VERSION"]
- except:
- pass
- if version:
- doml_version: str = version
- if doml_version:
- doml_version = DOMLVersion.get(doml_version)
+ # First try to infer DOML version from ENV, then query params
+ doml_version_str = os.environ.get("DOML_VERSION") or version
+
+ if doml_version_str:
+ doml_version = DOMLVersion.get(doml_version_str)
logging.info(f"Forcing DOML {doml_version.value}")
- dmc = ModelChecker(doml_xmi, doml_version)
-
- user_req_store = None
- user_req_str_consts = []
+ dmc = init_model(doml_xmi, doml_version)
- # Add support for Requirements in DOML
- if DOMLVersion.has_DOMLR_support(dmc.doml_version):
- domlr_parser = Parser(DOMLRTransformer)
- model = get_pyecore_model(doml_xmi, dmc.doml_version)
- func_reqs = model.functionalRequirements.items
+ res, msg = verify_model(dmc)
- user_req_store = RequirementStore()
+ if isHtml:
+ return html_template("DOML Model Checker - Results", "HELLO WORLD!")
+ else:
+ if res == MCResult.sat:
+ return {
+ "result": "sat",
+ "doml_version": dmc.doml_version.value
+ }
+ else:
+ return {
+ "result": res.name,
+ "doml_version": dmc.doml_version.value,
+ "description": f'[Using DOML {dmc.doml_version.value}]\n{msg}'
+ }
- 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
+ except Exception as e:
+ return make_error("The supplied DOMLX model is malformed or its DOML version is unsupported.", debug_msg=str(e)), 400
- 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()
+def csp(body, version=None):
+ doml_xmi = body
+ doml_version_str: str = None
+ doml_version: DOMLVersion = None
+ try:
+ # First try to infer DOML version from ENV, then query params
+ doml_version_str = os.environ.get("DOML_VERSION") or version
+
+ if doml_version_str:
+ doml_version = DOMLVersion.get(doml_version_str)
+ logging.info(f"Forcing DOML {doml_version.value}")
- if res == MCResult.sat:
- return {
- "result": "sat",
- "doml_version": dmc.doml_version.value
- }
- else:
- return {
- "result": res.name,
- "doml_version": dmc.doml_version.value,
- "description": f'[Using DOML {dmc.doml_version.value}]\n{msg}'
- }
+ dmc = init_model(doml_xmi, doml_version)
+
+ # TODO: Do something with the results
+ verify_csp_compatibility(dmc)
- # TODO: Make noteworthy exceptions to at least tell the user what is wrong
except Exception as e:
return make_error("The supplied DOMLX model is malformed or its DOML version is unsupported.", debug_msg=str(e)), 400
diff --git a/mc_openapi/openapi/model_checker.yaml b/mc_openapi/openapi/model_checker.yaml
index 6f4e6a4145d102c56e0d567aca80afcd5b765007..1cb4f6e761567db33bcd8f01ed62d7025427668c 100644
--- a/mc_openapi/openapi/model_checker.yaml
+++ b/mc_openapi/openapi/model_checker.yaml
@@ -8,10 +8,10 @@ paths:
/modelcheck:
post:
summary: Verify a DOML model
- description: Send a DOML model in XMI format and a requirement to check.
- The response says whether the requirements are satisfied by the model,
+ description: Send a DOML model in XMI format.
+ The response says whether the model satisfies the requirements,
with a description of the issue if it is not.
- operationId: mc_openapi.handlers.post
+ operationId: mc_openapi.handlers.modelcheck
requestBody:
content:
application/xml:
@@ -58,6 +58,80 @@ paths:
schema:
$ref: '#/components/schemas/error'
description: internal error
+ /modelcheck_html:
+ post:
+ summary: Verify a DOML model
+ description: Send a DOML model in XMI format.
+ The response says whether the model satisfies the requirements,
+ with a description of the issue if it is not. The output is in HTML.
+ operationId: mc_openapi.handlers.modelcheck_html
+ requestBody:
+ content:
+ application/xml:
+ schema:
+ type: string
+ required: true
+ parameters:
+ - in: query
+ name: version
+ schema:
+ type: string
+ description: >
+ The DOML version you're currently using, written as e.g. `2.0` or `V2_0`.
+ If not specified, it will try to infer it by trying to parse it for each supported
+ DOML version, starting with the most recent.
+ required: false
+ responses:
+ "200":
+ content:
+ text/html:
+ schema:
+ type: string
+ description: OK - model checking succeded
+ "400":
+ content:
+ application/json:
+ schema:
+ $ref: '#/components/schemas/error'
+ description: malformed request
+ "500":
+ content:
+ application/json:
+ schema:
+ $ref: '#/components/schemas/error'
+ description: internal error
+ /csp:
+ post:
+ summary: Verify compatibility of a DOML model with a set of Cloud Service Providers.
+ description: Send a DOML model in XMI format and a requirement to check.
+ The response says whether the model can be deployed on the supported CSPs.
+ It produces a compatibility matrix and lists required properties for each CSP.
+ operationId: mc_openapi.handlers.csp
+ requestBody:
+ content:
+ application/xml:
+ schema:
+ type: string
+ required: true
+ responses:
+ "200":
+ content:
+ text/html:
+ schema:
+ type: string
+ description: OK - CSP compatibility successfully completed.
+ "400":
+ content:
+ application/json:
+ schema:
+ $ref: '#/components/schemas/error'
+ description: malformed request
+ "500":
+ content:
+ application/json:
+ schema:
+ $ref: '#/components/schemas/error'
+ description: internal error
components:
schemas:
error:
diff --git a/requirements.txt b/requirements.txt
index b5475e5c8b9a4ef6d17a7ee2173db6e95a7ffa72..f742a1c9723037135b891bb45f415ad1c3d68480 100644
--- a/requirements.txt
+++ b/requirements.txt
@@ -52,3 +52,5 @@ urllib3==1.26.14
uvicorn==0.20.0
Werkzeug==2.2.2
z3-solver==4.11.2.0
+tabulate==0.9.0
+pytest-xdist==3.3.1
\ No newline at end of file
diff --git a/tests/doml/v2.2/nginx_flags.doml b/tests/doml/v2.2/nginx_flags.doml
new file mode 100644
index 0000000000000000000000000000000000000000..0434ccafbde78f2ab03c62ff6048cd1d512a8f5e
--- /dev/null
+++ b/tests/doml/v2.2/nginx_flags.doml
@@ -0,0 +1,140 @@
+doml nginx_func_req
+version "v2.2"
+
+application app {
+
+ software_component nginx {
+ properties {
+ source_code="/usr/share/nginx/html/index.html";
+ }
+ }
+}
+
+infrastructure infra {
+
+ vm_image vm_img {
+ generates vm1
+ image "ami-xxxxxxxxxxxxxxxxx"
+ }
+
+ net vpc {
+ cidr "/24"
+ protocol "tcp/ip"
+ subnet vpc_subnet {
+ cidr "/24"
+ protocol "tcp/ip"
+ }
+ }
+
+ security_group sg {
+ egress icmp {
+ from_port -1
+ to_port -1
+ protocol "icmp"
+ cidr ["0.0.0.0/0"]
+ }
+ ingress http {
+ from_port 80
+ to_port 80
+ protocol "tcp"
+ cidr ["0.0.0.0/0"]
+ }
+ ingress https {
+ from_port 443
+ to_port 443
+ protocol "tcp"
+ cidr ["0.0.0.0/0"]
+ }
+ ingress ssh {
+ from_port 22
+ to_port 22
+ protocol "tcp"
+ cidr ["0.0.0.0/0"]
+ }
+ ifaces i1
+ }
+
+ key_pair ssh_key {
+ user "ec2-user"
+ keyfile "/tmp/ssh_key_file"
+ algorithm "RSA"
+ bits 4096
+ }
+
+ autoscale_group ag {
+ vm vm1 {
+ iface i1 {
+ address "10.0.0.1"
+ belongs_to vpc
+ security sg
+ }
+ credentials ssh_key
+ loc {
+ region "eu-central-1"
+ }
+ }
+ }
+}
+
+deployment conf {
+ nginx -> vm1
+}
+
+active deployment conf
+
+concretizations {
+ concrete_infrastructure con_infra {
+ provider aws {
+ vm ec2_vm {
+ properties {
+ vm_name = "nginx-host";
+ instance_type = "t2.micro";
+ ssh_key_name = "demo-key";
+ ec2_role_name = "demo-ec2-role";
+ }
+ maps vm1
+ }
+
+ vm_image concrete_vm_image {
+ maps vm_img
+ }
+
+ net concrete_net {
+ properties {
+ vm_name = "nginx-host";
+ }
+ maps vpc
+ }
+ }
+ }
+ active con_infra
+}
+
+optimization opt {
+ objectives {
+ "cost" => min
+ "availability" => max
+ }
+ nonfunctional_requirements {
+ req1 "Cost <= 70.0" max 70.0 => "cost";
+ req2 "Availability >= 66.5%" min 66.5 => "availability";
+ }
+}
+
+functional_requirements {
+req_ext ```
+%IGNORE vm_has_iface
+%CHECK enforce_os_on_vm
+%CSP
+- "VM must have iface and iface is connected to network"
+ vm is class abstract.VirtualMachine
+ and
+ not exists iface, net (
+ vm has abstract.ComputingNode.ifaces iface
+ and
+ iface has abstract.NetworkInterface.belongsTo net
+
+ )
+ error: "TEST ERROR"
+
+ ```;}
diff --git a/tests/doml/v2.2/nginx_flags.domlx b/tests/doml/v2.2/nginx_flags.domlx
new file mode 100644
index 0000000000000000000000000000000000000000..740cac9ced98989998d29b322f5ac446612042f4
--- /dev/null
+++ b/tests/doml/v2.2/nginx_flags.domlx
@@ -0,0 +1,59 @@
+<?xml version="1.0" encoding="ASCII"?>
+<commons:DOMLModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:app="http://www.piacere-project.eu/doml/application" xmlns:commons="http://www.piacere-project.eu/doml/commons" xmlns:infra="http://www.piacere-project.eu/doml/infrastructure" xmlns:optimization="http://www.piacere-project.eu/doml/optimization" name="nginx_func_req" version="v2.2" activeConfiguration="//@configurations.0" activeInfrastructure="//@concretizations.0">
+ <application name="app">
+ <components xsi:type="app:SoftwareComponent" name="nginx">
+ <annotations xsi:type="commons:SProperty" key="source_code" value="/usr/share/nginx/html/index.html"/>
+ </components>
+ </application>
+ <infrastructure name="infra">
+ <generators xsi:type="infra:VMImage" name="vm_img" uri="ami-xxxxxxxxxxxxxxxxx" kind="IMAGE" generatedVMs="//@infrastructure/@groups.0/@machineDefinition"/>
+ <credentials xsi:type="commons:KeyPair" name="ssh_key" user="ec2-user" keyfile="/tmp/ssh_key_file" algorithm="RSA" bits="4096"/>
+ <groups xsi:type="infra:AutoScalingGroup" name="ag">
+ <machineDefinition name="vm1" credentials="//@infrastructure/@credentials.0" generatedFrom="//@infrastructure/@generators.0">
+ <ifaces name="i1" endPoint="10.0.0.1" belongsTo="//@infrastructure/@networks.0" associated="//@infrastructure/@securityGroups.0"/>
+ <location region="eu-central-1"/>
+ </machineDefinition>
+ </groups>
+ <securityGroups name="sg" ifaces="//@infrastructure/@groups.0/@machineDefinition/@ifaces.0">
+ <rules name="icmp" protocol="icmp" fromPort="-1" toPort="-1">
+ <cidr>0.0.0.0/0</cidr>
+ </rules>
+ <rules name="http" kind="INGRESS" protocol="tcp" fromPort="80" toPort="80">
+ <cidr>0.0.0.0/0</cidr>
+ </rules>
+ <rules name="https" kind="INGRESS" protocol="tcp" fromPort="443" toPort="443">
+ <cidr>0.0.0.0/0</cidr>
+ </rules>
+ <rules name="ssh" kind="INGRESS" protocol="tcp" fromPort="22" toPort="22">
+ <cidr>0.0.0.0/0</cidr>
+ </rules>
+ </securityGroups>
+ <networks name="vpc" protocol="tcp/ip" addressRange="/24" connectedIfaces="//@infrastructure/@groups.0/@machineDefinition/@ifaces.0">
+ <subnets name="vpc_subnet" protocol="tcp/ip" addressRange="/24"/>
+ </networks>
+ </infrastructure>
+ <concretizations name="con_infra">
+ <providers name="aws">
+ <vms name="ec2_vm" maps="//@infrastructure/@groups.0/@machineDefinition">
+ <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/>
+ <annotations xsi:type="commons:SProperty" key="instance_type" value="t2.micro"/>
+ <annotations xsi:type="commons:SProperty" key="ssh_key_name" value="demo-key"/>
+ <annotations xsi:type="commons:SProperty" key="ec2_role_name" value="demo-ec2-role"/>
+ </vms>
+ <vmImages name="concrete_vm_image" maps="//@infrastructure/@generators.0"/>
+ <networks name="concrete_net" maps="//@infrastructure/@networks.0">
+ <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/>
+ </networks>
+ </providers>
+ </concretizations>
+ <optimization name="opt">
+ <objectives xsi:type="optimization:MeasurableObjective" kind="min" property="cost"/>
+ <objectives xsi:type="optimization:MeasurableObjective" kind="max" property="availability"/>
+ <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req1" description="Cost <= 70.0" property="cost" max="70.0"/>
+ <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req2" description="Availability >= 66.5%" property="availability" min="66.5"/>
+ </optimization>
+ <configurations name="conf">
+ <deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/>
+ </configurations>
+ <functionalRequirements name="req_ext" description="```
%IGNORE vm_has_iface
%CHECK enforce_os_on_vm
%CSP
- "VM must have iface and iface is connected to network"
	vm is class abstract.VirtualMachine
	and
	not exists iface, net (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 
 )
 error: "TEST ERROR"
 
 ```"/>
+</commons:DOMLModel>
diff --git a/tests/test_modelchecker.py b/tests/test_modelchecker.py
new file mode 100644
index 0000000000000000000000000000000000000000..1881918a7844d898635fa070cd2bf35e5cff107e
--- /dev/null
+++ b/tests/test_modelchecker.py
@@ -0,0 +1,6 @@
+from mc_openapi.doml_mc import init_model, verify_model
+
+def setup(src, ver):
+ dmc = init_model(src, ver)
+ verify_model(dmc)
+