From df7f09914394b4a4a2375b83945c6ca04dd0acaa Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Wed, 6 Dec 2023 10:27:11 -0800 Subject: [PATCH] "The DifferenceZero property does not match the comment. The property should ensure that the number of sentUnacked messages equals the sum of msgs and acks for any edge, not the difference being zero." --- specifications/ewd687a/EWD687a.tla | 12 ++++++------ specifications/ewd687a/EWD687a_anim.cfg | 2 +- specifications/ewd687a/MCEWD687a.cfg | 2 +- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/specifications/ewd687a/EWD687a.tla b/specifications/ewd687a/EWD687a.tla index fa7314c9..b0693bea 100644 --- a/specifications/ewd687a/EWD687a.tla +++ b/specifications/ewd687a/EWD687a.tla @@ -395,14 +395,14 @@ Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ---------------------------------------------------------------------------- (***************************************************************************) -(* Messages are never lost, thus, the difference of msgs[e], acks[e], *) -(* sentUnacked[e], and rcvdUnacked[e] for any e in Edges is always zero. *) +(* EWd687a assumes messages are not lost. Thus, the four counters always *) +(* have to be consistent, i.e., the sum of msgs[e], acks[e], and *) +(* rcvdUnacked[e] equals sentUnacked[e], for any e in Edges. *) (***************************************************************************) -DifferenceZero == - [] \A e \in Edges: - (sentUnacked[e] - msgs[e] - rcvdUnacked[e] - acks[e]) = 0 +CountersConsistent == + [] \A e \in Edges: sentUnacked[e] = rcvdUnacked[e] + acks[e] + msgs[e] -THEOREM Spec => DifferenceZero +THEOREM Spec => CountersConsistent (***************************************************************************) (* The overlay tree is a tree of non-neutral nodes rooted in the leader, *) diff --git a/specifications/ewd687a/EWD687a_anim.cfg b/specifications/ewd687a/EWD687a_anim.cfg index deb43e01..37f4a1fc 100644 --- a/specifications/ewd687a/EWD687a_anim.cfg +++ b/specifications/ewd687a/EWD687a_anim.cfg @@ -25,7 +25,7 @@ INVARIANT PROPERTY DT2 - \* DifferenceZero + \* CountersConsistent \* TreeWithRoot \* StableUpEdge diff --git a/specifications/ewd687a/MCEWD687a.cfg b/specifications/ewd687a/MCEWD687a.cfg index 7c63089e..ffe26374 100644 --- a/specifications/ewd687a/MCEWD687a.cfg +++ b/specifications/ewd687a/MCEWD687a.cfg @@ -38,7 +38,7 @@ PROPERTY DT2 PROPERTIES - DifferenceZero + CountersConsistent TreeWithRoot \* StableUpEdge