diff --git a/mc_openapi/doml_mc/common_reqs.py b/mc_openapi/doml_mc/common_reqs.py
index 2fde383543f5acc36ad67926bf3857b27daab8c2..6962e79f668bebba84140c9b8de08124147cc888 100644
--- a/mc_openapi/doml_mc/common_reqs.py
+++ b/mc_openapi/doml_mc/common_reqs.py
@@ -1,17 +1,23 @@
+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)
]
]
)
diff --git a/mc_openapi/doml_mc/consistency_reqs.py b/mc_openapi/doml_mc/consistency_reqs.py
index ce9f2e805cdcb483a905ba943d05245fd35f0756..3b2bcdcf7afe02b7a8c056d74b6430a8b0c78e8d 100644
--- a/mc_openapi/doml_mc/consistency_reqs.py
+++ b/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)
diff --git a/mc_openapi/doml_mc/imc.py b/mc_openapi/doml_mc/imc.py
index 8efd89bdfd1a3e75eeb9f3981e933c2086331e0e..fb3ca02f46f7b0099d07fc62d5fea19709ef8bc0 100644
--- a/mc_openapi/doml_mc/imc.py
+++ b/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:
@@ -151,9 +151,13 @@ class IntermediateModelChecker:
self.solver.assert_and_track(
req.assert_callable(self.smt_encoding, self.smt_sorts),
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)
diff --git a/mc_openapi/doml_mc/intermediate_model/doml_element.py b/mc_openapi/doml_mc/intermediate_model/doml_element.py
index be2447bb5484d40ec175977165df06a63a719a29..d5caa8e8d1bcdf5c05ca2e78dcda14fbaf815023 100644
--- a/mc_openapi/doml_mc/intermediate_model/doml_element.py
+++ b/mc_openapi/doml_mc/intermediate_model/doml_element.py
@@ -1,4 +1,4 @@
-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"]
diff --git a/mc_openapi/doml_mc/xmi_parser/ecore.py b/mc_openapi/doml_mc/xmi_parser/ecore.py
index 022290ada8381df89d77cf8f4ff558a8f38086f6..224128cc01a7174c8321418bea4f708368e5eb70 100644
--- a/mc_openapi/doml_mc/xmi_parser/ecore.py
+++ b/mc_openapi/doml_mc/xmi_parser/ecore.py
@@ -1,5 +1,5 @@
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)
diff --git a/tests/test_mc_openapi.py b/tests/test_mc_openapi.py
index 50031433579146f43e1801b3cfa41a170eb34a80..097754fde225416145c8e507460fee9948283dbb 100644
--- a/tests/test_mc_openapi.py
+++ b/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"]