diff --git a/mc_openapi/__init__.py b/mc_openapi/__init__.py
index ba9b91332bd3ec3a25de8bc3fac20484f006fedd..5cd7abf832ef7fb7cad1db3c2f1640f87cbb35a5 100644
--- a/mc_openapi/__init__.py
+++ b/mc_openapi/__init__.py
@@ -1 +1 @@
-__version__ = '2.4.0'
+__version__ = '2.4.1'
diff --git a/mc_openapi/doml_mc/builtin_requirements/__init__.py b/mc_openapi/doml_mc/builtin_requirements/__init__.py
new file mode 100644
index 0000000000000000000000000000000000000000..e5d2d8dec45778cc6667e45b8eb4b23ba965bbeb
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/__init__.py
@@ -0,0 +1,29 @@
+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
diff --git a/mc_openapi/doml_mc/builtin_requirements/all_concrete_maps_something.py b/mc_openapi/doml_mc/builtin_requirements/all_concrete_maps_something.py
new file mode 100644
index 0000000000000000000000000000000000000000..18a571973dad731f86236deca6c5f2048083be70
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/all_concrete_maps_something.py
@@ -0,0 +1,59 @@
+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
diff --git a/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py b/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py
new file mode 100644
index 0000000000000000000000000000000000000000..05a1bbd1556a174365a0c167c5e1c0abbd4996a4
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/all_infrastructure_elements_deployed.py
@@ -0,0 +1,71 @@
+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
diff --git a/mc_openapi/doml_mc/builtin_requirements/all_software_components_deployed.py b/mc_openapi/doml_mc/builtin_requirements/all_software_components_deployed.py
new file mode 100644
index 0000000000000000000000000000000000000000..a10d5025a6df3aa63107bf6393f107e8670b4813
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/all_software_components_deployed.py
@@ -0,0 +1,43 @@
+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
diff --git a/mc_openapi/doml_mc/builtin_requirements/iface_uniq.py b/mc_openapi/doml_mc/builtin_requirements/iface_uniq.py
new file mode 100644
index 0000000000000000000000000000000000000000..669c8d0dedaa09b8673db74cd7d21d16bdb7cd62
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/iface_uniq.py
@@ -0,0 +1,35 @@
+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
diff --git a/mc_openapi/doml_mc/builtin_requirements/security_group_must_have_iface.py b/mc_openapi/doml_mc/builtin_requirements/security_group_must_have_iface.py
new file mode 100644
index 0000000000000000000000000000000000000000..e18ec59597bfac1797e261793f3d6f2d26283e07
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/security_group_must_have_iface.py
@@ -0,0 +1,38 @@
+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
diff --git a/mc_openapi/doml_mc/builtin_requirements/software_package_iface_net.py b/mc_openapi/doml_mc/builtin_requirements/software_package_iface_net.py
new file mode 100644
index 0000000000000000000000000000000000000000..e4ab9d07d93656b1da46fe4ad31d03656003a972
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/software_package_iface_net.py
@@ -0,0 +1,540 @@
+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 packages can see the interfaces they need through a common network.
+
+def software_package_iface_net(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+ asc_consumer, asc_exposer, siface, net, net_iface, cnode, cdeployment, enode, edeployment, vm, csubnet, esubnet = Consts(
+ "asc_consumer asc_exposer siface net net_iface cnode cdeployment enode edeployment vm csubnet esubnet", smtsorts.element_sort
+ )
+ return And(
+ smtenc.association_rel(
+ asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
+ smtenc.association_rel(
+ asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
+ Not(
+ Or(
+ Exists(
+ [cdeployment, cnode, edeployment, enode, net],
+ And(
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
+ Exists(
+ [vm, net_iface],
+ Or(
+ And( # asc_consumer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Container::hosts"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ )
+ ),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::node"], enode),
+ Exists(
+ [vm, net_iface],
+ Or(
+ And( # asc_exposer is deployed on a component with an interface in network n
+ # ASC_EXPLORER > CN > IFACE > NET
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
+ # ASC_EXPOSER > CONTAINER > CN > IFACE > NET
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Container::hosts"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ # ASC_EXPLORER > ASG > CN > IFACE > NET
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ )
+ )
+ )
+ ), # OR
+ Exists(
+ [cdeployment, cnode, edeployment, enode, csubnet, esubnet],
+ And(
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
+ Or(
+ smtenc.association_rel(
+ csubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], esubnet),
+ smtenc.association_rel(
+ esubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], csubnet),
+ ),
+ Exists(
+ [vm, net_iface],
+ Or(
+ And( # asc_consumer is deployed on a component with an interface in network n
+ # ASC_CONSUMER > CN > IFACE > csubnet
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
+ # ASC_CONSUMER > CONTAINER > CN > IFACE > csubnet
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Container::hosts"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ # ASC_CONSUMER > ASG > CN > IFACE > csubnet
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ )
+ ),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::node"], enode),
+ Exists(
+ [vm, net_iface],
+ Or(
+ And( # asc_exposer is deployed on a component with an interface in network n
+ # ASC_EXPOSER > CN > IFACE > esubnet
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ ),
+ And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
+ # ASC_EXPOSER > CONTAINER > CN > IFACE > esubnet
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Container::hosts"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ ),
+ And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ # ASC_EXPLORER > ASG > CN > IFACE > esubnet
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+
+def software_package_iface_net_v2_1(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+ asc_consumer, asc_exposer, siface, net, net_iface, cnode, cdeployment, enode, edeployment, vm, cconf, csubnet, esubnet = Consts(
+ "asc_consumer asc_exposer siface net net_iface cnode cdeployment enode edeployment vm cconf csubnet esubnet", smtsorts.element_sort
+ )
+ return And(
+ smtenc.association_rel(
+ asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
+ smtenc.association_rel(
+ asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
+ Not(
+ Or(
+ Exists(
+ [cdeployment, cnode, edeployment, enode, net],
+ And(
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_consumer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ )
+ ),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::node"], enode),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_exposer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ )
+ )
+ )
+ ), # OR
+ Exists(
+ [cdeployment, cnode, edeployment, enode, csubnet, esubnet],
+ And(
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
+ Or(
+ smtenc.association_rel(
+ csubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], esubnet),
+ smtenc.association_rel(
+ esubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], csubnet),
+ ),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_consumer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ )
+ ),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::node"], enode),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_exposer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ ),
+ And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ ),
+ And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+
+def software_package_iface_net_v2_3(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
+ asc_consumer, asc_exposer, siface, net, net_iface, cnode, cdeployment, enode, edeployment, vm, cconf, csubnet, esubnet = Consts(
+ "asc_consumer asc_exposer siface net net_iface cnode cdeployment enode edeployment vm cconf csubnet esubnet", smtsorts.element_sort
+ )
+ return And(
+ smtenc.association_rel(
+ asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
+ smtenc.association_rel(
+ asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
+ Not(
+ Or(
+ Exists(
+ [cdeployment, cnode, edeployment, enode, net],
+ And(
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_consumer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ )
+ ),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::node"], enode),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_exposer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
+ ),
+ )
+ )
+ )
+ ), # OR
+ Exists(
+ [cdeployment, cnode, edeployment, enode, csubnet, esubnet],
+ And(
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
+ smtenc.association_rel(
+ cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
+ Or(
+ smtenc.association_rel(
+ csubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], esubnet),
+ smtenc.association_rel(
+ esubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], csubnet),
+ ),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_consumer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
+ ),
+ )
+ ),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
+ smtenc.association_rel(
+ edeployment, smtenc.associations["commons_Deployment::node"], enode),
+ Exists(
+ [vm, net_iface, cconf],
+ Or(
+ And( # asc_exposer is deployed on a component with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ ),
+ And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_Container::configs"], cconf),
+ smtenc.association_rel(
+ cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ ),
+ And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
+ smtenc.association_rel(
+ enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
+ smtenc.association_rel(
+ vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
+ smtenc.association_rel(
+ net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+ )
+
+
+def ed_software_package_iface_net(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
+ try:
+ asc_consumer, asc_exposer, siface = Consts(
+ "asc_consumer asc_exposer siface", smtsorts.element_sort
+ )
+ 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."
+ )
+ except:
+ return "A software package is deployed on a node that has no access to an interface it consumes."
+
+MSG = "All software packages can see the interfaces they need through a common network."
+
+SOFTWARE_PACKAGE_IFACE_NET = (
+ software_package_iface_net,
+ "software_package_iface_net",
+ MSG,
+ ed_software_package_iface_net
+)
+
+SOFTWARE_PACKAGE_IFACE_NET_V2_1 = (
+ software_package_iface_net_v2_1,
+ "software_package_iface_net",
+ MSG,
+ ed_software_package_iface_net
+)
+
+SOFTWARE_PACKAGE_IFACE_NET_V2_3 = (
+ software_package_iface_net_v2_3,
+ "software_package_iface_net",
+ MSG,
+ ed_software_package_iface_net
+)
\ No newline at end of file
diff --git a/mc_openapi/doml_mc/builtin_requirements/vm_has_iface.py b/mc_openapi/doml_mc/builtin_requirements/vm_has_iface.py
new file mode 100644
index 0000000000000000000000000000000000000000..bfb43d5d1051dd1d28f9f9b7d326f810d9273747
--- /dev/null
+++ b/mc_openapi/doml_mc/builtin_requirements/vm_has_iface.py
@@ -0,0 +1,59 @@
+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
diff --git a/mc_openapi/doml_mc/common_reqs.py b/mc_openapi/doml_mc/common_reqs.py
index 4d1dabba0bd16996c5c76e1ee3cddcfd615aeb1a..bab95408a9da6b5e3352b139511623e0f6102df1 100644
--- a/mc_openapi/doml_mc/common_reqs.py
+++ b/mc_openapi/doml_mc/common_reqs.py
@@ -1,927 +1,47 @@
-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
-from .intermediate_model import DOMLVersion, IntermediateModel
-
-
-def get_consts(smtsorts: SMTSorts, consts: list[str]) -> list[ExprRef]:
- return Consts(" ".join(consts), smtsorts.element_sort)
-
-
-# Assertions
-
-def vm_has_iface(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- vm, iface = get_consts(smtsorts, ["vm", "iface"])
- 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_iface_v2_3(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- vm, iface = get_consts(smtsorts, ["vm", "iface"])
- return And(
- smtenc.element_class_fun(
- vm) == smtenc.classes["infrastructure_VirtualMachine"],
- Not(
- Exists(
- [iface],
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], iface)
- )
- )
- )
-
-# All software packages can see the interfaces they need through a common network.
-
-
-def software_package_iface_net(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- asc_consumer, asc_exposer, siface, net, net_iface, cnode, cdeployment, enode, edeployment, vm, csubnet, esubnet = get_consts(
- smtsorts,
- ["asc_consumer", "asc_exposer", "siface", "net", "net_iface",
- "cnode", "cdeployment", "enode", "edeployment", "vm", "csubnet", "esubnet"]
- )
- return And(
- smtenc.association_rel(
- asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
- smtenc.association_rel(
- asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
- Not(
- Or(
- Exists(
- [cdeployment, cnode, edeployment, enode, net],
- And(
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
- Exists(
- [vm, net_iface],
- Or(
- And( # asc_consumer is deployed on a component with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Container::hosts"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- )
- ),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::node"], enode),
- Exists(
- [vm, net_iface],
- Or(
- And( # asc_exposer is deployed on a component with an interface in network n
- # ASC_EXPLORER > CN > IFACE > NET
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
- # ASC_EXPOSER > CONTAINER > CN > IFACE > NET
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Container::hosts"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
- # ASC_EXPLORER > ASG > CN > IFACE > NET
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- )
- )
- )
- ), # OR
- Exists(
- [cdeployment, cnode, edeployment, enode, csubnet, esubnet],
- And(
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
- Or(
- smtenc.association_rel(
- csubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], esubnet),
- smtenc.association_rel(
- esubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], csubnet),
- ),
- Exists(
- [vm, net_iface],
- Or(
- And( # asc_consumer is deployed on a component with an interface in network n
- # ASC_CONSUMER > CN > IFACE > csubnet
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
- # ASC_CONSUMER > CONTAINER > CN > IFACE > csubnet
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Container::hosts"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
- # ASC_CONSUMER > ASG > CN > IFACE > csubnet
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- )
- ),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::node"], enode),
- Exists(
- [vm, net_iface],
- Or(
- And( # asc_exposer is deployed on a component with an interface in network n
- # ASC_EXPOSER > CN > IFACE > esubnet
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- ),
- And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
- # ASC_EXPOSER > CONTAINER > CN > IFACE > esubnet
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Container::hosts"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- ),
- And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
- # ASC_EXPLORER > ASG > CN > IFACE > esubnet
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- )
- )
- )
- )
- )
- )
- )
- )
-
-
-def software_package_iface_net_v2_1(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- asc_consumer, asc_exposer, siface, net, net_iface, cnode, cdeployment, enode, edeployment, vm, cconf, csubnet, esubnet = get_consts(
- smtsorts,
- ["asc_consumer", "asc_exposer", "siface", "net", "net_iface",
- "cnode", "cdeployment", "enode", "edeployment", "vm", "cconf", "csubnet", "esubnet"]
- )
- return And(
- smtenc.association_rel(
- asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
- smtenc.association_rel(
- asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
- Not(
- Or(
- Exists(
- [cdeployment, cnode, edeployment, enode, net],
- And(
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_consumer is deployed on a component with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- )
- ),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::node"], enode),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_exposer is deployed on a component with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- )
- )
- )
- ), # OR
- Exists(
- [cdeployment, cnode, edeployment, enode, csubnet, esubnet],
- And(
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
- Or(
- smtenc.association_rel(
- csubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], esubnet),
- smtenc.association_rel(
- esubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], csubnet),
- ),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_consumer is deployed on a component with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- )
- ),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::node"], enode),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_exposer is deployed on a component with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- ),
- And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- ),
- And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- )
- )
- )
- )
- )
- )
- )
- )
-
-def software_package_iface_net_v2_3(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- asc_consumer, asc_exposer, siface, net, net_iface, cnode, cdeployment, enode, edeployment, vm, cconf, csubnet, esubnet = get_consts(
- smtsorts,
- ["asc_consumer", "asc_exposer", "siface", "net", "net_iface",
- "cnode", "cdeployment", "enode", "edeployment", "vm", "cconf", "csubnet", "esubnet"]
- )
- return And(
- smtenc.association_rel(
- asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
- smtenc.association_rel(
- asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
- Not(
- Or(
- Exists(
- [cdeployment, cnode, edeployment, enode, net],
- And(
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_consumer is deployed on a component with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- )
- ),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::node"], enode),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_exposer is deployed on a component with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
- ),
- )
- )
- )
- ), # OR
- Exists(
- [cdeployment, cnode, edeployment, enode, csubnet, esubnet],
- And(
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
- smtenc.association_rel(
- cdeployment, smtenc.associations["commons_Deployment::node"], cnode),
- Or(
- smtenc.association_rel(
- csubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], esubnet),
- smtenc.association_rel(
- esubnet, smtenc.associations["infrastructure_Subnet::connectedTo"], csubnet),
- ),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_consumer is deployed on a component with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- And( # asc_consumer is deployed on a container hosted in a VM with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- And( # asc_consumer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- cnode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], csubnet),
- ),
- )
- ),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
- smtenc.association_rel(
- edeployment, smtenc.associations["commons_Deployment::node"], enode),
- Exists(
- [vm, net_iface, cconf],
- Or(
- And( # asc_exposer is deployed on a component with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- ),
- And( # asc_exposer is deployed on a container hosted on a VM with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_Container::configs"], cconf),
- smtenc.association_rel(
- cconf, smtenc.associations["infrastructure_ContainerConfig::host"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- ),
- And( # asc_exposer is deployed on a VM in an AutoScalingGroup with an interface in network n
- smtenc.association_rel(
- enode, smtenc.associations["infrastructure_AutoScalingGroup::machineDefinition"], vm),
- smtenc.association_rel(
- vm, smtenc.associations["infrastructure_Node::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], esubnet),
- )
- )
- )
- )
- )
- )
- )
- )
-
-
-# There are no duplicated interfaces.
-def iface_uniq(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- endPointAttr = smtenc.attributes["infrastructure_NetworkInterface::endPoint"]
- ni1, ni2 = get_consts(smtsorts, ["ni1", "ni2"])
- value = Const("value", smtsorts.attr_data_sort)
- return And(
- smtenc.attribute_rel(ni1, endPointAttr, value),
- smtenc.attribute_rel(ni2, endPointAttr, value),
- ni1 != ni2,
- )
-
-# All software components have been deployed to some node.
-
-
-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(
- 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),
- )
- )
- )
- )
-
-# All abstract infrastructure elements are mapped to an element in the active concretization.
-
-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")
-]
-
-# 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:
- 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 = get_consts(
- smtsorts, ["ielem", "concr", "provider", "celem"])
- 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
- )
- )
- )
-
-# 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 = get_consts(
- smtsorts, ["ielem", "concr", "provider", "celem"])
- 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 sw_components_have_source_code_property(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
-# sw_comp, prop = get_consts(smtsorts, ["sw_comp prop"])
-
-# big_x = smtsorts.attr_data_sort.str(smtenc.str_symbols["source_code"])
-
-# return And(
-# smtenc.element_class_fun(sw_comp) == smtenc.classes["application_SoftwareComponent"],
-# Not(
-# Exists([prop], And(
-# smtenc.element_class_fun(prop) == smtenc.classes["commons_SProperty"],
-# smtenc.attribute_rel(prop, smtenc.attributes["commons_Property::key"], big_x),
-# smtenc.association_rel(sw_comp, smtenc.associations["commons_DOMLElement::annotations"], prop)
-# ))
-# )
-# )
-
-# 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 = get_consts(smtsorts, ["sg iface"])
- return And(
- smtenc.element_class_fun(
- sg) == smtenc.classes["infrastructure_SecurityGroup"],
- Not(Exists([iface],
- smtenc.association_rel(
- iface, smtenc.associations["infrastructure_NetworkInterface::associated"], sg)
- ))
- )
-
-# TODO: Check if HTTP should be disabled too
-# TODO: Add support for DOML 2.3+ if kept
-def external_services_must_have_https(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprRef:
- saas, sw_iface, sw_comp, deployment, ielem, net_iface, sec_group, rule = get_consts(smtsorts,
- ["saas, sw_iface, sw_comp, deployment, ielem, net_iface, sec_group, rule"])
- return And(
- smtenc.element_class_fun(saas) == smtenc.classes["application_SaaS"],
- smtenc.element_class_fun(
- sec_group) == smtenc.classes["infrastructure_SecurityGroup"],
- Not(Exists([sw_iface, sw_comp, deployment, ielem, net_iface, rule],
- And(
- smtenc.association_rel(
- saas, smtenc.associations["application_SaaS::exposedInterfaces"], sw_iface),
- smtenc.association_rel(
- sw_comp, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], sw_iface),
- smtenc.association_rel(
- deployment, smtenc.associations["commons_Deployment::component"], sw_comp),
- smtenc.association_rel(
- deployment, smtenc.associations["commons_Deployment::node"], ielem),
- smtenc.association_rel(
- ielem, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
- smtenc.association_rel(
- net_iface, smtenc.associations["infrastructure_NetworkInterface::associated"], sec_group),
- smtenc.association_rel(
- sec_group, smtenc.associations["infrastructure_SecurityGroup::rules"], rule),
- smtenc.attribute_rel(
- rule, smtenc.attributes["infrastructure_Rule::fromPort"], smtsorts.attr_data_sort.int(443)),
- smtenc.attribute_rel(
- rule, smtenc.attributes["infrastructure_Rule::toPort"], smtsorts.attr_data_sort.int(443)),
- smtenc.attribute_rel(rule, smtenc.attributes["infrastructure_Rule::kind"], smtsorts.attr_data_sort.str(
- smtenc.str_symbols["INGRESS"]))
- )
- ))
- )
-
-# Error Descriptions
-
-
-def ed_vm_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."
-
-
-def ed_software_package_iface_net(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
- try:
- 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."
- )
- except:
- 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:
- try:
- 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."
- except:
- return "Two network interfaces share the same IP address."
-
-
-def ed_all_SoftwareComponents_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."
-
-
-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."
-
-
-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."
-
-
-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."
-
-
-def ed_external_services_must_have_https(solver: Solver, smtsorts: SMTSorts, intermediate_model: IntermediateModel) -> str:
- try:
- saas = Const("saas", smtsorts.element_sort)
- saas_name = get_user_friendly_name(
- intermediate_model, solver.model(), saas)
-
- sec_group = Const("sec_group", smtsorts.element_sort)
- sec_group_name = get_user_friendly_name(
- intermediate_model, solver.model(), sec_group)
-
- if saas_name:
- return f"A Security Group doesn't have a rule to access external service (SaaS) named '{saas_name}' through HTTPS (port 443)."
- if sec_group:
- return f"Security Group {sec_group_name} doesn't have a rule to access external service (SaaS) through HTTPS (port 443)."
- except:
- return "A Security Group doesn't have a rule to access an external service (SaaS) through HTTPS (port 443)."
+from .imc import Requirement, RequirementStore
+from .intermediate_model import DOMLVersion
+from .builtin_requirements import *
REQUIREMENTS = {
DOMLVersion.V2_0: [
- (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_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),
- (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),
- (security_group_must_have_iface, "security_group_must_have_iface",
- "All security group should be a associated to a network interface", ed_security_group_must_have_iface),
- # TODO: Fix rule
- # (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
+ VM_HAS_IFACE,
+ SOFTWARE_PACKAGE_IFACE_NET,
+ IFACE_UNIQ,
+ ALL_SOFTWARE_COMPONENTS_DEPLOYED,
+ ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
+ ALL_CONCRETE_MAP_SOMETHING,
+ SECURITY_GROUP_MUST_HAVE_IFACE
],
DOMLVersion.V2_1: [
- (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_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),
- (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),
- (security_group_must_have_iface, "security_group_must_have_iface",
- "All security group should be a associated to a network interface", ed_security_group_must_have_iface),
- # TODO: Fix rule
- # (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
+ VM_HAS_IFACE,
+ SOFTWARE_PACKAGE_IFACE_NET_V2_1,
+ IFACE_UNIQ,
+ ALL_SOFTWARE_COMPONENTS_DEPLOYED,
+ ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
+ ALL_CONCRETE_MAP_SOMETHING,
+ SECURITY_GROUP_MUST_HAVE_IFACE
],
DOMLVersion.V2_2: [
- (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_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),
- (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),
- (security_group_must_have_iface, "security_group_must_have_iface",
- "All security group should be a associated to a network interface", ed_security_group_must_have_iface),
- # TODO: Fix rule
- # (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_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_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),
- (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),
- (security_group_must_have_iface, "security_group_must_have_iface",
- "All security group should be a associated to a network interface", ed_security_group_must_have_iface),
- # TODO: Fix rule
- # (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
+ VM_HAS_IFACE,
+ SOFTWARE_PACKAGE_IFACE_NET_V2_1,
+ IFACE_UNIQ,
+ ALL_SOFTWARE_COMPONENTS_DEPLOYED,
+ ALL_INFRASTRUCTURE_ELEMENTS_DEPLOYED,
+ ALL_CONCRETE_MAP_SOMETHING,
+ SECURITY_GROUP_MUST_HAVE_IFACE
],
DOMLVersion.V2_3: [
- (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_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),
- (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),
- (security_group_must_have_iface, "security_group_must_have_iface",
- "All security group should be a associated to a network interface", ed_security_group_must_have_iface),
- # TODO: Fix rule
- # (external_services_must_have_https, "external_services_must_have_https", "All external SaaS should be accessed through HTTPS.", ed_external_services_must_have_https)
+ VM_HAS_IFACE_V2_3,
+ 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
],
}
-
CommonRequirements = {ver: RequirementStore(
[
Requirement(
diff --git a/mc_openapi/doml_mc/imc.py b/mc_openapi/doml_mc/imc.py
index 68aaa87d8f83ee587d20fa2da251c7af4332dab3..60e1e7ec79ef2b32407bf6aa5f47972244574781 100644
--- a/mc_openapi/doml_mc/imc.py
+++ b/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
))
diff --git a/requirements.txt b/requirements.txt
index 1eb60147aba0f845f5450a04bb238b6476ec38a1..c967d1527a6024d0b39f15dbea2edc0e14404b10 100644
--- a/requirements.txt
+++ b/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
diff --git a/tests/test_modelchecker.py b/tests/test_modelchecker.py
index df51edc5375beec929fb578c927e65b357bc408d..ac9355f16b6261be9d1a55c7dfd0ff61a6075635 100644
--- a/tests/test_modelchecker.py
+++ b/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': {