diff --git a/mc_openapi/doml_mc/common_reqs.py b/mc_openapi/doml_mc/common_reqs.py index 798ef41e673c884cee8b727f5568f6182f207f0f..c64922c9116bab3e4c441454d8a681bce3c8676f 100644 --- a/mc_openapi/doml_mc/common_reqs.py +++ b/mc_openapi/doml_mc/common_reqs.py @@ -1,7 +1,7 @@ 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" - ), + *( + checkOneClass( + ielem, concr, provider, celem, + 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" - ), + *( + checkOneClass( + ielem, provider, celem, + 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: