diff --git a/mc_openapi/doml_mc/common_reqs.py b/mc_openapi/doml_mc/common_reqs.py
index 1ff9a854760cd00bc03c3e13d8acc6a01237bf3e..593129cb1ba381859bda2388b5492687c87e1794 100644
--- a/mc_openapi/doml_mc/common_reqs.py
+++ b/mc_openapi/doml_mc/common_reqs.py
@@ -442,4 +442,4 @@ RequirementLists = {
}
-CommonRequirements = {ver: RequirementStore([Requirement(*rt) for rt in reqs]) for ver, reqs in RequirementLists.items()}
+CommonRequirements = {ver: RequirementStore([Requirement(*rt, flipped=True) for rt in reqs]) for ver, reqs in RequirementLists.items()}
diff --git a/mc_openapi/doml_mc/consistency_reqs.py b/mc_openapi/doml_mc/consistency_reqs.py
index 3b2bcdcf7afe02b7a8c056d74b6430a8b0c78e8d..58568284a5ed307fad5d8a42920502a94eff9101 100644
--- a/mc_openapi/doml_mc/consistency_reqs.py
+++ b/mc_openapi/doml_mc/consistency_reqs.py
@@ -58,6 +58,7 @@ def get_attribute_type_reqs(mm: MetaModel) -> RequirementStore:
f"attribute_st_types {cname}::{mm_attr.name}",
f"Attribute {mm_attr.name} from class {cname} must have type {mm_attr.type}.",
lambda _s, _m, _i: f"Attribute {mm_attr.name} from class {cname} has a type different from {mm_attr.type}.",
+ flipped=True
)
)
return RequirementStore(reqs)
@@ -100,6 +101,7 @@ def get_attribute_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
f"attribute_mult_lb {cname}::{mm_attr.name}",
f"Attribute {mm_attr.name} from class {cname} must have at least one value.",
lambda _s, _m, _i: f"Mandatory attribute {mm_attr.name} from class {cname} has no value.",
+ flipped=True
)
)
if ub == "1":
@@ -109,6 +111,7 @@ def get_attribute_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
f"attribute_mult_ub {cname}::{mm_attr.name}",
f"Attribute {mm_attr.name} from class {cname} must have at most one value.",
lambda _s, _m, _i: f"Attribute {mm_attr.name} from class {cname} has more than one value.",
+ flipped=True
)
)
return RequirementStore(reqs)
@@ -141,6 +144,7 @@ def get_association_type_reqs(mm: MetaModel) -> RequirementStore:
f"association_st_classes {cname}::{mm_assoc.name}",
f"Association {mm_assoc.name} from class {cname} must target class {mm_assoc.class_}.",
lambda _s, _m, _i: f"Association {mm_assoc.name} from class {cname} has a class different from {mm_assoc.class_}.",
+ flipped=True
)
)
return RequirementStore(reqs)
@@ -180,6 +184,7 @@ def get_association_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
f"association_mult_lb {cname}::{mm_assoc.name}",
f"Association {mm_assoc.name} from class {cname} must have at least one target.",
lambda _s, _m, _i: f"Mandatory association {mm_assoc.name} is missing from an element of class {cname}.",
+ flipped=True
)
)
if ub == "1":
@@ -189,6 +194,7 @@ def get_association_multiplicity_reqs(mm: MetaModel) -> RequirementStore:
f"association_mult_ub {cname}::{mm_assoc.name}",
f"Association {mm_assoc.name} from class {cname} must have at most one target.",
lambda _s, _m, _i: f"Association {mm_assoc.name} has more than one target in an element of class {cname}.",
+ flipped=True
)
)
return RequirementStore(reqs)
@@ -213,6 +219,7 @@ def get_inverse_association_reqs(inv_assoc: list[tuple[str, str]]) -> Requiremen
f"association_inverse {an1} {an2}",
f"Association {an1} must be the inverse of {an2}.",
lambda _s, _m, _i: f"Association {an1} is not the inverse of {an2}.",
+ flipped=True
)
)
return RequirementStore(reqs)
diff --git a/mc_openapi/doml_mc/dsl_parser/grammar.lark b/mc_openapi/doml_mc/dsl_parser/grammar.lark
index e7c3aba61153cb0e5c9ee636584336ecb080dfc6..47935de8731b057f49a33024471040945f41add0 100644
--- a/mc_openapi/doml_mc/dsl_parser/grammar.lark
+++ b/mc_openapi/doml_mc/dsl_parser/grammar.lark
@@ -1,6 +1,6 @@
-requirements : ">" requirement (">" requirement)*
+requirements : requirement (requirement)*
-requirement : req_name expression "---" error_desc
+requirement : FLIP_EXPR req_name expression "---" error_desc
req_name : ESCAPED_STRING
error_desc : ESCAPED_STRING
@@ -38,6 +38,9 @@ value : ESCAPED_STRING
| BOOL
| VALUE
+FLIP_EXPR : "+"
+ | "-"
+
EQUALITY_OP : "is"
| "is not"
diff --git a/mc_openapi/doml_mc/dsl_parser/parser.ipynb b/mc_openapi/doml_mc/dsl_parser/parser.ipynb
index 94d6654260dbe2c457f506c7edaf7849d82975af..4ae7cbbe91883c9a2760e51f1ee048fbeb213ceb 100644
--- a/mc_openapi/doml_mc/dsl_parser/parser.ipynb
+++ b/mc_openapi/doml_mc/dsl_parser/parser.ipynb
@@ -37,7 +37,7 @@
"# )\n",
"\n",
"expr_to_parse = r\"\"\"\n",
- "> \"example requirement to test\"\n",
+ "- \"example requirement to test\"\n",
" # Expr to parse\n",
" not vm is class infrastructure.VirtualMachine\n",
" and\n",
@@ -57,7 +57,7 @@
" ---\n",
" \"Virtual Machine {vm} has no iface\"\n",
"\n",
- " > \"example requirement to test\"\n",
+ "+ \"example requirement to test\"\n",
" # Expr to parse\n",
" not vm is class infrastructure.VirtualMachine\n",
" and\n",
@@ -84,6 +84,7 @@
"text": [
"requirements\n",
" requirement\n",
+ " -\n",
" req_name\t\"example requirement to test\"\n",
" iff_expr\n",
" and_expr\n",
@@ -123,6 +124,7 @@
" value\ttrue\n",
" error_desc\t\"Virtual Machine {vm} has no iface\"\n",
" requirement\n",
+ " -\n",
" req_name\t\"example requirement to test\"\n",
" iff_expr\n",
" and_expr\n",
@@ -177,15 +179,7 @@
"cell_type": "code",
"execution_count": 4,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "{'web', 'handle_image', 'http', 'bucket_in', 'vpc_subnet', 'ssh_key', '/tmp/ssh_key_file', 'INGRESS', 'bucket_name', 'path/web_app', 'lambda_memory', 'concrete_f', 'c', 'st2', 'aws', 'st1', '0.0.0.0/0', 'v_img', 'IMAGE', 'sg', 's3_bucket_out', 'RSA', 'ssh', 'python3.8', 't2.micro', 'lambda_handler', 'ImageResizeApp', 'instance_type', 'vm1', 'ami-xxxxxxxxxxxxxxxxx', 'storage_interface', 'f', 'SCRIPT', 's1', 'i1', 'tcp', 'c_img', 'concrete_net', 'con_infra', 's2', 'demo-key', 'source_code', 'infra', 'https', 's3_bucket_in', 'lambda_runtime', 'image_resize', 'ssh_key_name', 'lambda_timeout', 'ec2-user', 'demo-ec2-role', 'ec2_role_name', 'vpc', 'bucket_out', 'EGRESS', 'tcp/ip', 'eu-central-1', 'icmp', 'concrete_vm', 'lambda_role_name', 'notification', 'path/lambda/function/image_resize.py', 'DemoLambdaRole', 'web-app:0.1.0', 'image_resize.lambda_handler', 'config1'}\n"
- ]
- }
- ],
+ "outputs": [],
"source": [
"from mc_openapi.doml_mc import ModelChecker, DOMLVersion\n",
"from mc_openapi.doml_mc.imc import IntermediateModelChecker\n",
@@ -220,14 +214,16 @@
"name": "stdout",
"output_type": "stream",
"text": [
- "[Requirement(assert_callable=<function DSLTransformer.iff_expr.<locals>.<lambda> at 0x7f64681feb90>,\n",
+ "[Requirement(assert_callable=<function DSLTransformer.iff_expr.<locals>.<lambda> at 0x7f5060012e60>,\n",
" assert_name='example_requirement_to_test',\n",
" description='example requirement to test',\n",
- " error_description=<function DSLTransformer.requirement.<locals>.<lambda> at 0x7f64681fea70>),\n",
- " Requirement(assert_callable=<function DSLTransformer.iff_expr.<locals>.<lambda> at 0x7f64681fe170>,\n",
+ " error_description=<function DSLTransformer.requirement.<locals>.<lambda> at 0x7f50600128c0>,\n",
+ " flipped=True),\n",
+ " Requirement(assert_callable=<function DSLTransformer.iff_expr.<locals>.<lambda> at 0x7f5060011fc0>,\n",
" assert_name='example_requirement_to_test',\n",
" description='example requirement to test',\n",
- " error_description=<function DSLTransformer.requirement.<locals>.<lambda> at 0x7f64681fe050>)]\n"
+ " error_description=<function DSLTransformer.requirement.<locals>.<lambda> at 0x7f5060012320>,\n",
+ " flipped=True)]\n"
]
}
],
@@ -248,15 +244,7 @@
"cell_type": "code",
"execution_count": 6,
"metadata": {},
- "outputs": [
- {
- "name": "stdout",
- "output_type": "stream",
- "text": [
- "{'web', 'handle_image', 'http', 'bucket_in', 'vpc_subnet', 'ssh_key', '/tmp/ssh_key_file', 'INGRESS', 'bucket_name', 'path/web_app', 'lambda_memory', 'concrete_f', 'c', 'st2', 'aws', 'st1', '0.0.0.0/0', 'v_img', 'IMAGE', 'sg', 's3_bucket_out', 'RSA', 'ssh', 'python3.8', 't2.micro', 'lambda_handler', '\"linux\"', 'ImageResizeApp', 'instance_type', 'vm1', 'ami-xxxxxxxxxxxxxxxxx', 'storage_interface', 'f', 'SCRIPT', 's1', 'i1', 'tcp', 'c_img', 'concrete_net', 'con_infra', 's2', 'demo-key', 'source_code', 'infra', 'https', 's3_bucket_in', 'lambda_runtime', 'image_resize', 'ssh_key_name', 'lambda_timeout', 'ec2-user', 'demo-ec2-role', 'ec2_role_name', 'vpc', 'bucket_out', 'EGRESS', 'tcp/ip', 'eu-central-1', 'icmp', 'concrete_vm', 'lambda_role_name', 'notification', 'path/lambda/function/image_resize.py', 'DemoLambdaRole', 'web-app:0.1.0', 'image_resize.lambda_handler', 'config1'}\n"
- ]
- }
- ],
+ "outputs": [],
"source": [
"intermediate_model_checker.instantiate_solver(user_value_strings)\n",
"ENCODINGS = intermediate_model_checker.smt_encoding\n",
@@ -293,7 +281,7 @@
" int(1024)),\n",
" attribute(vm,\n",
" infrastructure_ComputingNode::architecture,\n",
- " ss(ss_26__linux_)),\n",
+ " ss(ss_5__linux_)),\n",
" attribute(vm,\n",
" application_SoftwareComponent::isPersistent,\n",
" bool(True)))))\n",
diff --git a/mc_openapi/doml_mc/dsl_parser/parser.py b/mc_openapi/doml_mc/dsl_parser/parser.py
index d02c7eed453acfb789317e63459fa0b54b15ffa5..2d6b7a703404d2f5fbec0cbfaa29548e00b27cb2 100644
--- a/mc_openapi/doml_mc/dsl_parser/parser.py
+++ b/mc_openapi/doml_mc/dsl_parser/parser.py
@@ -48,14 +48,16 @@ class DSLTransformer(Transformer):
return args
def requirement(self, args) -> Requirement:
- name: str = args[0]
- expr: Callable[[SMTEncoding, SMTSorts], ExprRef] = args[1]
- errd: Callable[[Solver, SMTSorts, IntermediateModel, int], str] = args[2]
+ flip_expr: bool = args[0].value == "-"
+ name: str = args[1]
+ expr: Callable[[SMTEncoding, SMTSorts], ExprRef] = args[2]
+ errd: Callable[[Solver, SMTSorts, IntermediateModel, int], str] = args[3]
return Requirement(
expr,
name.lower().replace(" ", "_"),
name,
- lambda solver, sorts, model: errd(solver, sorts, model, self.const_store.get_index_and_push())
+ lambda solver, sorts, model: errd(solver, sorts, model, self.const_store.get_index_and_push()),
+ flipped=flip_expr
)
def req_name(self, args) -> str:
diff --git a/mc_openapi/doml_mc/imc.py b/mc_openapi/doml_mc/imc.py
index b3ad342f8b92fba0bab38e291502100bebbf1219..684918d93c53e845a793af8b504b03132588eea8 100644
--- a/mc_openapi/doml_mc/imc.py
+++ b/mc_openapi/doml_mc/imc.py
@@ -1,25 +1,22 @@
from collections.abc import Callable
from dataclasses import dataclass
-from z3 import (
- Context, FuncDeclRef, Solver, ExprRef, SortRef, DatatypeSortRef, sat
-)
+from z3 import (Context, DatatypeSortRef, ExprRef, FuncDeclRef, Solver,
+ SortRef, sat)
from .intermediate_model.doml_element import IntermediateModel
-from .z3encoding.im_encoding import (
- assert_im_associations_q, assert_im_attributes,
- def_elem_class_f_and_assert_classes,
- mk_elem_sort_dict, mk_stringsym_sort_dict
-)
-from .z3encoding.metamodel_encoding import (
- def_association_rel,
- def_attribute_rel,
- mk_association_sort_dict,
- mk_attribute_sort_dict, mk_class_sort_dict
-)
+from .mc_result import MCResult, MCResults
+from .z3encoding.im_encoding import (assert_im_associations_q,
+ assert_im_attributes,
+ def_elem_class_f_and_assert_classes,
+ mk_elem_sort_dict, mk_stringsym_sort_dict)
+from .z3encoding.metamodel_encoding import (def_association_rel,
+ def_attribute_rel,
+ mk_association_sort_dict,
+ mk_attribute_sort_dict,
+ mk_class_sort_dict)
from .z3encoding.types import Refs
from .z3encoding.utils import mk_attr_data_sort
-from .mc_result import MCResult, MCResults
@dataclass
@@ -50,7 +47,7 @@ class Requirement:
assert_name: str
description: str
error_description: Callable[[Solver, SMTSorts, IntermediateModel], str]
-
+ flipped: bool = False
class RequirementStore:
def __init__(self, requirements: list[Requirement]):
@@ -159,7 +156,7 @@ class IntermediateModelChecker:
)
res = self.solver.check()
results.append((
- MCResult.from_z3result(res, flipped=True),
+ MCResult.from_z3result(res, flipped=req.flipped),
req.error_description(self.solver, self.smt_sorts, self.intermediate_model)
if res == sat else ""
))
diff --git a/tests/req_dsl/example_multiple_reqs.dsl b/tests/req_dsl/example_multiple_reqs.dsl
index e5c0ab6e9c3a8eda7f5b2fe6523ae31b6a941ac0..9da237a0a067af5c485da738f78c1e67fe6a8086 100644
--- a/tests/req_dsl/example_multiple_reqs.dsl
+++ b/tests/req_dsl/example_multiple_reqs.dsl
@@ -9,7 +9,7 @@
# )
# )
-> "Something that will be unsatisfiable"
+- "Something that will be unsatisfiable"
vm is class infrastructure.VirtualMachine
and
not exists iface (
@@ -32,7 +32,7 @@
---
"VM {vm} has some problems."
-> "All VMs have at least one interface 2"
+- "All VMs have at least one interface 2"
vm is class infrastructure.VirtualMachine
and
not exists iface (
@@ -41,7 +41,7 @@
---
"VM {vm} has no associated interface."
-> "All VMs have at least one interface 3"
++ "All VMs have at least one interface 3"
vm is class infrastructure.VirtualMachine
and
exists iface (
diff --git a/tests/req_dsl/example_single_req.dsl b/tests/req_dsl/example_single_req.dsl
index 908eaf690888da3b576431dfdb69829f6ee22511..9c9a5b3ff7a1bd7bbcb69b07bcc561f1b688f467 100644
--- a/tests/req_dsl/example_single_req.dsl
+++ b/tests/req_dsl/example_single_req.dsl
@@ -9,7 +9,7 @@
# )
# )
-> "All VMs have at least one interface 1"
+- "All VMs have at least one interface 1"
vm is class infrastructure.VirtualMachine
and
not exists iface (