refactor each requirement into a file

mc_openapi/__init__.py

-__version__ = '2.4.0'
+__version__ = '2.4.1'

mc_openapi/doml_mc/builtin_requirements/__init__.py

+CELEMS_V2_0 = [
+    ("infrastructure_VirtualMachine", "concrete_RuntimeProvider::vms", "concrete_VirtualMachine::maps"),
+    ("infrastructure_VMImage", "concrete_RuntimeProvider::vmImages", "concrete_VMImage::maps"),
+    ("infrastructure_Network", "concrete_RuntimeProvider::networks", "concrete_Network::maps"),
+    ("infrastructure_Storage", "concrete_RuntimeProvider::storages", "concrete_Storage::maps"),
+    ("infrastructure_FunctionAsAService", "concrete_RuntimeProvider::faas","concrete_FunctionAsAService::maps"),
+    ("infrastructure_ComputingGroup", "concrete_RuntimeProvider::group","concrete_ComputingGroup::maps")
+]
+
+from .vm_has_iface import VM_HAS_IFACE, VM_HAS_IFACE_V2_3
+from .software_package_iface_net import SOFTWARE_PACKAGE_IFACE_NET, SOFTWARE_PACKAGE_IFACE_NET_V2_1, SOFTWARE_PACKAGE_IFACE_NET_V2_3
+from .iface_uniq import IFACE_UNIQ
+from .all_software_components_deployed import ALL_SOFTWARE_COMPONENTS_DEPLOYED
+from .all_infrastructure_elements_deployed import ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED
+from .all_concrete_maps_something import ALL_CONCRETE_MAP_SOMETHING
+from .security_group_must_have_iface import SECURITY_GROUP_MUST_HAVE_IFACE
+
+__ALL__ = [
+    VM_HAS_IFACE,
+    VM_HAS_IFACE_V2_3,
+    SOFTWARE_PACKAGE_IFACE_NET,
+    SOFTWARE_PACKAGE_IFACE_NET_V2_1,
+    SOFTWARE_PACKAGE_IFACE_NET_V2_3,
+    IFACE_UNIQ,
+    ALL_SOFTWARE_COMPONENTS_DEPLOYED,
+    ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
+    ALL_CONCRETE_MAP_SOMETHING,
+    SECURITY_GROUP_MUST_HAVE_IFACE
+]
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/all_concrete_maps_something.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+from . import CELEMS_V2_0
+
+# All elements in the active concretization are mapped to some abstract infrastructure element.
+
+def all_concrete_map_something(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    def checkOneClass(ielem, provider, celem, providerAssoc, celemAssoc):
+        return And(
+            smtenc.association_rel(
+                provider, smtenc.associations[providerAssoc], celem),
+            Not(
+                Exists(
+                    [ielem],
+                    smtenc.association_rel(
+                        celem, smtenc.associations[celemAssoc], ielem)
+                )
+            )
+        )
+
+    ielem, concr, provider, celem = Consts(
+       "ielem concr provider celem", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            concr) == smtenc.classes["concrete_ConcreteInfrastructure"],
+        smtenc.association_rel(
+            concr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
+        Or(
+            *(
+                checkOneClass(
+                    ielem, provider, celem,
+                    providerAssoc, celemAssoc
+                )
+                for _, providerAssoc, celemAssoc in CELEMS_V2_0
+            )
+        )
+    )
+
+
+def ed_all_concrete_map_something(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        celem = Const("celem", smtsorts.element_sort)
+        celem_name = get_user_friendly_name(
+            intermediate_model, solver.model(), celem)
+        if celem_name:
+            return f"Concrete infrastructure element '{celem_name}' is not mapped to any abstract infrastructure element."
+    except:
+        return "A concrete infrastructure element is not mapped to any abstract infrastructure element."
+
+MSG = "All elements in the active concretization are mapped to some abstract infrastructure element."
+
+ALL_CONCRETE_MAP_SOMETHING = (
+    all_concrete_map_something,
+    "all_concrete_map_something",
+    MSG,
+    ed_all_concrete_map_something
+)
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+from . import CELEMS_V2_0
+
+# Provider > elements generated by IOP only have "commons_DOMLElement::annotations" as an association
+# and do not have maps. Also networks are not generated by the IOP. But they are the same class
+# (concrete_infrastructure), so I can't make distinction.
+
+def all_infrastructure_elements_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    """Checks:
+        - infrastructure_VMImage
+        - infrastructure_Network
+        - infrastructure_Storage
+        - infrastructure_FunctionAsAService
+        - infrastructure_ComputingGroup
+    """
+    def checkOneClass(ielem, cinfr, provider, celem, ielemClass, providerAssoc, celemAssoc):
+        return And(
+            smtenc.element_class_fun(ielem) == smtenc.classes[ielemClass],
+            Not(
+                Exists(
+                    [provider, celem],
+                    And(
+                        smtenc.association_rel(
+                            cinfr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
+                        smtenc.association_rel(
+                            provider, smtenc.associations[providerAssoc], celem),
+                        smtenc.association_rel(
+                            celem, smtenc.associations[celemAssoc], ielem)
+                    )
+                )
+            )
+        )
+
+    ielem, concr, provider, celem, asg = Consts("ielem concr provider celem asg", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            concr) == smtenc.classes["concrete_ConcreteInfrastructure"],
+        Or(
+            *(
+                checkOneClass(
+                    ielem, concr, provider, celem,
+                    ielemClass, providerAssoc, celemAssoc
+                ) 
+                for ielemClass, providerAssoc, celemAssoc in CELEMS_V2_0
+                if ielemClass != 'infrastructure_VirtualMachine' # handle special case separately below
+            ),
+        )
+    )
+
+
+def ed_all_infrastructure_elements_deployed(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        ielem = Const("ielem", smtsorts.element_sort)
+        ielem_name = get_user_friendly_name(
+            intermediate_model, solver.model(), ielem)
+        if ielem_name:
+            return f"Abstract infrastructure element '{ielem_name}' is not mapped to any element in the active concretization."
+    except:
+        return "An abstract infrastructure element has is not mapped to any element in the active concretization."
+
+MSG = "All abstract infrastructure elements are mapped to an element in the active concretization."
+
+ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED = (
+    all_infrastructure_elements_deployed,
+    "all_infrastructure_elements_deployed",
+    MSG,
+    ed_all_infrastructure_elements_deployed
+)
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/all_software_components_deployed.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+
+# All software components have been deployed to some node.
+
+def all_software_components_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    sc, deployment, ielem = Consts("sc deployment ielem", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            sc) == smtenc.classes["application_SoftwareComponent"],
+        Not(
+            Exists(
+                [deployment, ielem],
+                And(
+                    smtenc.association_rel(
+                        deployment, smtenc.associations["commons_Deployment::component"], sc),
+                    smtenc.association_rel(
+                        deployment, smtenc.associations["commons_Deployment::node"], ielem),
+                )
+            )
+        )
+    )
+
+def ed_all_software_components_deployed(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        sc = Const("sc", smtsorts.element_sort)
+        sc_name = get_user_friendly_name(
+            intermediate_model, solver.model(), sc)
+        if sc_name:
+            return f"Software component '{sc_name}' is not deployed to any abstract infrastructure node."
+    except:
+        return "A software component is not deployed to any abstract infrastructure node."
+
+MSG = "All software components have been deployed to some node."
+
+ALL_SOFTWARE_COMPONENTS_DEPLOYED = (
+    all_software_components_deployed,
+    "all_software_components_deployed",
+    MSG,
+    ed_all_software_components_deployed
+)
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/iface_uniq.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+
+# There are no duplicated interfaces.
+def iface_uniq(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    endPointAttr = smtenc.attributes["infrastructure_NetworkInterface::endPoint"]
+    ni1, ni2 = Consts("ni1 ni2", smtsorts.element_sort)
+    value = Const("value", smtsorts.attr_data_sort)
+    return And(
+        smtenc.attribute_rel(ni1, endPointAttr, value),
+        smtenc.attribute_rel(ni2, endPointAttr, value),
+        ni1 != ni2,
+    )
+
+def ed_iface_uniq(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        ni1, ni2 = Consts("ni1 ni2", smtsorts.element_sort)
+        model = solver.model()
+        ni1_name = get_user_friendly_name(intermediate_model, model, ni1)
+        ni2_name = get_user_friendly_name(intermediate_model, model, ni2)
+        if ni1_name and ni2_name:
+            return f"Network interfaces '{ni1_name}' and '{ni2_name}' share the same IP address."
+    except:
+        return "Two network interfaces share the same IP address."
+
+MSG = "There are no duplicated interfaces."
+
+IFACE_UNIQ = (
+    iface_uniq,
+    "iface_uniq",
+    MSG,
+    ed_iface_uniq
+)
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/security_group_must_have_iface.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+
+# From DOML V2.3+:
+# The association between security groups and network interfaces can now be done only
+# in the security groups definition through the “ifaces” keyword (removed the "security"
+# keyword in the network interface definition)
+def security_group_must_have_iface(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    sg, iface = Consts("sg iface", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            sg) == smtenc.classes["infrastructure_SecurityGroup"],
+        Not(Exists([iface],
+            smtenc.association_rel(
+                iface, smtenc.associations["infrastructure_NetworkInterface::associated"], sg)
+        ))
+    )
+
+def ed_security_group_must_have_iface(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        sg = Const("sg", smtsorts.element_sort)
+        sg_name = get_user_friendly_name(
+            intermediate_model, solver.model(), sg)
+        if sg_name:
+            return f"Security group '{sg_name}' is not associated with any network interface."
+    except:
+        return "A network interface doesn't belong to any security group, or a security group is not associated with any network interface."
+
+MSG = "All security group should be a associated to a network interface."
+
+SECURITY_GROUP_MUST_HAVE_IFACE = (
+    security_group_must_have_iface,
+    "security_group_must_have_iface",
+    MSG,
+    ed_security_group_must_have_iface
+)
\ No newline at end of file

mc_openapi/doml_mc/builtin_requirements/vm_has_iface.py

+from z3 import And, Const, Consts, Exists, ExprRef, Not, Or, Solver, Implies
+from mc_openapi.doml_mc.imc import Requirement, SMTEncoding, SMTSorts
+from mc_openapi.doml_mc.intermediate_model import DOMLVersion, IntermediateModel
+from mc_openapi.doml_mc.error_desc_helper import get_user_friendly_name
+
+
+def vm_has_iface(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    vm, iface = Consts("vm iface", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            vm) == smtenc.classes["infrastructure_VirtualMachine"],
+        Not(
+            Exists(
+                [iface],
+                smtenc.association_rel(
+                    vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], iface)
+            )
+        )
+    )
+
+def vm_has_iface_v2_3(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+    vm, iface = Consts("vm iface", smtsorts.element_sort)
+    return And(
+        smtenc.element_class_fun(
+            vm) == smtenc.classes["infrastructure_VirtualMachine"],
+        Not(
+            Exists(
+                [iface],
+                smtenc.association_rel(
+                    vm, smtenc.associations["infrastructure_Node::ifaces"], iface)
+            )
+        )
+    )
+
+def ed_vm_has_iface(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    try:
+        vm = Const("vm", smtsorts.element_sort)
+        vm_name = get_user_friendly_name(
+            intermediate_model, solver.model(), vm)
+        if vm_name:
+            return f"Virtual machine {vm_name} is not connected to any network interface."
+    except:
+        return "A virtual machine is not connected to any network interface."
+    
+MSG = "All virtual machines must be connected to at least one network interface."
+
+VM_HAS_IFACE = (
+    vm_has_iface, 
+    "vm_has_iface",
+    MSG,
+    ed_vm_has_iface
+)
+
+VM_HAS_IFACE_V2_3 = (
+    vm_has_iface_v2_3,
+    "vm_has_iface",
+    MSG,
+    ed_vm_has_iface
+)
\ No newline at end of file

mc_openapi/doml_mc/imc.py

@@ -163,11 +163,12 @@ class IntermediateModelChecker:
                 req.assert_name
             )
             res = self.solver.check()
-            req_src, req_fn = req.error_description
+            req_type, req_err_desc_fn = req.error_description
+            req_is_sat = MCResult.from_z3result(res, flipped=req.flipped)
             results.append((
-                MCResult.from_z3result(res, flipped=req.flipped),
-                req_src,
-                req_fn(self.solver, self.smt_sorts, self.intermediate_model)
+                req_is_sat,
+                req_type,
+                req_err_desc_fn(self.solver, self.smt_sorts, self.intermediate_model) if req_is_sat else ""
                 # if res == sat else "" # not needed since we're try/catching model() errors
                 # in each requirement now
             ))

requirements.txt

@@ -2,7 +2,7 @@ tabulate
 connexion
 connexion[swagger-ui]
 joblib
-z3-solver
+z3-solver==4.11.* # Else it deadlocks the MC somehow
 networkx
 lxml
 pyecore

tests/test_modelchecker.py

@@ -19,16 +19,17 @@ def test_domlx_models_by_version(subtests):
             with open(domlx, "rb") as f:
                 domlx_file = f.read()
                 assert_ver = DOMLVersion.get(doml_ver)
-                res = run(domlx_file, assert_ver)
+                assert_result = None
                 try:
                     assert_result = OUTPUT[doml_ver][domlx.name]
                     i += 1
                 except:
                     pass
-            if assert_result:
-                with subtests.test(msg=f"{doml_ver}/{domlx.name}", i=i):
-                        assert assert_result == res['result'].name
-                        assert assert_ver.name == res['doml_version']
+                if assert_result:
+                    with subtests.test(msg=f"{doml_ver}/{domlx.name}", i=i):
+                            res = run(domlx_file, assert_ver)
+                            assert assert_result == res['result'].name
+                            assert assert_ver.name == res['doml_version']
 
 OUTPUT = {
     'v2.0': {