.

1Bit.tla

@@ -8,12 +8,12 @@ ASSUME N \in Nat
 Procs == 0..N
 
          
-\* PlusCal options (wf)
+
 (********
 --algorithm 1BitProtocol {
     variables flag = [i \in Procs |-> FALSE], turn = 0 ;
-    process (P \in Procs) {
-     ncs: while (TRUE) {
+    fair process (P \in Procs) {
+     ncs:- while (TRUE) {
             skip ; 
      enter: flag[self] := TRUE ; 
         e2: if (flag[1-self]) {
@@ -32,7 +32,7 @@ Procs == 0..N
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "5149a336" /\ chksum(tla) = "c5e4a370")
+\* BEGIN TRANSLATION (chksum(pcal) = "9162e634" /\ chksum(tla) = "3b0cd6ea")
 VARIABLES flag, turn, pc
 
 vars == << flag, turn, pc >>
@@ -92,7 +92,7 @@ P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(self)
 Next == (\E self \in Procs: P(self))
 
 Spec == /\ Init /\ [][Next]_vars
-        /\ \A self \in Procs : WF_vars(P(self))
+        /\ \A self \in Procs : WF_vars((pc[self] # "ncs") /\ P(self))
 
 \* END TRANSLATION 
 
@@ -108,6 +108,9 @@ ME == INSTANCE MutualExclusionSpec WITH
                 pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"             ->  "cs"
                                               [] pc[proc] \in {"enter","e2","e3","e4","e5"} ->  "csentry"
                                               [] OTHER                       ->  "non-cs"]
+                                              
+Live0 == (pc[0] = "enter") ~> (pc[0] = "cs")
+Live1 == (pc[1] = "enter") ~> (pc[1] = "cs")
 
 THEOREM Spec => ME!Spec
 THEOREM Spec => []ME!MutualExclusion

1Bit.toolbox/1Bit___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="64"/>
+    <intAttribute key="fpIndex" value="96"/>
     <booleanAttribute key="fpIndexRandom" value="true"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <intAttribute key="maxSetSize" value="1000000"/>
@@ -30,8 +30,8 @@
         <listEntry value="0Inv"/>
     </listAttribute>
     <listAttribute key="modelCorrectnessProperties">
-        <listEntry value="0ME!Spec"/>
-        <listEntry value="0ME!Liveness"/>
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
         <listEntry value="0Live0"/>
         <listEntry value="0Live1"/>
     </listAttribute>