Emit more user-friendly error messages.

mc_openapi/doml_mc/common_reqs.py

+from typing import Optional
+
 from z3 import (
     Const, Consts, ExprRef,
-    Exists, And, Or, Not
+    Exists, And, Or, Not,
+    Solver, ModelRef
 )
 
 from .imc import (
     SMTEncoding, SMTSorts, Requirement, RequirementStore
 )
+from .intermediate_model.doml_element import IntermediateModel
 
 
 def get_consts(smtsorts: SMTSorts, consts: list[str]) -> list[ExprRef]:
     return Consts(" ".join(consts), smtsorts.element_sort)
 
 
+# Assertions
+
 def vm_iface(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
     vm, iface = get_consts(smtsorts, ["vm", "iface"])
     return And(
@@ -216,15 +222,96 @@ def all_concrete_map_something(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprR
     )
 
 
+# Error Descriptions
+
+def get_user_friendly_name(
+    intermediate_model: IntermediateModel,
+    model: ModelRef,
+    const: ExprRef
+) -> Optional[str]:
+    z3_elem = model[const]
+    if z3_elem is not None:
+        im_elem = intermediate_model.get(str(z3_elem))
+        if im_elem is not None:
+            return im_elem.user_friendly_name
+    return None
+
+
+def ed_vm_iface(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    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 connected to no network interface."
+    else:
+        return "A virtual machine is connected to no network interface."
+
+
+def ed_software_package_iface_net(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    asc_consumer, asc_exposer, siface = get_consts(
+        smtsorts,
+        ["asc_consumer", "asc_exposer", "siface"]
+    )
+    model = solver.model()
+    asc_consumer_name = get_user_friendly_name(intermediate_model, model, asc_consumer)
+    asc_exposer_name = get_user_friendly_name(intermediate_model, model, asc_exposer)
+    siface_name = get_user_friendly_name(intermediate_model, model, siface)
+    if asc_consumer_name and asc_exposer_name and siface_name:
+        return (
+            f"Software components '{asc_consumer_name}' and '{asc_exposer_name}' "
+            f"are supposed to communicate through interface '{siface_name}', "
+            "but they are deployed to nodes that cannot communicate through a common network."
+        )
+    else:
+        return "A software package is deployed on a node that has no access to an interface it consumes."
+
+
+def ed_iface_uniq(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    ni1, ni2 = get_consts(smtsorts, ["ni1", "ni2"])
+    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."
+    else:
+        return "Two network interfaces share the same IP address."
+
+
+def ed_all_SoftwareComponents_deployed(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    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."
+    else:
+        return "A software component has not been deployed to any node."
+
+
+def ed_all_infrastructure_elements_deployed(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    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}' has not been mapped to any element in the active concretization."
+    else:
+        return "An abstract infrastructure element has not been mapped to any element in the active concretization."
+
+
+def ed_all_concrete_map_something(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+    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 mapped to no abstract infrastructure element."
+    else:
+        return "A concrete infrastructure element is mapped to no abstract infrastructure element."
+
+
 CommonRequirements = RequirementStore(
     [
         Requirement(*rt) for rt in [
-            (vm_iface, "vm_iface", "All virtual machines must be connected to at least one network interface.", "A virtual machine is connected to no network interface."),
-            (software_package_iface_net, "software_package_iface_net", "All software packages can see the interfaces they need through a common network.", "A software package is deployed on a node that has no access to an interface it consumes."),
-            (iface_uniq, "iface_uniq", "There are no duplicated interfaces.", "There is a duplicated interface."),
-            (all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed", "All software components have been deployed to some node.", "A software component has not been deployed to any node."),
-            (all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed", "All abstract infrastructure elements are mapped to an element in the active concretization.", "An abstract infrastructure element has not been mapped to any element in the active concretization."),
-            (all_concrete_map_something, "all_concrete_map_something", "All elements in the active concretization are mapped to some abstract infrastructure element.", "A concrete infrastructure element is mapped to no abstract infrastructure element.")
+            (vm_iface, "vm_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 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),
+            (all_concrete_map_something, "all_concrete_map_something", "All elements in the active concretization are mapped to some abstract infrastructure element.", ed_all_concrete_map_something)
         ]
     ]
 )

mc_openapi/doml_mc/consistency_reqs.py

@@ -57,7 +57,7 @@ def get_attribute_type_reqs(mm: MetaModel) -> RequirementStore:
                     req_assertion,
                     f"attribute_st_types {cname}::{mm_attr.name}",
                     f"Attribute {mm_attr.name} from class {cname} must have type {mm_attr.type}.",
-                    f"Attribute {mm_attr.name} from class {cname} has a type different from {mm_attr.type}.",
+                    lambda _s, _m, _i: f"Attribute {mm_attr.name} from class {cname} has a type different from {mm_attr.type}.",
                 )
             )
     return RequirementStore(reqs)
@@ -99,7 +99,7 @@ def get_attribute_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
                         req_assertion_lb,
                         f"attribute_mult_lb {cname}::{mm_attr.name}",
                         f"Attribute {mm_attr.name} from class {cname} must have at least one value.",
-                        f"Mandatory attribute {mm_attr.name} from class {cname} has no value.",
+                        lambda _s, _m, _i: f"Mandatory attribute {mm_attr.name} from class {cname} has no value.",
                     )
                 )
             if ub == "1":
@@ -108,7 +108,7 @@ def get_attribute_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
                         req_assertion_ub,
                         f"attribute_mult_ub {cname}::{mm_attr.name}",
                         f"Attribute {mm_attr.name} from class {cname} must have at most one value.",
-                        f"Attribute {mm_attr.name} from class {cname} has more than one value.",
+                        lambda _s, _m, _i: f"Attribute {mm_attr.name} from class {cname} has more than one value.",
                     )
                 )
     return RequirementStore(reqs)
@@ -140,7 +140,7 @@ def get_association_type_reqs(mm: MetaModel) -> RequirementStore:
                     req_assertion,
                     f"association_st_classes {cname}::{mm_assoc.name}",
                     f"Association {mm_assoc.name} from class {cname} must target class {mm_assoc.class_}.",
-                    f"Association {mm_assoc.name} from class {cname} has a class different from {mm_assoc.class_}.",
+                    lambda _s, _m, _i: f"Association {mm_assoc.name} from class {cname} has a class different from {mm_assoc.class_}.",
                 )
             )
     return RequirementStore(reqs)
@@ -179,7 +179,7 @@ def get_association_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
                         req_assertion_lb,
                         f"association_mult_lb {cname}::{mm_assoc.name}",
                         f"Association {mm_assoc.name} from class {cname} must have at least one target.",
-                        f"Mandatory association {mm_assoc.name} is missing from an element of class {cname}.",
+                        lambda _s, _m, _i: f"Mandatory association {mm_assoc.name} is missing from an element of class {cname}.",
                     )
                 )
             if ub == "1":
