Fixes to make ci happy

.github/workflows/setup.sh

@@ -2,3 +2,6 @@
 
 # Get TLA⁺ tools
 wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -P "."
+# Get TLA⁺ community modules
+wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
+    -O "."

.github/workflows/wrapper.sh

@@ -1,8 +1,24 @@
 #!/usr/bin/env bash
+set -e
 # A small wrapper around TLC
-TLC_PATH=$1
-
-TLC_COMMAND="java -Dtlc2.TLC.stopAfter=180 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -tool -deadlock"
-find . -mindepth 1 -maxdepth 1 -type d '!' -exec test -e "{}/.ciignore" ';' -print | grep -v ".git" | xargs -n 1 "$TLC_COMMAND"
+# Add .ciignore file in a directory to ignore it.
 
+tlc="java -Dtlc2.TLC.stopAfter=180 \
+  -Dtlc2.TLC.ide=Github \
+  -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff \
+  -XX:+UseParallelGC \
+  -cp "tla2tools.jar:CommunityModules-deps.jar"  tlc2.TLC \
+  -workers auto \
+  -lncheck final \
+  -tool -modelcheck"
 
+find . -mindepth 1 -maxdepth 1 -type d '!' -exec test -e "{}/.ciignore" ';' -print | grep -v ".git" | while read -r dir; do
+  echo "Running $dir"
+  cd $dir
+  cfg_file=$(find "." -maxdepth 1 -type f -name "*.cfg" -print -quit)
+  tla_file=${cfg_file/.cfg/.tla}
+  ($tlc -config "$cfg_file" "$tla_file")
+  cd ../
+  echo "Finished checking $dir"
+done
+echo "Completed successfully."

2-phase-commit/2pc.tla

@@ -61,7 +61,7 @@ RM:
 
 }
 *)
-\* BEGIN TRANSLATION (chksum(pcal) = "3f73e87b" /\ chksum(tla) = "ad96144a")
+\* BEGIN TRANSLATION (chksum(pcal) = "c33de399" /\ chksum(tla) = "3f28490e")
 VARIABLES resourceManagerState, tmState, pc
 
 (* define statement *)
@@ -72,7 +72,7 @@ CanCommit == \A rm \in ResourceManagers :
 CanAbort == \A rm \in ResourceManagers :
                 resourceManagerState[rm] = StateAborted
 Inv == /\ \E rm1 \in ResourceManagers: resourceManagerState[rm1] \in {StateCommitted} => ~ \E rm2 \in ResourceManagers : resourceManagerState[rm2] \in {StateAborted}
-       /\ baitinv
+
 
 Terminate == \A rm \in ResourceManagers: resourceManagerState[rm] \in {StateCommitted, StateAborted}
 

lease-buggy-code/lease.tla

@@ -54,47 +54,42 @@ States == {StatesSleep, StatesWaitingLease, StatesDoingOperation, StatesRenewedL
     variables states = [x \in Workers |-> StatesWaitingLease];
     define {
         OnlyOneLeader == Cardinality({w \in DOMAIN (states): states[w] = StatesDoingOperation}) <= 1
-        TypeOk == \A w \in Workers: states[w] \in States
+        TypeOk == \A w \in Workers: states[w] \in States 
         Inv == /\ TypeOk
                /\ OnlyOneLeader
                \*/\ baitinv 
     }
 
-    macro stateIs(s) {
-        states[self] = s
-    }
-
     process (w \in Workers) {
 W:
         while(TRUE) {
             either {
                 \* If lease is expired, renew
-                await stateIs(StatesWaitingLease)
+                await states[self] = StatesWaitingLease;
                 await ~\E w \in Workers : states[w] = StatesDoingOperation \/ states[w] = StatesRenewedLease;
                 states[self] := StatesRenewedLease;
             } or {
                 \* Leader goes to sleep before start operation
-                await stateIs(StatesRenewedLease);
+                await states[self] = StatesRenewedLease;
                 \* this state is like saying that lease is expired.
                 states[self] := StatesSleep;
             } or {
                 \* Leader start the operation
-                await stateIs(StatesRenewedLease) \/ stateIs(StatesSleep);
+                await states[self] = StatesRenewedLease \/ states[self] = StatesSleep;
                 states[self] := StatesDoingOperation;
             } or {
                 \* Leader has completed the operation, no goes through the renew lease phase.
-                await stateIs(StatesDoingOperation);
+                await states[self] = StatesDoingOperation;
                 states[self] := StatesWaitingLease;
             }
         }
     }
 }*)
-\* BEGIN TRANSLATION (chksum(pcal) = "92808600" /\ chksum(tla) = "8f5050cf")
+\* BEGIN TRANSLATION (chksum(pcal) = "a482c2a" /\ chksum(tla) = "8f5050cf")
 VARIABLE states
 
 (* define statement *)
 OnlyOneLeader == Cardinality({w \in DOMAIN (states): states[w] = StatesDoingOperation}) <= 1
-
 TypeOk == \A w \in Workers: states[w] \in States
 Inv == /\ TypeOk
        /\ OnlyOneLeader

logical-clocks-and-mutual-exclusion/lamport_clock.cfg

@@ -3,7 +3,7 @@ SPECIFICATION Spec
 
 CONSTANTS 
     Processes = {0, 1}
-    ProcessCanFail = TRUE
+    ProcessCanFail = FALSE
     MaxTimestamp = 15
 INVARIANT  
     Inv

missionaries_and_cannibals_problem/.ciignore

@@ -0,0 +1 @@
+