Skip to content
Snippets Groups Projects
Commit ac1a0380 authored by Michele Chiari's avatar Michele Chiari
Browse files

Check more requirements.

parent 623c1c4e
Branches
No related tags found
No related merge requests found
......@@ -1490,7 +1490,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.9.12"
"version": "3.9.13"
},
"orig_nbformat": 4
},
......
......@@ -5,7 +5,8 @@ from dataclasses import dataclass
from z3 import (
CheckSatResult, Consts, ExprRef, FuncDeclRef, Solver, SortRef,
ForAll, Exists, Implies, And
ForAll, Exists, Implies, And, Or,
sat, unsat, unknown
)
from .. import assets
......@@ -143,19 +144,33 @@ class ModelChecker:
reciprocate_inverse_associations(self.intermediate_model, ModelChecker.inv_assoc)
instantiate_solver()
def check_common_requirements(self) -> tuple[CheckSatResult, str]:
common_requirements = self.get_common_requirements()
some_dontknow = False
for expr_thunk, assert_name, _, err_msg in common_requirements:
self.solver.push()
self.solver.assert_and_track(expr_thunk(), "vm_iface")
res = self.solver.check()
if res == unsat:
return res, err_msg
elif res == unknown:
some_dontknow = True
self.solver.pop()
if some_dontknow:
return unknown, "Unable to check some requirements."
else:
return sat, "All requirements satisfied."
def get_consts(self, consts: list[str]) -> list[ExprRef]:
return Consts(" ".join(consts), self.smt_sorts.element_sort)
def check(self) -> CheckSatResult:
return self.solver.check()
def add_requirement(self, assertion: ExprRef, description: str):
self.solver.assert_and_track(assertion, description)
def get_common_requirements(self):
smtenc = self.smt_encoding
def add_common_requirements(self):
def vm_iface():
vm, iface = self.get_consts(["vm", "iface"])
smtenc = self.smt_encoding
vmIfaceAssertion = ForAll(
return ForAll(
[vm],
Implies(
smtenc.element_class_fun(vm) == smtenc.classes["infrastructure_VirtualMachine"],
......@@ -167,4 +182,157 @@ class ModelChecker:
)
)
)
self.add_requirement(vmIfaceAssertion, "vm_iface")
def software_package_iface_net():
asc_consumer, asc_exposer, siface, net, net_iface, cn, vm, deployment, dc = self.get_consts(
["asc_consumer", "asc_exposer", "siface", "net", "net_iface", "cn", "vm", "deployment", "dc"]
)
return ForAll(
[asc_consumer, asc_exposer, siface],
Implies(
And(
smtenc.association_rel(asc_consumer, smtenc.associations["application_SoftwareComponent::exposedInterfaces"], siface),
smtenc.association_rel(asc_exposer, smtenc.associations["application_SoftwareComponent::consumedInterfaces"], siface),
),
Exists(
[net],
And(
Or(
Exists(
[cn, deployment, net_iface],
And( # asc_consumer is deployed on a component with an interface in network n
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::node"], cn),
smtenc.association_rel(cn, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
smtenc.association_rel(net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
),
),
Exists( # asc_consumer is deployed on a container hosting a VM with an interface in network n
[cn, deployment, vm, net_iface],
And(
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::component"], asc_consumer),
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::node"], cn),
smtenc.association_rel(cn, 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),
),
),
),
Or(
Exists(
[cn, deployment, net_iface],
And( # asc_exposer is deployed on a component with an interface in network n
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::node"], cn),
smtenc.association_rel(cn, smtenc.associations["infrastructure_ComputingNode::ifaces"], net_iface),
smtenc.association_rel(net_iface, smtenc.associations["infrastructure_NetworkInterface::belongsTo"], net),
),
),
Exists( # asc_exposer is deployed on a container hosting a VM with an interface in network n
[cn, deployment, vm, net_iface],
And(
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::component"], asc_exposer),
smtenc.association_rel(deployment, smtenc.associations["commons_Deployment::node"], cn),
smtenc.association_rel(cn, 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),
),
),
),
),
),
),
)
def iface_uniq():
def any_iface(elem, iface):
ifaces_assocs = [
"infrastructure_ComputingNode::ifaces",
"infrastructure_Storage::ifaces",
"infrastructure_FunctionAsAService::ifaces"
]
return Or(*(smtenc.association_rel(elem, smtenc.associations[assoc_name], iface) for assoc_name in ifaces_assocs))
e1, e2, ni = self.get_consts(["e1", "e2", "i"])
return ForAll(
[e1, e2, ni],
Implies(
And(any_iface(e1, ni), any_iface(e2, ni)),
e1 == e2
)
)
def all_SoftwareComponents_deployed():
sc, deployment, ielem = self.get_consts(["sc", "deployment", "ielem"])
return ForAll(
[sc],
Implies(
smtenc.element_class_fun(sc) == smtenc.classes["application_SoftwareComponent"],
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 all_infrastructure_elements_deployed():
def checkOneClass(ielem, concr, provider, celem, ielemClass, providerAssoc, celemAssoc):
return Implies(
smtenc.element_class_fun(ielem) == smtenc.classes[ielemClass],
Exists(
[provider, celem],
And(
smtenc.association_rel(concr, 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 = self.get_consts(["ielem", "concr", "provider", "celem"])
return Exists(
[concr],
And(
smtenc.element_class_fun(concr) == smtenc.classes["concrete_ConcreteInfrastructure"],
ForAll(
[ielem],
And(
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"
),
)
)
)
)
return [
(vm_iface, "vm_iface", "All virtual machines must be connected to at least one network interface.", "A virtual machine is connected to no network interface."),
(software_package_iface_net, "software_package_iface_net", "All software packages can see the interfaces they need through a common network.", "A software package is deployed on a node that has no access to an interface it consumes."),
(iface_uniq, "iface_uniq", "There are no duplicated interfaces.", "There is a duplicated interface."),
(all_SoftwareComponents_deployed, "all_SoftwareComponents_deployed", "All software components have been deployed to some node.", "A software component has not been deployed to any node."),
(all_infrastructure_elements_deployed, "all_infrastructure_elements_deployed", "All abstract infrastructure elements are mapped to an element in the active concretization.", "An abstract infrastructure element has not been mapped to any element in the active concretization."),
]
%% Cell type:code id: tags:
``` python
import mc_openapi.doml_mc as mc
# doml_document_path = "../../tests/doml/nginx-openstack_v2.domlx"
doml_document_path = "../../tests/doml/nginx-openstack_v2_wrong.domlx"
doml_document_path = "../../tests/doml/nginx-openstack_v2.domlx"
# doml_document_path = "../../tests/doml/nginx-openstack_v2_wrong.domlx"
with open(doml_document_path, "rb") as xmif:
doc = xmif.read()
dmc = mc.ModelChecker(doc)
```
%% Output
Attribute cidr of multiplicity > 1 not supported yet.
Attribute cidr of multiplicity > 1 not supported yet.
Attribute cidr of multiplicity > 1 not supported yet.
Attribute cidr of multiplicity > 1 not supported yet.
%% Cell type:code id: tags:
``` python
dmc.add_common_requirements()
dmc.check()
dmc.check_common_requirements()
```
%% Output
unsat
(sat, 'All requirements satisfied.')
......
......@@ -14,17 +14,16 @@ def post(body, requirement=None):
doml_xmi = body
try:
dmc = ModelChecker(doml_xmi)
dmc.add_common_requirements()
result = dmc.check()
result, msg = dmc.check_common_requirements()
if result == sat:
return {"result": "sat"}
elif result == unsat:
return {"result": "unsat",
"description": "Virtual machine is not linked to any network."}
"description": msg}
else:
return {"result": "dontknow"}
return {"result": "dontknow",
"description": msg}
except Exception as e:
return make_error("Supplied with malformed DOML XMI model.", debug_msg=str(e)), 400
<?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" name="faas_app" activeConfiguration="//@configurations.0" activeInfrastructure="//@concretizations.0">
<application name="ImageResizeApp">
<components xsi:type="app:SoftwareComponent" name="image_resize" consumedInterfaces="//@application/@components.1/@exposedInterfaces.0 //@application/@components.1/@exposedInterfaces.1 //@application/@components.2/@exposedInterfaces.1">
<annotations xsi:type="commons:SProperty" key="source_code" value="path/lambda/function/image_resize.py"/>
<exposedInterfaces name="handle_image"/>
</components>
<components xsi:type="app:SaaS" name="s1">
<exposedInterfaces name="storage_interface"/>
<exposedInterfaces name="bucket_in"/>
</components>
<components xsi:type="app:SaaS" name="s2">
<exposedInterfaces name="storage_interface"/>
<exposedInterfaces name="bucket_out"/>
</components>
<components xsi:type="app:SoftwareComponent" name="notification" consumedInterfaces="//@application/@components.0/@exposedInterfaces.0 //@application/@components.1/@exposedInterfaces.1"/>
<components xsi:type="app:SoftwareComponent" name="web" consumedInterfaces="//@application/@components.1/@exposedInterfaces.0 //@application/@components.2/@exposedInterfaces.1">
<annotations xsi:type="commons:SProperty" key="source_code" value="path/web_app"/>
</components>
</application>
<infrastructure name="infra">
<nodes xsi:type="infra:VirtualMachine" name="vm1" credentials="//@infrastructure/@credentials.0" group="//@infrastructure/@groups.0" generatedFrom="//@infrastructure/@generators.0">
<ifaces name="i1" endPoint="10.0.0.1" belongsTo="//@infrastructure/@networks.0" associated="//@infrastructure/@groups.0"/>
<location region="eu-central-1"/>
</nodes>
<nodes xsi:type="infra:Container" name="c" generatedFrom="//@infrastructure/@generators.1" hosts="//@infrastructure/@nodes.0"/>
<networks name="vpc" protocol="tcp/ip" addressRange="10.0.0.0/24" connectedIfaces="//@infrastructure/@nodes.0/@ifaces.0">
<subnets name="vpc_subnet" protocol="tcp/ip" addressRange="10.0.0.0/24"/>
</networks>
<generators xsi:type="infra:VMImage" name="v_img" uri="ami-xxxxxxxxxxxxxxxxx" kind="IMAGE" generatedVMs="//@infrastructure/@nodes.0"/>
<generators xsi:type="infra:ContainerImage" name="c_img" uri="web-app:0.1.0" kind="IMAGE" generatedContainers="//@infrastructure/@nodes.1"/>
<storages name="st1"/>
<storages name="st2"/>
<faas name="f"/>
<credentials xsi:type="infra:KeyPair" name="ssh_key" user="ec2-user" keyfile="/tmp/ssh_key_file" algorithm="RSA" bits="4096"/>
<groups xsi:type="infra:SecurityGroup" name="sg" groupedNodes="//@infrastructure/@nodes.0" ifaces="//@infrastructure/@nodes.0/@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>
</groups>
</infrastructure>
<concretizations name="con_infra">
<providers name="aws">
<vms name="concrete_vm" maps="//@infrastructure/@nodes.0">
<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>
<networks name="concrete_net" maps="//@infrastructure/@networks.0"/>
<storages name="s3_bucket_in" maps="//@infrastructure/@storages.0">
<annotations xsi:type="commons:SProperty" key="bucket_name" value="bucket_in"/>
</storages>
<storages name="s3_bucket_out" maps="//@infrastructure/@storages.1">
<annotations xsi:type="commons:SProperty" key="bucket_name" value="bucket_out"/>
</storages>
<faas name="concrete_f" maps="//@infrastructure/@faas.0">
<annotations xsi:type="commons:SProperty" key="lambda_role_name" value="DemoLambdaRole"/>
<annotations xsi:type="commons:SProperty" key="lambda_runtime" value="python3.8"/>
<annotations xsi:type="commons:SProperty" key="lambda_handler" value="image_resize.lambda_handler"/>
<annotations xsi:type="commons:IProperty" key="lambda_timeout" value="5"/>
<annotations xsi:type="commons:IProperty" key="lambda_memory" value="128"/>
</faas>
</providers>
</concretizations>
<configurations name="config1">
<deployments component="//@application/@components.0" node="//@infrastructure/@faas.0"/>
<deployments component="//@application/@components.4" node="//@infrastructure/@nodes.1"/>
<deployments component="//@application/@components.1" node="//@infrastructure/@storages.0"/>
<deployments component="//@application/@components.2" node="//@infrastructure/@storages.1"/>
</configurations>
</commons:DOMLModel>
......@@ -7,31 +7,27 @@
</application>
<infrastructure name="infra">
<nodes xsi:type="infra:AutoScalingGroup" name="ag" deploymentNetwork="//@infrastructure/@networks.0">
<machineDefinition name="vm1" credentials="//@infrastructure/@credentials.0" group="//@infrastructure/@secGroups.0" generatedFrom="//@infrastructure/@generators.0">
<ifaces name="i1" endPoint="16.0.0.1" belongsTo="//@infrastructure/@networks.0" associated="//@infrastructure/@secGroups.0"/>
<machineDefinition name="vm1" os="ubuntu-20.04.3" credentials="//@infrastructure/@credentials.0" group="//@infrastructure/@groups.0" generatedFrom="//@infrastructure/@generators.0">
<ifaces name="i1" endPoint="16.0.0.1" belongsTo="//@infrastructure/@networks.0" associated="//@infrastructure/@groups.0"/>
</machineDefinition>
</nodes>
<networks name="net1" protocol="tcp/ip" addressRange="16.0.0.0/24" connectedIfaces="//@infrastructure/@nodes.0/@machineDefinition/@ifaces.0"/>
<secGroups name="sg" groupedNodes="//@infrastructure/@nodes.0/@machineDefinition" ifaces="//@infrastructure/@nodes.0/@machineDefinition/@ifaces.0">
<rules name="out_all" protocol="-1" fromPort="0" toPort="0">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<generators xsi:type="infra:VMImage" name="v_img" generatedVMs="//@infrastructure/@nodes.0/@machineDefinition"/>
<credentials xsi:type="infra:KeyPair" name="ssh_key" user="ubuntu" keyfile="/home/user1/.ssh/openstack.key" algorithm="RSA" bits="4096"/>
<groups xsi:type="infra:SecurityGroup" name="sg" groupedNodes="//@infrastructure/@nodes.0/@machineDefinition" ifaces="//@infrastructure/@nodes.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">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<cidr>0.0.0.0/0</cidr>
</rules>
<rules name="https" kind="INGRESS" protocol="tcp" fromPort="443" toPort="443">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<cidr>0.0.0.0/0</cidr>
</rules>
<rules name="ssh" kind="INGRESS" protocol="tcp" fromPort="22" toPort="22">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<cidr>0.0.0.0/0</cidr>
</rules>
</secGroups>
<generators xsi:type="infra:VMImage" name="v_img" generatedVMs="//@infrastructure/@nodes.0/@machineDefinition"/>
<credentials xsi:type="infra:KeyPair" name="ssh_key" user="ubuntu" keyfile="/home/user1/.ssh/openstack.key" algorithm="RSA" bits="4096"/>
</groups>
</infrastructure>
<concretizations name="con_infra">
<providers name="openstack">
......@@ -49,28 +45,10 @@
</providers>
</concretizations>
<optimization name="opt">
<solutions name="sol1">
<objectives cost="200.0" availability="99.76667" performance="8.0"/>
<decisions>Storage4_Europe</decisions>
<decisions>db.dynamo.3</decisions>
<decisions>C8_Germany</decisions>
</solutions>
<solutions name="sol2">
<objectives cost="45.53" availability="99.03333" performance="11.0"/>
<decisions>Storage1_Spain</decisions>
<decisions>db.dynamo.3</decisions>
<decisions>t2.nano</decisions>
</solutions>
<objectives xsi:type="optimization:MeasurableObjective" kind="min" property="cost"/>
<objectives xsi:type="optimization:MeasurableObjective" kind="max" property="availability"/>
<objectives xsi:type="optimization:MeasurableObjective" kind="max" property="performance"/>
<nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req1" description="Cost &lt;= 200" property="cost" max="200.0"/>
<nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req2" description="Availability >= 98%" property="availability" min="98.0"/>
<nonfunctionalRequirements xsi:type="commons:EnumeratedRequirement" name="req3" description="Region" property="region">
<values>00EU</values>
</nonfunctionalRequirements>
<nonfunctionalRequirements xsi:type="commons:EnumeratedRequirement" name="req4" description="Provider" property="provider">
<values>AMAZ</values>
<nonfunctionalRequirements xsi:type="commons:EnumeratedRequirement" name="req2" description="Provider" property="provider">
<values>OPEN</values>
</nonfunctionalRequirements>
</optimization>
<configurations name="config">
......
......@@ -7,29 +7,25 @@
</application>
<infrastructure name="infra">
<nodes xsi:type="infra:AutoScalingGroup" name="ag" deploymentNetwork="//@infrastructure/@networks.0">
<machineDefinition name="vm1" credentials="//@infrastructure/@credentials.0" group="//@infrastructure/@secGroups.0" generatedFrom="//@infrastructure/@generators.0"/>
<machineDefinition name="vm1" os="ubuntu-20.04.3" credentials="//@infrastructure/@credentials.0" group="//@infrastructure/@groups.0" generatedFrom="//@infrastructure/@generators.0"/>
</nodes>
<networks name="net1" protocol="tcp/ip" addressRange="16.0.0.0/24"/>
<secGroups name="sg" groupedNodes="//@infrastructure/@nodes.0/@machineDefinition">
<rules name="out_all" protocol="-1" fromPort="0" toPort="0">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<generators xsi:type="infra:VMImage" name="v_img" generatedVMs="//@infrastructure/@nodes.0/@machineDefinition"/>
<credentials xsi:type="infra:KeyPair" name="ssh_key" user="ubuntu" keyfile="/home/user1/.ssh/openstack.key" algorithm="RSA" bits="4096"/>
<groups xsi:type="infra:SecurityGroup" name="sg" groupedNodes="//@infrastructure/@nodes.0/@machineDefinition">
<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">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<cidr>0.0.0.0/0</cidr>
</rules>
<rules name="https" kind="INGRESS" protocol="tcp" fromPort="443" toPort="443">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<cidr>0.0.0.0/0</cidr>
</rules>
<rules name="ssh" kind="INGRESS" protocol="tcp" fromPort="22" toPort="22">
<addressRanges>0.0.0.0/0</addressRanges>
<addressRanges>::/0</addressRanges>
<cidr>0.0.0.0/0</cidr>
</rules>
</secGroups>
<generators xsi:type="infra:VMImage" name="v_img" generatedVMs="//@infrastructure/@nodes.0/@machineDefinition"/>
<credentials xsi:type="infra:KeyPair" name="ssh_key" user="ubuntu" keyfile="/home/user1/.ssh/openstack.key" algorithm="RSA" bits="4096"/>
</groups>
</infrastructure>
<concretizations name="con_infra">
<providers name="openstack">
......@@ -47,28 +43,10 @@
</providers>
</concretizations>
<optimization name="opt">
<solutions name="sol1">
<objectives cost="200.0" availability="99.76667" performance="8.0"/>
<decisions>Storage4_Europe</decisions>
<decisions>db.dynamo.3</decisions>
<decisions>C8_Germany</decisions>
</solutions>
<solutions name="sol2">
<objectives cost="45.53" availability="99.03333" performance="11.0"/>
<decisions>Storage1_Spain</decisions>
<decisions>db.dynamo.3</decisions>
<decisions>t2.nano</decisions>
</solutions>
<objectives xsi:type="optimization:MeasurableObjective" kind="min" property="cost"/>
<objectives xsi:type="optimization:MeasurableObjective" kind="max" property="availability"/>
<objectives xsi:type="optimization:MeasurableObjective" kind="max" property="performance"/>
<nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req1" description="Cost &lt;= 200" property="cost" max="200.0"/>
<nonfunctionalRequirements xsi:type="commons:RangedRequirement" name="req2" description="Availability >= 98%" property="availability" min="98.0"/>
<nonfunctionalRequirements xsi:type="commons:EnumeratedRequirement" name="req3" description="Region" property="region">
<values>00EU</values>
</nonfunctionalRequirements>
<nonfunctionalRequirements xsi:type="commons:EnumeratedRequirement" name="req4" description="Provider" property="provider">
<values>AMAZ</values>
<nonfunctionalRequirements xsi:type="commons:EnumeratedRequirement" name="req2" description="Provider" property="provider">
<values>OPEN</values>
</nonfunctionalRequirements>
</optimization>
<configurations name="config">
......
......@@ -6,7 +6,7 @@ def test_version():
assert __version__ == '0.2.0'
def test_post_sat():
def test_post_nginx_sat():
with open("tests/doml/nginx-openstack_v2.domlx", "r") as f:
doml = f.read()
......@@ -17,7 +17,7 @@ def test_post_sat():
assert payload["result"] == "sat"
def test_post_unsat():
def test_post_nginx_unsat():
with open("tests/doml/nginx-openstack_v2_wrong.domlx", "r") as f:
doml = f.read()
......@@ -26,3 +26,14 @@ def test_post_unsat():
assert r.status_code == requests.codes.ok
assert payload["result"] is not None
assert payload["result"] == "unsat"
def test_post_faas_sat():
with open("tests/doml/faas.domlx", "r") as f:
doml = f.read()
r = requests.post("http://0.0.0.0:8080/modelcheck", data=doml)
payload = r.json()
assert r.status_code == requests.codes.ok
assert payload["result"] is not None
assert payload["result"] == "unsat"
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment