final touches

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

Author: muenchnerkindl

specifications/ewd687a/EWD687a.tla

@@ -377,13 +377,13 @@ RcvMsg(p) == \E e \in InEdges(p) :
                   /\ UNCHANGED <<acks, sentUnacked>>
 
 (***************************************************************************)
-(* A process p may finish its computation and become idle at any time.     *)
+(* An active process p may become idle at any time.                        *)
 (*                                                                         *)
-(* If a non-leader process p is neutral after an idle step, it implies     *)
-(* that p was not a node of the overlay tree when it became idle.  Thus,   *)
-(* there is no need to change upEdge[p] in the  Idle  subaction.           *)
+(* Since p is active before the step, it must be a node of the overlay     *)
+(* tree. If it is a leaf, it can be removed from the tree in a subsequent  *)
+(* SendAck transition.                                                     *)
 (***************************************************************************)
-Idle(p) == /\ active[p]  \* otherwise this step is subsumed by stuttering
+Idle(p) == /\ active[p]
            /\ active' = [active EXCEPT ![p] = FALSE]
            /\ UNCHANGED <<msgs, acks, sentUnacked, rcvdUnacked, upEdge>>
 
@@ -419,9 +419,7 @@ THEOREM Spec => []CountersConsistent
 
 TreeWithRoot ==
     LET E == {upEdge[p] : p \in DOMAIN upEdge} \ {NotAnEdge}
-        \* The original definition includes every node occurring in the tree
-        \* twice (except the leader), which unnecessarily complicates the proof.
-        N == (* {e[1] : e \in E} \cup *) {e[2] : e \in E} \cup {Leader}
+        N == {e[2] : e \in E} \cup {Leader}
         O == Transpose([edge |-> E, node |-> N])
     IN \* O is a tree rooted in the leader.
        /\ IsTreeWithRoot(O, Leader)

specifications/ewd687a/EWD687a_anim.cfg

@@ -35,6 +35,3 @@ ALIAS
 CHECK_DEADLOCK
     FALSE
 
-ACTION_CONSTRAINT
-    NoSuperfluousIdleSteps
-

specifications/ewd687a/EWD687a_anim.tla

@@ -160,11 +160,6 @@ InterestingBehavior ==
     \* 30 states with the Leader neutral in the final state.
     TLCGet("level") > 20 => ~neutral(Leader)
 
-NoSuperfluousIdleSteps ==
-    \* Disable Idle steps that leave the variables unchange (an idle process becoming idle)
-    \* to prevent finite stuttering when simulating.
-    ~UNCHANGED vars
-
 ----------------------------------------------------------------------------
 
 \* Processes.

specifications/ewd687a/MCEWD687a.cfg

@@ -1,11 +1,10 @@
 CONSTANTS
     \* model values for processes
-    L = L
+    Leader = Leader
     P1 = P1
     P2 = P2
     P3 = P3
     MaxCounter = 3
-    Leader = L
     Procs <- MCProcs
     Edges <- MCEdges
 

specifications/ewd687a/MCEWD687a.tla

@@ -2,12 +2,12 @@
 EXTENDS EWD687a, TLC
 
 CONSTANTS 
-    L, P1, P2, P3, \* constants representing the processes in the MC instance
-    MaxCounter     \* bound on counter values
+    P1, P2, P3, \* constants representing the non-leader processes in the MC instance
+    MaxCounter  \* bound on counter values
 
-MCProcs == {L, P1, P2, P3}
+MCProcs == {Leader, P1, P2, P3}
 MCEdges == 
-    {<<L, P1>>, <<P1, P2>>, <<P1, P2>>, <<P2, P1>>, <<P2,P3>>}
+    {<<Leader, P1>>, <<P1, P2>>, <<P1, P2>>, <<P2, P1>>, <<P2,P3>>}
 
 StateConstraint == \A e \in Edges : 
     /\ msgs[e] < MaxCounter