diff --git a/mc_openapi/__main__.py b/mc_openapi/__main__.py index 7d04f2fee0db4692e5c32c7a2245f3d11cefcd9b..42877c0d2501d435bb5d2555e8956b4049c89197 100644 --- a/mc_openapi/__main__.py +++ b/mc_openapi/__main__.py @@ -103,7 +103,7 @@ else: print("Failed to parse the DOMLR.", file=sys.stderr) exit(-1) - if doml_ver == DOMLVersion.V2_2: + if doml_ver == DOMLVersion.V2_2 or doml_ver == DOMLVersion.V2_2_1: model = get_pyecore_model(doml_xmi, doml_ver) func_reqs = model.functionalRequirements.items for req in func_reqs: diff --git a/mc_openapi/doml_mc/imc.py b/mc_openapi/doml_mc/imc.py index 3bab3f156537e1cd46cd7ed0498711895d2c213b..90cb8367f9349bf2b2aa119332aa33c9a5431f0b 100644 --- a/mc_openapi/doml_mc/imc.py +++ b/mc_openapi/doml_mc/imc.py @@ -172,6 +172,5 @@ class IntermediateModelChecker: )) self.solver.pop() - stats = self.solver.statistics() - STATS.add(stats) + # stats = self.solver.statistics() return MCResults(results) diff --git a/tests/doml/v2.2/nginx_func_req.domlx b/tests/doml/v2.2/nginx_func_req.domlx index f0f4e5af2424f404c8532f60487286bcf46367fb..5de0b46c4eec6bf1f1f466f72579750e22cfc2d9 100644 --- a/tests/doml/v2.2/nginx_func_req.domlx +++ b/tests/doml/v2.2/nginx_func_req.domlx @@ -55,5 +55,5 @@ <configurations name="conf"> <deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/> </configurations> - <functionalRequirements name="req_ext" description="+ "All Virtual Machines have a Interface and at least 4 CPUs" forall vm (vm is class abstract.VirtualMachine implies exists iface (vm has abstract.ComputingNode.ifaces iface and vm has abstract.ComputingNode.cpu_count >= 4 )) error: "A vm does lacks an associated interface or has less than 4 CPUs""/> + <functionalRequirements name="req_ext" description="```

 + "VM must have iface and iface is connected to network"
 	forall vm (
 		vm is class abstract.VirtualMachine
 	implies
 (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 )
 )
 error: "TEST ERROR"
 
 ```"/> </commons:DOMLModel> diff --git a/tests/doml/v2.2/nginx_func_req2_unsat.domlx b/tests/doml/v2.2/nginx_func_req2_unsat.domlx new file mode 100644 index 0000000000000000000000000000000000000000..ab00f04895723cb0d57cd329588537d0c45a97ac --- /dev/null +++ b/tests/doml/v2.2/nginx_func_req2_unsat.domlx @@ -0,0 +1,59 @@ +<?xml version="1.0" encoding="ASCII"?> +<commons:DOMLModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:app="http://www.piacere-project.eu/doml/application" xmlns:commons="http://www.piacere-project.eu/doml/commons" xmlns:infra="http://www.piacere-project.eu/doml/infrastructure" xmlns:optimization="http://www.piacere-project.eu/doml/optimization" name="nginx_func_req" activeConfiguration="//@configurations.0" activeInfrastructure="//@concretizations.0"> + <application name="app"> + <components xsi:type="app:SoftwareComponent" name="nginx"> + <annotations xsi:type="commons:SProperty" key="source_code" value="/usr/share/nginx/html/index.html"/> + </components> + </application> + <infrastructure name="infra"> + <generators xsi:type="infra:VMImage" name="vm_img" uri="ami-xxxxxxxxxxxxxxxxx" kind="IMAGE" generatedVMs="//@infrastructure/@groups.0/@machineDefinition"/> + <credentials xsi:type="commons:KeyPair" name="ssh_key" user="ec2-user" keyfile="/tmp/ssh_key_file" algorithm="RSA" bits="4096"/> + <groups xsi:type="infra:AutoScalingGroup" name="ag"> + <machineDefinition name="vm1" credentials="//@infrastructure/@credentials.0" generatedFrom="//@infrastructure/@generators.0"> + <ifaces name="i1" endPoint="10.0.0.1" associated="//@infrastructure/@securityGroups.0"/> + <location region="eu-central-1"/> + </machineDefinition> + </groups> + <securityGroups name="sg" ifaces="//@infrastructure/@groups.0/@machineDefinition/@ifaces.0"> + <rules name="icmp" protocol="icmp" fromPort="-1" toPort="-1"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="http" kind="INGRESS" protocol="tcp" fromPort="80" toPort="80"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="https" kind="INGRESS" protocol="tcp" fromPort="443" toPort="443"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="ssh" kind="INGRESS" protocol="tcp" fromPort="22" toPort="22"> + <cidr>0.0.0.0/0</cidr> + </rules> + </securityGroups> + <networks name="vpc" protocol="tcp/ip" addressRange="/24"> + <subnets name="vpc_subnet" protocol="tcp/ip" addressRange="/24"/> + </networks> + </infrastructure> + <concretizations name="con_infra"> + <providers name="aws"> + <vms name="ec2_vm" maps="//@infrastructure/@groups.0/@machineDefinition"> + <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/> + <annotations xsi:type="commons:SProperty" key="instance_type" value="t2.micro"/> + <annotations xsi:type="commons:SProperty" key="ssh_key_name" value="demo-key"/> + <annotations xsi:type="commons:SProperty" key="ec2_role_name" value="demo-ec2-role"/> + </vms> + <vmImages name="concrete_vm_image" maps="//@infrastructure/@generators.0"/> + <networks name="concrete_net" maps="//@infrastructure/@networks.0"> + <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/> + </networks> + </providers> + </concretizations> + <optimization name="opt"> + <objectives xsi:type="optimization:MeasurableObjective" kind="min" property="cost"/> + <objectives xsi:type="optimization:MeasurableObjective" kind="max" property="availability"/> + <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req1" description="Cost <= 70.0" property="cost" max="70.0"/> + <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req2" description="Availability >= 66.5%" property="availability" min="66.5"/> + </optimization> + <configurations name="conf"> + <deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/> + </configurations> + <functionalRequirements name="req_ext" description="```

 + "VM must have iface and iface is connected to network"
 	forall vm (
 		vm is class abstract.VirtualMachine
 	implies
 (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 )
 )
 error: "TEST ERROR"
 
 ```"/> +</commons:DOMLModel> diff --git a/tests/doml/v2.2/nginx_func_req2_unsat_neg.domlx b/tests/doml/v2.2/nginx_func_req2_unsat_neg.domlx new file mode 100644 index 0000000000000000000000000000000000000000..e577a79eccc03adce5be21f56ce4495894f39b2d --- /dev/null +++ b/tests/doml/v2.2/nginx_func_req2_unsat_neg.domlx @@ -0,0 +1,59 @@ +<?xml version="1.0" encoding="ASCII"?> +<commons:DOMLModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:app="http://www.piacere-project.eu/doml/application" xmlns:commons="http://www.piacere-project.eu/doml/commons" xmlns:infra="http://www.piacere-project.eu/doml/infrastructure" xmlns:optimization="http://www.piacere-project.eu/doml/optimization" name="nginx_func_req" activeConfiguration="//@configurations.0" activeInfrastructure="//@concretizations.0"> + <application name="app"> + <components xsi:type="app:SoftwareComponent" name="nginx"> + <annotations xsi:type="commons:SProperty" key="source_code" value="/usr/share/nginx/html/index.html"/> + </components> + </application> + <infrastructure name="infra"> + <generators xsi:type="infra:VMImage" name="vm_img" uri="ami-xxxxxxxxxxxxxxxxx" kind="IMAGE" generatedVMs="//@infrastructure/@groups.0/@machineDefinition"/> + <credentials xsi:type="commons:KeyPair" name="ssh_key" user="ec2-user" keyfile="/tmp/ssh_key_file" algorithm="RSA" bits="4096"/> + <groups xsi:type="infra:AutoScalingGroup" name="ag"> + <machineDefinition name="vm1" credentials="//@infrastructure/@credentials.0" generatedFrom="//@infrastructure/@generators.0"> + <ifaces name="i1" endPoint="10.0.0.1" associated="//@infrastructure/@securityGroups.0"/> + <location region="eu-central-1"/> + </machineDefinition> + </groups> + <securityGroups name="sg" ifaces="//@infrastructure/@groups.0/@machineDefinition/@ifaces.0"> + <rules name="icmp" protocol="icmp" fromPort="-1" toPort="-1"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="http" kind="INGRESS" protocol="tcp" fromPort="80" toPort="80"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="https" kind="INGRESS" protocol="tcp" fromPort="443" toPort="443"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="ssh" kind="INGRESS" protocol="tcp" fromPort="22" toPort="22"> + <cidr>0.0.0.0/0</cidr> + </rules> + </securityGroups> + <networks name="vpc" protocol="tcp/ip" addressRange="/24"> + <subnets name="vpc_subnet" protocol="tcp/ip" addressRange="/24"/> + </networks> + </infrastructure> + <concretizations name="con_infra"> + <providers name="aws"> + <vms name="ec2_vm" maps="//@infrastructure/@groups.0/@machineDefinition"> + <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/> + <annotations xsi:type="commons:SProperty" key="instance_type" value="t2.micro"/> + <annotations xsi:type="commons:SProperty" key="ssh_key_name" value="demo-key"/> + <annotations xsi:type="commons:SProperty" key="ec2_role_name" value="demo-ec2-role"/> + </vms> + <vmImages name="concrete_vm_image" maps="//@infrastructure/@generators.0"/> + <networks name="concrete_net" maps="//@infrastructure/@networks.0"> + <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/> + </networks> + </providers> + </concretizations> + <optimization name="opt"> + <objectives xsi:type="optimization:MeasurableObjective" kind="min" property="cost"/> + <objectives xsi:type="optimization:MeasurableObjective" kind="max" property="availability"/> + <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req1" description="Cost <= 70.0" property="cost" max="70.0"/> + <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req2" description="Availability >= 66.5%" property="availability" min="66.5"/> + </optimization> + <configurations name="conf"> + <deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/> + </configurations> + <functionalRequirements name="req_ext" description="```

