.

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="96"/>
+    <intAttribute key="fpIndex" value="50"/>
     <booleanAttribute key="fpIndexRandom" value="true"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <intAttribute key="maxSetSize" value="1000000"/>

MutualExclusionSpec.tla

@@ -47,7 +47,7 @@ Spec == /\ Init
 MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
 
 \* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
-\* A process should keep on entering the critical-section unless it is stuck in it non-critical part.
+\* A process should keep on entering the critical-section unless it is stuck in its non-critical part.
 Liveness == \A i \in Procs:
                 /\
                     \/ <>[](pc[i] = "non-cs")                   \* either stuck in non-cs, or
@@ -61,5 +61,4 @@ THEOREM Spec => []TypeOK
 THEOREM Spec => []MutualExclusion
 THEOREM Spec => Liveness
 
-
 =============================================================================