@@ -188,7 +188,7 @@ def get_association_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
                         req_assertion_ub,
                         f"association_mult_ub {cname}::{mm_assoc.name}",
                         f"Association {mm_assoc.name} from class {cname} must have at most one target.",
-                        f"Association {mm_assoc.name} has more than one target in an element of class {cname}.",
+                        lambda _s, _m, _i: f"Association {mm_assoc.name} has more than one target in an element of class {cname}.",
                     )
                 )
     return RequirementStore(reqs)
@@ -212,7 +212,7 @@ def get_inverse_association_reqs(inv_assoc: list[tuple[str, str]]) -> Requiremen
                 req_assertion,
                 f"association_inverse {an1} {an2}",
                 f"Association {an1} must be the inverse of {an2}.",
-                f"Association {an1} is not the inverse of {an2}.",
+                lambda _s, _m, _i: f"Association {an1} is not the inverse of {an2}.",
             )
         )
     return RequirementStore(reqs)

mc_openapi/doml_mc/imc.py

@@ -2,7 +2,7 @@ from collections.abc import Callable
 from dataclasses import dataclass
 
 from z3 import (
-    Context, FuncDeclRef, Solver, ExprRef, SortRef, DatatypeSortRef
+    Context, FuncDeclRef, Solver, ExprRef, SortRef, DatatypeSortRef, sat
 )
 
 from .intermediate_model.doml_element import IntermediateModel
