v04a01: Let multiple (logical processes) nodes deactivate at the same…

… time/in the same step.

This breaks the refinement ATD => STD.

AsyncTerminationDetection.tla

@@ -126,15 +126,8 @@ TypeOK ==
 
 \* * Node i terminates.
 Terminate(i) ==
-    \* * Assuming active is a function (can we be sure?), function application
-     \* * is denoted by square brakets.  A mathmatician would expect parens, but TLA+
-     \* * uses parenthesis for (non-zero-arity) operator application.
-    \* * If node i is active *in this state*, it can terminate...
-    /\ active[i]
-    \* * ...in the next state (the prime operator ').
-    \* * The previous expression didn't say anything about the other values of the
-     \* * function, or even state that active' is a function (function update).
-    /\ active' = [ active EXCEPT ![i] = FALSE ]
+    \* Any subset of *active* nodes can become inactive in the next step.
+    /\ active' \in { f \in [ Node -> BOOLEAN] : \A n \in Node: ~active[n] => ~f[n] }
     \* * Also, the variable active is no longer unchanged.
     /\ pending' = pending
     \* * Possibly (but not necessarily) detect termination, iff all nodes are inactive

AsyncTerminationDetection_proof.tla

@@ -82,44 +82,44 @@ THEOREM Stability == Spec => Stable
 
 -----------------------------------------------------------------------------
 
-syncActive == [n \in Node |-> active[n] \/ pending[n] # 0]
+\* syncActive == [n \in Node |-> active[n] \/ pending[n] # 0]
 
-STD == INSTANCE SyncTerminationDetection WITH active <- syncActive
+\* STD == INSTANCE SyncTerminationDetection WITH active <- syncActive
 
-(***************************************************************************)
-(* We prove (the safety part of) refinement.                               *)
-(***************************************************************************)
+\* (***************************************************************************)
+\* (* We prove (the safety part of) refinement.                               *)
+\* (***************************************************************************)
 
-THEOREM Refinement == Spec => STD!Spec
-<1>. USE DEF Node, STD!Node, syncActive, terminated, STD!terminated
-<1>1. Init => STD!Init
-  BY NIsPosNat, Zenon DEF Init, STD!Init
-<1>2. TypeOK /\ Safe /\ [Next]_vars => [STD!Next]_(STD!vars)
-  <2> SUFFICES ASSUME TypeOK, Safe, [Next]_vars
-               PROVE  [STD!Next]_(STD!vars)
-    OBVIOUS
-  <2>. USE NIsPosNat DEF TypeOK, STD!Next, STD!vars
-  <2>1. CASE DetectTermination
-    BY <2>1, Zenon DEF DetectTermination, STD!DetectTermination
-  <2>2. ASSUME NEW i \in Node, Terminate(i)
-        PROVE  [STD!Next]_(STD!vars)
-    BY <2>2, Zenon DEF Terminate, STD!Terminate, Safe
-  <2>3. ASSUME NEW i \in Node, Wakeup(i)
-        PROVE  [STD!Next]_(STD!vars)
-    BY <2>3 DEF Wakeup
-  <2>4. ASSUME NEW i \in Node, NEW j \in Node, SendMsg(i, j)
-        PROVE  [STD!Next]_(STD!vars)
-    <3>1. syncActive[i] /\ UNCHANGED terminationDetected
-      BY <2>4 DEF SendMsg
-    <3>2. syncActive' = [syncActive EXCEPT ![j] = TRUE]
-      BY <2>4, Isa DEF SendMsg
-    <3>. QED  BY <3>1, <3>2, Zenon DEF STD!Wakeup
-  <2>5. CASE UNCHANGED vars
-    BY <2>5 DEF vars
-  <2>6. QED
-    BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next
-<1>3. Spec => WF_(STD!vars)(STD!DetectTermination)
-  OMITTED
-<1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, Safety, PTL DEF Spec, STD!Spec
+\* THEOREM Refinement == Spec => STD!Spec
+\* <1>. USE DEF Node, STD!Node, syncActive, terminated, STD!terminated
+\* <1>1. Init => STD!Init
+\*   BY NIsPosNat, Zenon DEF Init, STD!Init
+\* <1>2. TypeOK /\ Safe /\ [Next]_vars => [STD!Next]_(STD!vars)
+\*   <2> SUFFICES ASSUME TypeOK, Safe, [Next]_vars
+\*                PROVE  [STD!Next]_(STD!vars)
+\*     OBVIOUS
+\*   <2>. USE NIsPosNat DEF TypeOK, STD!Next, STD!vars
+\*   <2>1. CASE DetectTermination
+\*     BY <2>1, Zenon DEF DetectTermination, STD!DetectTermination
+\*   <2>2. ASSUME NEW i \in Node, Terminate(i)
+\*         PROVE  [STD!Next]_(STD!vars)
+\*     BY <2>2, Zenon DEF Terminate, STD!Terminate, Safe
+\*   <2>3. ASSUME NEW i \in Node, Wakeup(i)
+\*         PROVE  [STD!Next]_(STD!vars)
+\*     BY <2>3 DEF Wakeup
+\*   <2>4. ASSUME NEW i \in Node, NEW j \in Node, SendMsg(i, j)
+\*         PROVE  [STD!Next]_(STD!vars)
+\*     <3>1. syncActive[i] /\ UNCHANGED terminationDetected
+\*       BY <2>4 DEF SendMsg
+\*     <3>2. syncActive' = [syncActive EXCEPT ![j] = TRUE]
+\*       BY <2>4, Isa DEF SendMsg
+\*     <3>. QED  BY <3>1, <3>2, Zenon DEF STD!Wakeup
+\*   <2>5. CASE UNCHANGED vars
+\*     BY <2>5 DEF vars
+\*   <2>6. QED
+\*     BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next
+\* <1>3. Spec => WF_(STD!vars)(STD!DetectTermination)
+\*   OMITTED
+\* <1>. QED  BY <1>1, <1>2, <1>3, TypeCorrect, Safety, PTL DEF Spec, STD!Spec
 
 =============================================================================

EWD998.tla

@@ -152,16 +152,22 @@ RecvMsg(i) ==
     /\ UNCHANGED <<token>>
 
 \* Terminate(i) in AsyncTerminationDetection.
-Deactivate(i) ==
-    /\ active[i]
-    /\ active' = [active EXCEPT ![i] = FALSE]
+Deactivate ==
+    \* Modeling variant: Let multiple (logical processes) nodes deactivate at
+     \* the same time/in the same step. This breaks the refinement ATD => STD.
+     \* (Pick a function from the set of functions s.t. the inactive nodes in
+     \* the current step remain inactive and the active nodes in the current
+     \* step non-deterministically deactivate.)
+    /\ active' \in { f \in [ Node -> BOOLEAN] : \A n \in Node: ~active[n] => ~f[n] }
+    \* To avoid generating behaviors that quickly stutter when simulating the spec.
+    \* /\ active' # active
     /\ UNCHANGED <<pending, color, counter, token>>
 
 Environment == 
     \E n \in Node:
         \/ SendMsg(n)
         \/ RecvMsg(n)
-        \/ Deactivate(n)
+        \/ Deactivate
 
 -----------------------------------------------------------------------------