v04a02: Sanity-check with an Alias that nodes deactivate simultaneously

.github/workflows/main.yml

@@ -33,18 +33,6 @@ jobs:
         -Dutil.ExecutionStatisticsCollector.id=aabbcc60f238424fa70d124d0c77bbf1
         -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60
         -coverage 60 -tool -deadlock MCAsyncTerminationDetection
-    - name: Check EWD998 with TLC
-      run: >-
-        java -Dtlc2.TLC.stopAfter=1800 -Dtlc2.TLC.ide=Github
-        -Dutil.ExecutionStatisticsCollector.id=aabbcc60f238424fa70d124d0c77bbf1
-        -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60
-        -coverage 60 -tool -deadlock MCEWD998
-    - name: Check EWD998!IInv with TLC
-      run: >-
-        java -Dtlc2.TLC.stopAfter=1800 -Dtlc2.TLC.ide=Github
-        -Dutil.ExecutionStatisticsCollector.id=aabbcc60f238424fa70d124d0c77bbf1
-        -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60
-        -coverage 60 -tool -deadlock -config MCEWD998.tla MCEWD998
     - name: Get (nightly) Apalache
       run: wget https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz
     - name: Install Apalache

EWD998.tla

@@ -160,7 +160,7 @@ Deactivate ==
      \* 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
+    /\ active' # active
     /\ UNCHANGED <<pending, color, counter, token>>
 
 Environment == 

MCEWD998.cfg

@@ -2,5 +2,7 @@ CONSTANT N = 3
 SPECIFICATION Spec
 INVARIANT TypeOK
 INVARIANT Inv
-CONSTRAINT StateConstraint
-PROPERTY ATDSpec
+\* CONSTRAINT StateConstraint
+PROPERTY ATDSpec
+INVARIANT MaxDiameter
+ALIAS Alias

MCEWD998.tla

@@ -1,5 +1,5 @@
 ------------------------------- MODULE MCEWD998 -------------------------------
-EXTENDS EWD998
+EXTENDS EWD998, TLC
 
 (***************************************************************************)
 (* Bound the otherwise infinite state space that TLC has to check.         *)
@@ -8,6 +8,35 @@ StateConstraint ==
   /\ \A i \in Node : counter[i] < 3 /\ pending[i] < 3
   /\ token.q < 3
 
+-----------------------------------------------------------------------------
+
+\* Note that the non-property  TLCGet("level") < 42  combined with TLC's
+ \* simulator quickly triggers som "counter-example" for MCEWD998.
+MaxDiameter == TLCGet("level") < 42
+
+\* $ tlc -noTE -simulate -deadlock MCEWD998 | grep -A1 "sim = TRUE"
+Alias ==
+    [
+        active |-> active
+        ,color |-> color
+        ,counter |-> counter
+        ,pending |-> pending
+        ,token |-> token
+
+        \* Eye-ball test if some nodes simultaneously deactivate. Note that
+         \* the nodes deactive in the *successor* (primed) state.
+        ,sim |-> \E i,j \in Node:
+                        /\ i # j
+                        /\ active[i] # active[i]'
+                        /\ active[j] # active[j]'
+        \* Yes, one can prime  TLCGet("...")  in recent version of TLC! With it,
+         \* we account for the  sim  being true when the nodes deactivate in the
+         \* successor state.  Obviously, .name will be "Deactivate".
+        ,action |-> TLCGet("action")'.name
+    ]
+
+-----------------------------------------------------------------------------
+
 \* With TLC, checking  IInv /\ [Next]_vars => IInv'  translate to a config s.t.
  \*
  \*  CONSTANT N = 3