.

Alternate.tla

@@ -14,9 +14,9 @@ NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
 
 
 (********
---fair algorithm Alternate {
+--algorithm Alternate {
   variable turn \in Procs;
-  process (p \in Procs) {
+  fair process (p \in Procs) {
     ncs: while (TRUE) {
             skip;   \* non-critical section
 
@@ -30,7 +30,7 @@ NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
+\* BEGIN TRANSLATION (chksum(pcal) = "5d5d2a74" /\ chksum(tla) = "579f6ceb")
 VARIABLES turn, pc
 
 vars == << turn, pc >>
@@ -65,7 +65,7 @@ p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
 Next == (\E self \in Procs: p(self))
 
 Spec == /\ Init /\ [][Next]_vars
-        /\ WF_vars(Next)
+        /\ \A self \in Procs : WF_vars(p(self))
 
 \* END TRANSLATION 
 

Alternate.toolbox/Alternate___Model_1.launch

@@ -13,7 +13,7 @@
     <stringAttribute key="distributedTLC" value="off"/>
     <stringAttribute key="distributedTLCVMArgs" value=""/>
     <intAttribute key="fpBits" value="1"/>
-    <intAttribute key="fpIndex" value="26"/>
+    <intAttribute key="fpIndex" value="12"/>
     <booleanAttribute key="fpIndexRandom" value="true"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <intAttribute key="maxSetSize" value="1000000"/>