# + "VM must have iface and iface is connected to network"
# 	forall vm (
# 		vm is class abstract.VirtualMachine
# 	implies
# (
# 	vm has abstract.ComputingNode.ifaces iface
# 	and
# 	iface has abstract.NetworkInterface.belongsTo net
# )
# )
# error: "TEST ERROR"

- "VM must have iface and iface is connected to network"
	vm is class abstract.VirtualMachine
	and
	not exists iface, net (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 
 )
 error: "TEST ERROR"
 
 ```"/> +</commons:DOMLModel> diff --git a/tests/doml/v2.2/nginx_func_req_neg.domlx b/tests/doml/v2.2/nginx_func_req_neg.domlx new file mode 100644 index 0000000000000000000000000000000000000000..206a82af3d96c2f2a393981599b26adf6cfd5b94 --- /dev/null +++ b/tests/doml/v2.2/nginx_func_req_neg.domlx @@ -0,0 +1,59 @@ +<?xml version="1.0" encoding="ASCII"?> +<commons:DOMLModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:app="http://www.piacere-project.eu/doml/application" xmlns:commons="http://www.piacere-project.eu/doml/commons" xmlns:infra="http://www.piacere-project.eu/doml/infrastructure" xmlns:optimization="http://www.piacere-project.eu/doml/optimization" name="nginx_func_req" activeConfiguration="//@configurations.0" activeInfrastructure="//@concretizations.0"> + <application name="app"> + <components xsi:type="app:SoftwareComponent" name="nginx"> + <annotations xsi:type="commons:SProperty" key="source_code" value="/usr/share/nginx/html/index.html"/> + </components> + </application> + <infrastructure name="infra"> + <generators xsi:type="infra:VMImage" name="vm_img" uri="ami-xxxxxxxxxxxxxxxxx" kind="IMAGE" generatedVMs="//@infrastructure/@groups.0/@machineDefinition"/> + <credentials xsi:type="commons:KeyPair" name="ssh_key" user="ec2-user" keyfile="/tmp/ssh_key_file" algorithm="RSA" bits="4096"/> + <groups xsi:type="infra:AutoScalingGroup" name="ag"> + <machineDefinition name="vm1" credentials="//@infrastructure/@credentials.0" generatedFrom="//@infrastructure/@generators.0"> + <ifaces name="i1" endPoint="10.0.0.1" belongsTo="//@infrastructure/@networks.0" associated="//@infrastructure/@securityGroups.0"/> + <location region="eu-central-1"/> + </machineDefinition> + </groups> + <securityGroups name="sg" ifaces="//@infrastructure/@groups.0/@machineDefinition/@ifaces.0"> + <rules name="icmp" protocol="icmp" fromPort="-1" toPort="-1"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="http" kind="INGRESS" protocol="tcp" fromPort="80" toPort="80"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="https" kind="INGRESS" protocol="tcp" fromPort="443" toPort="443"> + <cidr>0.0.0.0/0</cidr> + </rules> + <rules name="ssh" kind="INGRESS" protocol="tcp" fromPort="22" toPort="22"> + <cidr>0.0.0.0/0</cidr> + </rules> + </securityGroups> + <networks name="vpc" protocol="tcp/ip" addressRange="/24" connectedIfaces="//@infrastructure/@groups.0/@machineDefinition/@ifaces.0"> + <subnets name="vpc_subnet" protocol="tcp/ip" addressRange="/24"/> + </networks> + </infrastructure> + <concretizations name="con_infra"> + <providers name="aws"> + <vms name="ec2_vm" maps="//@infrastructure/@groups.0/@machineDefinition"> + <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/> + <annotations xsi:type="commons:SProperty" key="instance_type" value="t2.micro"/> + <annotations xsi:type="commons:SProperty" key="ssh_key_name" value="demo-key"/> + <annotations xsi:type="commons:SProperty" key="ec2_role_name" value="demo-ec2-role"/> + </vms> + <vmImages name="concrete_vm_image" maps="//@infrastructure/@generators.0"/> + <networks name="concrete_net" maps="//@infrastructure/@networks.0"> + <annotations xsi:type="commons:SProperty" key="vm_name" value="nginx-host"/> + </networks> + </providers> + </concretizations> + <optimization name="opt"> + <objectives xsi:type="optimization:MeasurableObjective" kind="min" property="cost"/> + <objectives xsi:type="optimization:MeasurableObjective" kind="max" property="availability"/> + <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req1" description="Cost <= 70.0" property="cost" max="70.0"/> + <nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req2" description="Availability >= 66.5%" property="availability" min="66.5"/> + </optimization> + <configurations name="conf"> + <deployments component="//@application/@components.0" node="//@infrastructure/@groups.0/@machineDefinition"/> + </configurations> + <functionalRequirements name="req_ext" description="```

# + "VM must have iface and iface is connected to network"
# 	forall vm (
# 		vm is class abstract.VirtualMachine
# 	implies
# (
# 	vm has abstract.ComputingNode.ifaces iface
# 	and
# 	iface has abstract.NetworkInterface.belongsTo net
# )
# )
# error: "TEST ERROR"

- "VM must have iface and iface is connected to network"
	vm is class abstract.VirtualMachine
	and
	not exists iface, net (
 	vm has abstract.ComputingNode.ifaces iface
 	and
 	iface has abstract.NetworkInterface.belongsTo net
 
 )
 error: "TEST ERROR"
 
 ```"/> +</commons:DOMLModel>