@@ -46,10 +46,10 @@ class SMTSorts:
 
 @dataclass
 class Requirement:
-    assert_callable: Callable[[SMTEncoding, SMTSorts], list[ExprRef]]
+    assert_callable: Callable[[SMTEncoding, SMTSorts], ExprRef]
     assert_name: str
     description: str
-    error_description: str
+    error_description: Callable[[Solver, SMTSorts, IntermediateModel], str]
 
 
 class RequirementStore:
@@ -153,7 +153,11 @@ class IntermediateModelChecker:
                 req.assert_name
             )
             res = self.solver.check()
+            results.append((
+                MCResult.from_z3result(res, flipped=True),
+                req.error_description(self.solver, self.smt_sorts, self.intermediate_model)
+                if res == sat else ""
+            ))
             self.solver.pop()
-            results.append((MCResult.from_z3result(res, flipped=True), req.error_description))
 
         return MCResults(results)

mc_openapi/doml_mc/intermediate_model/doml_element.py

-from typing import Union
+from typing import Union, Optional
 from dataclasses import dataclass
 
 from .metamodel import (
@@ -21,6 +21,7 @@ class DOMLElement:
     # e.g., `"application_SoftwarePackage::isPersistent"`.
     attributes: Attributes
     associations: Associations
+    user_friendly_name: Optional[str]
 
 
 IntermediateModel = dict[str, "DOMLElement"]

mc_openapi/doml_mc/xmi_parser/ecore.py

 import sys
-from typing import Callable
+from typing import Callable, Optional
 
 from pyecore.ecore import EEnumLiteral, EObject, EOrderedSet, EClass
 
@@ -89,14 +89,13 @@ class ELayerParser:
         assocs = parse_associations(raw_assocs, mm_class, self.mm)
 
         self.im[name] = DOMLElement(
-            id_=name, class_=mm_class, attributes=attrs, associations=assocs
+            id_=name, class_=mm_class, attributes=attrs, associations=assocs,
+            user_friendly_name=ELayerParser.get_user_friendly_name(doc)
         )
         return name
 
-    def getUniqueName(self):
-        name = f"__generated_name__{self.nextUniqueId}"
-        self.nextUniqueId += 1
-        return name
-
     def mangle_eclass_name(eClass: EClass) -> str:
         return eClass.ePackage.name + "_" + eClass.name
+
+    def get_user_friendly_name(doc: EObject) -> Optional[str]:
+        return getattr(doc, "name", None)

tests/test_mc_openapi.py

@@ -30,7 +30,16 @@ def test_post_faas_sat():
 
 
 def test_post_common_reqs():
-    for req in CommonRequirements.get_all_requirements():
+    check_strings = [
+        "is connected to no network interface.",
+        "but they are deployed to nodes that cannot communicate through a common network.",
+        "share the same IP address.",
+        "is not deployed to any abstract infrastructure node.",
+        "has not been mapped to any element in the active concretization.",
+        "is mapped to no abstract infrastructure element."
+    ]
+
+    for req, err_desc in zip(CommonRequirements.get_all_requirements(), check_strings):
         with open(f"tests/doml/nginx-openstack_v2.0_wrong_{req.assert_name}.domlx", "r") as f:
             doml = f.read()
 
@@ -39,4 +48,4 @@ def test_post_common_reqs():
         assert r.status_code == requests.codes.ok
         assert payload["result"] is not None
         assert payload["result"] == "unsat"
-        assert req.error_description in payload["description"]
+        assert err_desc in payload["description"]