Exclude link condition from link expression

Fixes #277
AdaCore · Jun 6, 2020 · c955625 · c955625
1 parent 1203586
commit c955625
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 2 deletions.
diff --git a/rflx/model.py b/rflx/model.py
@@ -637,11 +637,12 @@ def has_final(field: Field) -> bool:
             errors = []
             for path in self.__paths[f]:
                 facts = [fact for link in path for fact in self.__link_expression(link)]
+                conditions = [link.condition for link in path]
                 if f != FINAL:
                     facts.extend(
                         expression_list(Or(*[o.condition for o in self.outgoing(f)]).simplified())
                     )
-                proof = TRUE.check(facts)
+                proof = TRUE.check([*facts, *conditions])
                 if proof.result == ProofResult.sat:
                     break
 
@@ -695,7 +696,6 @@ def __link_expression(self, link: Link) -> Sequence[Expr]:
             GreaterEqual(Last("Message"), Last(name)),
             GreaterEqual(Last("Message"), First("Message")),
             Equal(Length("Message"), Add(Sub(Last("Message"), First("Message")), Number(1)),),
-            *expression_list(link.condition),
         ]
 
     def __prove_field_positions(self) -> None:

diff --git a/tests/test_verification.py b/tests/test_verification.py
@@ -880,3 +880,26 @@ def test_aggregate_equal_invalid_length_field() -> None:
         r'^contradicting condition 0 from field "Magic" to "Final"'
         r' on path \[Length -> Magic\] in "P.M"',
     )
+
+
+def test_no_contradiction_multi() -> None:
+    structure = [
+        Link(INITIAL, Field("F0")),
+        Link(Field("F0"), Field("F1"), condition=Equal(Variable("F0"), Number(1))),
+        Link(Field("F0"), Field("F2"), condition=Equal(Variable("F0"), Number(2))),
+        Link(Field("F1"), Field("F3")),
+        Link(Field("F2"), Field("F3")),
+        Link(Field("F3"), Field("F4"), condition=Equal(Variable("F0"), Number(1))),
+        Link(Field("F3"), Field("F5"), condition=Equal(Variable("F0"), Number(2))),
+        Link(Field("F4"), FINAL),
+        Link(Field("F5"), FINAL),
+    ]
+    types = {
+        Field("F0"): RANGE_INTEGER,
+        Field("F1"): RANGE_INTEGER,
+        Field("F2"): RANGE_INTEGER,
+        Field("F3"): RANGE_INTEGER,
+        Field("F4"): RANGE_INTEGER,
+        Field("F5"): RANGE_INTEGER,
+    }
+    Message("P.M", structure, types)