rewrite some common_reqs.py

mc_openapi/doml_mc/common_reqs.py

 from re import M
 from typing import Optional
 
-from z3 import And, Const, Consts, Exists, ExprRef, ModelRef, Not, Or, Solver
+from z3 import And, Const, Consts, Exists, ExprRef, ModelRef, Not, Or, Solver, ForAll
 
 from .error_desc_helper import get_user_friendly_name
 from .imc import Requirement, RequirementStore, SMTEncoding, SMTSorts
@@ -398,9 +398,21 @@ def all_SoftwareComponents_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts) ->
 
 # 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, concr, provider, celem, ielemClass, providerAssoc, celemAssoc):
+    def checkOneClass(ielem, cinfr, provider, celem, ielemClass, providerAssoc, celemAssoc):
         return And(
             smtenc.element_class_fun(ielem) == smtenc.classes[ielemClass],
             Not(
@@ -408,7 +420,7 @@ def all_infrastructure_elements_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts
                     [provider, celem],
                     And(
                         smtenc.association_rel(
-                            concr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
+                            cinfr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
                         smtenc.association_rel(
                             provider, smtenc.associations[providerAssoc], celem),
                         smtenc.association_rel(
@@ -424,30 +436,13 @@ def all_infrastructure_elements_deployed(smtenc: SMTEncoding, smtsorts: SMTSorts
         smtenc.element_class_fun(
             concr) == smtenc.classes["concrete_ConcreteInfrastructure"],
         Or(
+            *(
                 checkOneClass(
                     ielem, concr, provider, celem,
-                "infrastructure_VirtualMachine",
-                "concrete_RuntimeProvider::vms",
-                "concrete_VirtualMachine::maps"
-            ),
-            checkOneClass(
-                ielem, concr, provider, celem,
-                "infrastructure_Network",
-                "concrete_RuntimeProvider::networks",
-                "concrete_Network::maps"
-            ),
-            checkOneClass(
-                ielem, concr, provider, celem,
-                "infrastructure_Storage",
-                "concrete_RuntimeProvider::storages",
-                "concrete_Storage::maps"
-            ),
-            checkOneClass(
-                ielem, concr, provider, celem,
-                "infrastructure_FunctionAsAService",
-                "concrete_RuntimeProvider::faas",
-                "concrete_FunctionAsAService::maps"
-            ),
+                    ielemClass, providerAssoc, celemAssoc
+                ) 
+                for ielemClass, providerAssoc, celemAssoc in CELEMS_V2_0
+            )
         )
     )
 
@@ -476,41 +471,13 @@ def all_concrete_map_something(smtenc: SMTEncoding, smtsorts: SMTSorts) -> ExprR
         smtenc.association_rel(
             concr, smtenc.associations["concrete_ConcreteInfrastructure::providers"], provider),
         Or(
+            *(
                 checkOneClass(
                     ielem, provider, celem,
-                "concrete_RuntimeProvider::vms",
-                "concrete_VirtualMachine::maps"
-            ),
-            checkOneClass(
-                ielem, provider, celem,
-                "concrete_RuntimeProvider::vmImages",
-                "concrete_VMImage::maps"
-            ),
-            checkOneClass(
-                ielem, provider, celem,
-                "concrete_RuntimeProvider::containerImages",
-                "concrete_ContainerImage::maps"
-            ),
-            checkOneClass(
-                ielem, provider, celem,
-                "concrete_RuntimeProvider::networks",
-                "concrete_Network::maps"
-            ),
-            checkOneClass(
-                ielem, provider, celem,
-                "concrete_RuntimeProvider::storages",
-                "concrete_Storage::maps"
-            ),
-            checkOneClass(
-                ielem, provider, celem,
-                "concrete_RuntimeProvider::faas",
-                "concrete_FunctionAsAService::maps"
-            ),
-            checkOneClass(
-                ielem, provider, celem,
-                "concrete_RuntimeProvider::group",
-                "concrete_ComputingGroup::maps"
-            ),
+                    providerAssoc, celemAssoc
+                )
+                for _, providerAssoc, celemAssoc in CELEMS_V2_0
+            )
         )
     )
 
@@ -643,9 +610,9 @@ def ed_all_infrastructure_elements_deployed(solver: Solver, smtsorts: SMTSorts,
         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."
+            return f"Abstract infrastructure element '{ielem_name}' is not mapped to any element in the active concretization."
     except:
-        return "An abstract infrastructure element has not been mapped to any element in the active concretization."
+        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:
@@ -654,9 +621,9 @@ def ed_all_concrete_map_something(solver: Solver, smtsorts: SMTSorts, intermedia
         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."
+            return f"Concrete infrastructure element '{celem_name}' is not mapped to any abstract infrastructure element."
     except:
-        return "A concrete infrastructure element is mapped to no abstract infrastructure element."
+        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: