diff --git a/mc_openapi/doml_mc/domlr_parser/parser.py b/mc_openapi/doml_mc/domlr_parser/parser.py index d5d3edbe74546ffc547d1c61b629b2b3b118ddef..ef34a540945fb720407f603e713b368a6f413465 100644 --- a/mc_openapi/doml_mc/domlr_parser/parser.py +++ b/mc_openapi/doml_mc/domlr_parser/parser.py @@ -178,7 +178,7 @@ class DOMLRTransformer(Transformer): return _gen_rel_elem_expr def rel_attr_value_expr(self, args): - """An ATTRIBUTE relationship""" + """An ATTRIBUTE relationship with a rhs that is a value""" rel_name = args[1].value def _gen_rel_attr_value_expr(enc: SMTEncoding, sorts: SMTSorts): @@ -219,15 +219,62 @@ class DOMLRTransformer(Transformer): return _gen_rel_attr_value_expr def rel_attr_elem_expr(self, args): - """Parse rhs of expression containing: - <, <=, >, >=, ==, != can be followed by a NUMBER - ==, != can be followed by a BOOL or STRING - should generate attr(e1, rel, attr_data_sort(VALUE)) for ==, != - or attr(e1, rel, val) and get_int(val) >= NUMBER + """An ATTRIBUTE relationship with a rhs that is another element""" - """ - print("rel_attr_elem_expr", args) - return args + rel1_name = args[1].value + rel2_name = args[4].value + op = args[2].value + + def _gen_rel_attr_elem_expr(enc: SMTEncoding, sorts: SMTSorts): + elem1 = RefHandler.get_const(args[0].value, sorts) + elem2 = RefHandler.get_const(args[3].value, sorts) + rel1, rel1_type = RefHandler.get_relationship(enc, rel1_name) + rel2, rel2_type = RefHandler.get_relationship(enc, rel2_name) + + assert rel1_type == RefHandler.ATTRIBUTE + assert rel2_type == RefHandler.ATTRIBUTE + + rhs_value = RefHandler.get_value("x", sorts) + + expr = And( + RefHandler.get_attribute_rel(enc, + elem1, + rel1, + rhs_value + ), + RefHandler.get_attribute_rel(enc, + elem2, + rel2, + rhs_value + ) + ) + if op == "==": + return expr + elif op == "!=": + return Not(expr) + else: + rhs1_value = RefHandler.get_value("rhs1", sorts) + rhs2_value = RefHandler.get_value("rhs2", sorts) + expr = And( + RefHandler.get_attribute_rel(enc, + elem1, + rel1, + rhs1_value + ), + RefHandler.get_attribute_rel(enc, + elem2, + rel2, + rhs2_value + ), + self.compare_int(sorts, op, rhs1_value, rhs2_value) + ) + print( + "Warning: Comparing attributes of two elements with {op} is experimental!\n", + "Assumption: the attribute is an Integer." + ) + return expr + + return _gen_rel_attr_elem_expr def _get_equality_sides(self, arg1, arg2): # We track use of const in const_or_class diff --git a/tests/domlr/example_single_req_qty_comparison.domlr b/tests/domlr/example_single_req_qty_comparison.domlr index 09e1f435d87dc0b9f1b21dde1b8b4e8000dfc0ef..9d7029dcc1b145e2d62a8885e81f3fc1aa564de7 100644 --- a/tests/domlr/example_single_req_qty_comparison.domlr +++ b/tests/domlr/example_single_req_qty_comparison.domlr @@ -9,16 +9,27 @@ # ) # ) +# OLD SYNTAX +# + "All VMs have at least 512 MB of memory" +# forall vm ( +# vm is class infrastructure.VirtualMachine +# implies +# ( +# vm has abstract.ComputingNode.memory_mb Mem +# and +# Mem < 512 +# ) +# ) + +# --- +# "All VMs have at least 256 MB of memory" + + "All VMs have at least 512 MB of memory" forall vm ( vm is class infrastructure.VirtualMachine - implies - ( - vm has abstract.ComputingNode.memory_mb Mem - and - Mem < 512 - ) + implies + vm has abstract.ComputingNode.memory_mb >= 512 + ) - --- - "All VMs have at least 256 MB of memory" + error: "All VMs have at least 256 MB of memory" \ No newline at end of file