"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

@@ -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,   *)

specifications/ewd687a/EWD687a_anim.cfg

@@ -25,7 +25,7 @@ INVARIANT
 
 PROPERTY
     DT2
-    \* DifferenceZero
+    \* CountersConsistent
     \* TreeWithRoot
     \* StableUpEdge
 

specifications/ewd687a/MCEWD687a.cfg

@@ -38,7 +38,7 @@ PROPERTY
     DT2
 
 PROPERTIES  
-    DifferenceZero
+    CountersConsistent
     TreeWithRoot
     \* StableUpEdge