From c95562573f40257ee4e370d7c0d055ce87576a1b Mon Sep 17 00:00:00 2001 From: Alexander Senier Date: Sat, 6 Jun 2020 01:05:29 +0200 Subject: [PATCH] Exclude link condition from link expression Fixes #277 --- rflx/model.py | 4 ++-- tests/test_verification.py | 23 +++++++++++++++++++++++ 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/rflx/model.py b/rflx/model.py index 948a351be7..f1d6f3e35c 100644 --- 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 index eb57bf5a5c..aca299b48e 100644 --- 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)