X Adjust ME!Liveness to require that a proc is either stuck in non-cs or keeps on entering cs

See MutualExclusionSpec.tla

1Bit.tla

@@ -7,9 +7,10 @@ ASSUME N \in Nat
 
 Procs == 0..N
 
+         
 \* PlusCal options (wf)
 (********
---fair algorithm 1BitProtocol {
+--algorithm 1BitProtocol {
     variables flag = [i \in Procs |-> FALSE], turn = 0 ;
     process (P \in Procs) {
      ncs: while (TRUE) {
@@ -31,7 +32,7 @@ Procs == 0..N
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "55b6bf32")
+\* BEGIN TRANSLATION (chksum(pcal) = "5149a336" /\ chksum(tla) = "c5e4a370")
 VARIABLES flag, turn, pc
 
 vars == << flag, turn, pc >>
@@ -91,7 +92,6 @@ P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(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 
@@ -116,5 +116,5 @@ THEOREM Spec => ME!Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Feb 09 22:17:21 MSK 2022 by kirr
+\* Last modified Wed Feb 09 22:19:36 MSK 2022 by kirr
 \* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

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

1Bit.toolbox/1Bit___Model_1_SnapShot_1644433283403.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644434389260.launch

@@ -3,7 +3,7 @@
     <stringAttribute key="TLCCmdLineParameters" value=""/>
     <stringAttribute key="alias" value=""/>
     <intAttribute key="collectCoverage" value="1"/>
-    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644433283403"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644434389260"/>
     <booleanAttribute key="deferLiveness" value="false"/>
     <intAttribute key="dfidDepth" value="100"/>
     <booleanAttribute key="dfidMode" value="false"/>
@@ -13,7 +13,7 @@
     <stringAttribute key="distributedTLC" value="off"/>
     <stringAttribute key="distributedTLCVMArgs" value=""/>
     <intAttribute key="fpBits" value="1"/>
-    <intAttribute key="fpIndex" value="38"/>
+    <intAttribute key="fpIndex" value="16"/>
     <booleanAttribute key="fpIndexRandom" value="true"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <intAttribute key="maxSetSize" value="1000000"/>
@@ -22,16 +22,16 @@
     <stringAttribute key="modelBehaviorNext" value=""/>
     <stringAttribute key="modelBehaviorSpec" value="Spec"/>
     <intAttribute key="modelBehaviorSpecType" value="1"/>
-    <stringAttribute key="modelBehaviorVars" value="flag, pc"/>
+    <stringAttribute key="modelBehaviorVars" value="flag, pc, turn"/>
     <stringAttribute key="modelComments" value=""/>
     <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
     <listAttribute key="modelCorrectnessInvariants">
         <listEntry value="1ME!MutualExclusion"/>
-        <listEntry value="1Inv"/>
+        <listEntry value="0Inv"/>
     </listAttribute>
     <listAttribute key="modelCorrectnessProperties">
         <listEntry value="1ME!Spec"/>
-        <listEntry value="0ME!Liveness"/>
+        <listEntry value="1ME!Liveness"/>
     </listAttribute>
     <intAttribute key="modelEditorOpenTabs" value="8"/>
     <stringAttribute key="modelExpressionEval" value=""/>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644433275573.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644486204136.launch

@@ -3,7 +3,7 @@
     <stringAttribute key="TLCCmdLineParameters" value=""/>
     <stringAttribute key="alias" value=""/>
     <intAttribute key="collectCoverage" value="1"/>
-    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644433275573"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644486204136"/>
     <booleanAttribute key="deferLiveness" value="false"/>
     <intAttribute key="dfidDepth" value="100"/>
     <booleanAttribute key="dfidMode" value="false"/>
@@ -13,7 +13,7 @@
     <stringAttribute key="distributedTLC" value="off"/>
     <stringAttribute key="distributedTLCVMArgs" value=""/>
     <intAttribute key="fpBits" value="1"/>
-    <intAttribute key="fpIndex" value="87"/>
+    <intAttribute key="fpIndex" value="77"/>
     <booleanAttribute key="fpIndexRandom" value="true"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <intAttribute key="maxSetSize" value="1000000"/>
@@ -22,16 +22,16 @@
     <stringAttribute key="modelBehaviorNext" value=""/>
     <stringAttribute key="modelBehaviorSpec" value="Spec"/>
     <intAttribute key="modelBehaviorSpecType" value="1"/>
-    <stringAttribute key="modelBehaviorVars" value="flag, pc"/>
+    <stringAttribute key="modelBehaviorVars" value="flag, pc, turn"/>
     <stringAttribute key="modelComments" value=""/>
     <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
     <listAttribute key="modelCorrectnessInvariants">
         <listEntry value="1ME!MutualExclusion"/>
-        <listEntry value="1Inv"/>
+        <listEntry value="0Inv"/>
     </listAttribute>
     <listAttribute key="modelCorrectnessProperties">
-        <listEntry value="0ME!Spec"/>
-        <listEntry value="0ME!Liveness"/>
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
     </listAttribute>
     <intAttribute key="modelEditorOpenTabs" value="8"/>
     <stringAttribute key="modelExpressionEval" value=""/>

1Bit.toolbox/Model_1/1Bit.tla

@@ -7,9 +7,10 @@ ASSUME N \in Nat
 
 Procs == 0..N
 
+         
 \* PlusCal options (wf)
 (********
---fair algorithm 1BitProtocol {
+--algorithm 1BitProtocol {
     variables flag = [i \in Procs |-> FALSE], turn = 0 ;
     process (P \in Procs) {
      ncs: while (TRUE) {
@@ -31,7 +32,7 @@ Procs == 0..N
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "55b6bf32")
+\* BEGIN TRANSLATION (chksum(pcal) = "5149a336" /\ chksum(tla) = "c5e4a370")
 VARIABLES flag, turn, pc
 
 vars == << flag, turn, pc >>
@@ -91,7 +92,6 @@ P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(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 
@@ -116,5 +116,5 @@ THEOREM Spec => ME!Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Feb 09 22:17:21 MSK 2022 by kirr
+\* Last modified Wed Feb 09 22:19:36 MSK 2022 by kirr
 \* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

1Bit.toolbox/Model_1/MC.cfg

 \* CONSTANT definitions
 
 CONSTANT
-    N <- const_1644434264801795000
+    N <- const_1644486201121915000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
 \* INVARIANT definition
 INVARIANT
-inv_1644434264801796000
+inv_1644486201121916000
 \* PROPERTY definition
 PROPERTY
-prop_1644434264801797000
-prop_1644434264801798000
-\* Generated on Wed Feb 09 22:17:44 MSK 2022
+prop_1644486201121917000
+prop_1644486201121918000
+\* Generated on Thu Feb 10 12:43:21 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1/MC.tla

@@ -2,22 +2,22 @@
 EXTENDS 1Bit, TLC
 
 \* CONSTANT definitions @modelParameterConstants:0N
-const_1644434264801795000 == 
+const_1644486201121915000 == 
 1
 ----
 
 \* INVARIANT definition @modelCorrectnessInvariants:0
-inv_1644434264801796000 ==
+inv_1644486201121916000 ==
 ME!MutualExclusion
 ----
 \* PROPERTY definition @modelCorrectnessProperties:0
-prop_1644434264801797000 ==
+prop_1644486201121917000 ==
 ME!Spec
 ----
 \* PROPERTY definition @modelCorrectnessProperties:1
-prop_1644434264801798000 ==
+prop_1644486201121918000 ==
 ME!Liveness
 ----
 =============================================================================
 \* Modification History
-\* Created Wed Feb 09 22:17:44 MSK 2022 by kirr
+\* Created Thu Feb 10 12:43:21 MSK 2022 by kirr

1Bit.toolbox/Model_1/MutualExclusionSpec.tla

@@ -51,6 +51,12 @@ Liveness == \A i \in Procs:
                     /\ (pc[i] = "csentry") ~> (pc[i] = "cs")
                     /\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
 
+\* XXX
+MELive == \A i \in Procs :
+                \/ <>[](pc[i] = "ncs")  \* stuck in non-cs
+                \/ []<>(pc[i] = "cs")   \* keeps on entering cs
+
+
 
 THEOREM Spec => []TypeOK        
 THEOREM Spec => []MutualExclusion
@@ -59,5 +65,5 @@ THEOREM Spec => Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Feb 09 19:11:11 MSK 2022 by kirr
+\* Last modified Thu Feb 10 12:43:05 MSK 2022 by kirr
 \* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644433275573/MC.cfg

-\* CONSTANT definitions
-
-CONSTANT
-    N <- const_1644433273561746000
-\* SPECIFICATION definition
-SPECIFICATION
-Spec
-\* INVARIANT definition
-INVARIANT
-inv_1644433273561747000
-Inv
-\* Generated on Wed Feb 09 22:01:13 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1_SnapShot_1644433275573/MC.tla

----- MODULE MC ----
-EXTENDS 1Bit, TLC
-
-\* CONSTANT definitions @modelParameterConstants:0N
-const_1644433273561746000 == 
-1
-----
-
-\* INVARIANT definition @modelCorrectnessInvariants:0
-inv_1644433273561747000 ==
-ME!MutualExclusion
-----
-=============================================================================
-\* Modification History
-\* Created Wed Feb 09 22:01:13 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644433283403/1Bit.tla → 1Bit.toolbox/Model_1_SnapShot_1644434389260/1Bit.tla

@@ -7,83 +7,92 @@ ASSUME N \in Nat
 
 Procs == 0..N
 
+         
+\* PlusCal options (wf)
 (********
---fair algorithm 1BitProtocol {
-    variables flag = [i \in Procs |-> FALSE] ;
+--algorithm 1BitProtocol {
+    variables flag = [i \in Procs |-> FALSE], turn = 0 ;
     process (P \in Procs) {
      ncs: while (TRUE) {
             skip ; 
      enter: flag[self] := TRUE ; 
         e2: if (flag[1-self]) {
-        e3:   if (self = 0) {
-                goto e2
+        e3:   if (self /= turn) {
+        e4:     flag[self] := FALSE;
+                goto e3;
               }
               else {
-                flag[self] := FALSE;
-        e4:     await ~flag[1-self];
                 goto enter;
               }
             };
         cs: skip ;
       exit: flag[self] := FALSE ;
+        x2: turn := 1-self;            
     }
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "fe37cc8e")
-VARIABLES flag, pc
+\* BEGIN TRANSLATION (chksum(pcal) = "5149a336" /\ chksum(tla) = "c5e4a370")
+VARIABLES flag, turn, pc
 
-vars == << flag, pc >>
+vars == << flag, turn, pc >>
 
 ProcSet == (Procs)
 
 Init == (* Global variables *)
         /\ flag = [i \in Procs |-> FALSE]
+        /\ turn = 0
         /\ pc = [self \in ProcSet |-> "ncs"]
 
 ncs(self) == /\ pc[self] = "ncs"
              /\ TRUE
              /\ pc' = [pc EXCEPT ![self] = "enter"]
-             /\ flag' = flag
+             /\ UNCHANGED << flag, turn >>
 
 enter(self) == /\ pc[self] = "enter"
                /\ flag' = [flag EXCEPT ![self] = TRUE]
                /\ pc' = [pc EXCEPT ![self] = "e2"]
+               /\ turn' = turn
 
 e2(self) == /\ pc[self] = "e2"
             /\ IF flag[1-self]
                   THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
                   ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
-            /\ flag' = flag
+            /\ UNCHANGED << flag, turn >>
 
 e3(self) == /\ pc[self] = "e3"
-            /\ IF self = 0
-                  THEN /\ pc' = [pc EXCEPT ![self] = "e2"]
-                       /\ flag' = flag
-                  ELSE /\ flag' = [flag EXCEPT ![self] = FALSE]
-                       /\ pc' = [pc EXCEPT ![self] = "e4"]
+            /\ IF self /= turn
+                  THEN /\ pc' = [pc EXCEPT ![self] = "e4"]
+                  ELSE /\ pc' = [pc EXCEPT ![self] = "enter"]
+            /\ UNCHANGED << flag, turn >>
 
 e4(self) == /\ pc[self] = "e4"
-            /\ ~flag[1-self]
-            /\ pc' = [pc EXCEPT ![self] = "enter"]
-            /\ flag' = flag
+            /\ flag' = [flag EXCEPT ![self] = FALSE]
+            /\ pc' = [pc EXCEPT ![self] = "e3"]
+            /\ turn' = turn
 
 cs(self) == /\ pc[self] = "cs"
             /\ TRUE
             /\ pc' = [pc EXCEPT ![self] = "exit"]
-            /\ flag' = flag
+            /\ UNCHANGED << flag, turn >>
 
 exit(self) == /\ pc[self] = "exit"
               /\ flag' = [flag EXCEPT ![self] = FALSE]
+              /\ pc' = [pc EXCEPT ![self] = "x2"]
+              /\ turn' = turn
+
+x2(self) == /\ pc[self] = "x2"
+            /\ turn' = 1-self
             /\ pc' = [pc EXCEPT ![self] = "ncs"]
+            /\ flag' = flag
 
 P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(self)
-              \/ cs(self) \/ exit(self)
+              \/ cs(self) \/ exit(self) \/ x2(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 
 
@@ -107,5 +116,5 @@ THEOREM Spec => ME!Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Feb 09 22:01:10 MSK 2022 by kirr
+\* Last modified Wed Feb 09 22:19:36 MSK 2022 by kirr
 \* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418501814/MC.cfg → 1Bit.toolbox/Model_1_SnapShot_1644434389260/MC.cfg

 \* CONSTANT definitions
 
 CONSTANT
-    Procs <- const_1644418499799475000
+    N <- const_1644434386227799000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
 \* INVARIANT definition
 INVARIANT
-inv_1644418499799476000
+inv_1644434386227800000
 \* PROPERTY definition
 PROPERTY
-prop_1644418499799477000
-prop_1644418499799478000
-\* Generated on Wed Feb 09 17:54:59 MSK 2022
+prop_1644434386227801000
+prop_1644434386227802000
+\* Generated on Wed Feb 09 22:19:46 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1_SnapShot_1644433283403/MC.tla → 1Bit.toolbox/Model_1_SnapShot_1644434389260/MC.tla

@@ -2,18 +2,22 @@
 EXTENDS 1Bit, TLC
 
 \* CONSTANT definitions @modelParameterConstants:0N
-const_1644433280678753000 == 
+const_1644434386227799000 == 
 1
 ----
 
 \* INVARIANT definition @modelCorrectnessInvariants:0
-inv_1644433280678754000 ==
+inv_1644434386227800000 ==
 ME!MutualExclusion
 ----
 \* PROPERTY definition @modelCorrectnessProperties:0
-prop_1644433280678756000 ==
+prop_1644434386227801000 ==
 ME!Spec
 ----
+\* PROPERTY definition @modelCorrectnessProperties:1
+prop_1644434386227802000 ==
+ME!Liveness
+----
 =============================================================================
 \* Modification History
-\* Created Wed Feb 09 22:01:20 MSK 2022 by kirr
+\* Created Wed Feb 09 22:19:46 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644433275573/1Bit.tla → 1Bit.toolbox/Model_1_SnapShot_1644486204136/1Bit.tla

@@ -7,83 +7,92 @@ ASSUME N \in Nat
 
 Procs == 0..N
 
+         
+\* PlusCal options (wf)
 (********
---fair algorithm 1BitProtocol {
-    variables flag = [i \in Procs |-> FALSE] ;
+--algorithm 1BitProtocol {
+    variables flag = [i \in Procs |-> FALSE], turn = 0 ;
     process (P \in Procs) {
      ncs: while (TRUE) {
             skip ; 
      enter: flag[self] := TRUE ; 
         e2: if (flag[1-self]) {
-        e3:   if (self = 0) {
-                goto e2
+        e3:   if (self /= turn) {
+        e4:     flag[self] := FALSE;
+                goto e3;
               }
               else {
-                flag[self] := FALSE;
-        e4:     await ~flag[1-self];
                 goto enter;
               }
             };
         cs: skip ;
       exit: flag[self] := FALSE ;
+        x2: turn := 1-self;            
     }
   }
 }
 ********)
-\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "fe37cc8e")
-VARIABLES flag, pc
+\* BEGIN TRANSLATION (chksum(pcal) = "5149a336" /\ chksum(tla) = "c5e4a370")
+VARIABLES flag, turn, pc
 
-vars == << flag, pc >>
+vars == << flag, turn, pc >>
 
 ProcSet == (Procs)
 
 Init == (* Global variables *)
         /\ flag = [i \in Procs |-> FALSE]
+        /\ turn = 0
         /\ pc = [self \in ProcSet |-> "ncs"]
 
 ncs(self) == /\ pc[self] = "ncs"
              /\ TRUE
              /\ pc' = [pc EXCEPT ![self] = "enter"]
-             /\ flag' = flag
+             /\ UNCHANGED << flag, turn >>
 
 enter(self) == /\ pc[self] = "enter"
                /\ flag' = [flag EXCEPT ![self] = TRUE]
                /\ pc' = [pc EXCEPT ![self] = "e2"]
+               /\ turn' = turn
 
 e2(self) == /\ pc[self] = "e2"
             /\ IF flag[1-self]
                   THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
                   ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
-            /\ flag' = flag
+            /\ UNCHANGED << flag, turn >>
 
 e3(self) == /\ pc[self] = "e3"
-            /\ IF self = 0
-                  THEN /\ pc' = [pc EXCEPT ![self] = "e2"]
-                       /\ flag' = flag
-                  ELSE /\ flag' = [flag EXCEPT ![self] = FALSE]
-                       /\ pc' = [pc EXCEPT ![self] = "e4"]
+            /\ IF self /= turn
+                  THEN /\ pc' = [pc EXCEPT ![self] = "e4"]
+                  ELSE /\ pc' = [pc EXCEPT ![self] = "enter"]
+            /\ UNCHANGED << flag, turn >>
 
 e4(self) == /\ pc[self] = "e4"
-            /\ ~flag[1-self]
-            /\ pc' = [pc EXCEPT ![self] = "enter"]
-            /\ flag' = flag
+            /\ flag' = [flag EXCEPT ![self] = FALSE]
+            /\ pc' = [pc EXCEPT ![self] = "e3"]
+            /\ turn' = turn
 
 cs(self) == /\ pc[self] = "cs"
             /\ TRUE
             /\ pc' = [pc EXCEPT ![self] = "exit"]
-            /\ flag' = flag
+            /\ UNCHANGED << flag, turn >>
 
 exit(self) == /\ pc[self] = "exit"
               /\ flag' = [flag EXCEPT ![self] = FALSE]
+              /\ pc' = [pc EXCEPT ![self] = "x2"]
+              /\ turn' = turn
+
+x2(self) == /\ pc[self] = "x2"
+            /\ turn' = 1-self
             /\ pc' = [pc EXCEPT ![self] = "ncs"]
+            /\ flag' = flag
 
 P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(self)
-              \/ cs(self) \/ exit(self)
+              \/ cs(self) \/ exit(self) \/ x2(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 
 
@@ -107,5 +116,5 @@ THEOREM Spec => ME!Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Wed Feb 09 22:01:10 MSK 2022 by kirr
+\* Last modified Wed Feb 09 22:19:36 MSK 2022 by kirr
 \* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418452332/MC.cfg → 1Bit.toolbox/Model_1_SnapShot_1644486204136/MC.cfg

 \* CONSTANT definitions
 
 CONSTANT
-    Procs <- const_1644418450318471000
+    N <- const_1644486201121915000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
 \* INVARIANT definition
 INVARIANT
-inv_1644418450318472000
+inv_1644486201121916000
 \* PROPERTY definition
 PROPERTY
-prop_1644418450318473000
-prop_1644418450318474000
-\* Generated on Wed Feb 09 17:54:10 MSK 2022
+prop_1644486201121917000
+prop_1644486201121918000
+\* Generated on Thu Feb 10 12:43:21 MSK 2022
\ No newline at end of file

Alternate.toolbox/Model_1_SnapShot_1644418927867/MC.tla → 1Bit.toolbox/Model_1_SnapShot_1644486204136/MC.tla

 ---- MODULE MC ----
-EXTENDS Alternate, TLC
+EXTENDS 1Bit, TLC
 
-\* CONSTANT definitions @modelParameterConstants:0Procs
-const_1644418925853479000 == 
-0..1
+\* CONSTANT definitions @modelParameterConstants:0N
+const_1644486201121915000 == 
+1
 ----
 
 \* INVARIANT definition @modelCorrectnessInvariants:0
-inv_1644418925853480000 ==
+inv_1644486201121916000 ==
 ME!MutualExclusion
 ----
 \* PROPERTY definition @modelCorrectnessProperties:0
-prop_1644418925854481000 ==
+prop_1644486201121917000 ==
 ME!Spec
 ----
 \* PROPERTY definition @modelCorrectnessProperties:1
-prop_1644418925854482000 ==
+prop_1644486201121918000 ==
 ME!Liveness
 ----
 =============================================================================
 \* Modification History
-\* Created Wed Feb 09 18:02:05 MSK 2022 by kirr
+\* Created Thu Feb 10 12:43:21 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644486204136/MutualExclusionSpec.tla

+------------------------ MODULE MutualExclusionSpec ------------------------
+\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
+
+\* Procs is set of processes.
+\* Every process is assumed to loop and enter into "cs" state on every interation.
+\* Non-critical state is represented as "non-cs".
+\* When process decides it want to enter into critical-section, it first goes into "csentry" state.
+CONSTANT Procs
+VARIABLES pc
+
+TypeOK == pc \in [Procs -> {"non-cs", "csentry", "cs"}]
+
+vars == <<pc>>
+
+\* All processes start from non-critical section.
+Init == pc \in [Procs -> {"non-cs"}]
+
+\* WantCS(proc) is action when proc decides that it wants to enter into critical section.
+WantCS(proc) ==
+        /\ pc[proc] = "non-cs"
+        /\ pc' = [pc EXCEPT ![proc] = "csentry"]
+
+\* EnterCS(proc) is action when proc enters critical section.
+EnterCS(proc) ==
+        /\ pc[proc] = "csentry"
+        /\ \A i \in Procs \ {proc} : pc[i] /= "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "cs"]
+        
+\* ExitCS(proc) is action when proc leaves critical section.
+ExitCS(proc) ==
+        /\ pc[proc] = "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "non-cs"]
+
+Next == \E i \in Procs: WantCS(i) \/ EnterCS(i) \/ ExitCS(i)
+
+
+Spec == /\ Init
+        /\ [][Next]_vars
+        /\ \A i \in Procs: (            \* fairness
+            \* not fair for WantCS - it can pause and even hang there
+            /\ SF_vars(EnterCS(i))
+            /\ SF_vars(ExitCS(i)))
+
+----------------
+
+\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
+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.
+Liveness == \A i \in Procs:
+                    /\ (pc[i] = "csentry") ~> (pc[i] = "cs")
+                    /\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
+
+\* XXX
+MELive == \A i \in Procs :
+                \/ <>[](pc[i] = "ncs")  \* stuck in non-cs
+                \/ []<>(pc[i] = "cs")   \* keeps on entering cs
+
+
+
+THEOREM Spec => []TypeOK        
+THEOREM Spec => []MutualExclusion
+THEOREM Spec => Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Thu Feb 10 12:43:05 MSK 2022 by kirr
+\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

1Bit.toolbox/MutualExclusionSpec.aux

+\relax 
+\gdef \@abspage@last{2}

Alternate.tla

@@ -83,7 +83,12 @@ THEOREM Spec => ME!Spec
 THEOREM Spec => []ME!MutualExclusion
 THEOREM Spec => ME!Liveness
 
+
+KeepsEnteringCS == \A i \in Procs : []<>(pc[i] = "cs")
+Stuck           == \E i \in Procs : <>[](pc[i] = "ncs")
+
+
 =============================================================================
 \* Modification History
-\* Last modified Wed Feb 09 19:58:34 MSK 2022 by kirr
+\* Last modified Thu Feb 10 12:42:40 MSK 2022 by kirr
 \* Created Wed Feb 09 16:13:49 MSK 2022 by kirr

Alternate.toolbox/Alternate.log

-This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9)  9 FEB 2022 20:01
+This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9)  10 FEB 2022 12:40
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -162,7 +162,7 @@ ts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
 mti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti7.p
 fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></us
 r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/latxfont/lasy10.pfb>
-Output written on Alternate.pdf (2 pages, 168869 bytes).
+Output written on Alternate.pdf (2 pages, 171121 bytes).
 PDF statistics:
  79 PDF objects out of 1000 (max. 8388607)
  57 compressed objects within 1 object stream

Alternate.toolbox/Alternate.tex

@@ -1089,7 +1089,24 @@
 \@x{ {\THEOREM} Spec \.{\implies} ME {\bang} Spec}%
 \@x{ {\THEOREM} Spec \.{\implies} {\Box} ME {\bang} MutualExclusion}%
 \@x{ {\THEOREM} Spec \.{\implies} ME {\bang} Liveness}%
+\@pvspace{16.0pt}%
+ \@x{ KeepsEnteringCS \.{\defeq} \A\, i \.{\in} Procs \.{:} {\Box} {\Diamond}
+ ( pc [ i ] \.{=}\@w{cs} )}%
+ \@x{ Stuck\@s{52.79} \.{\defeq} \E\, i \.{\in} Procs \.{:} {\Diamond} {\Box}
+ ( pc [ i ] \.{=}\@w{ncs} )}%
 \@pvspace{8.0pt}%
+\@x{ MELive \.{\defeq} \A\, i \.{\in} Procs \.{:}}%
+\@x{\@s{69.33} \.{\lor} {\Diamond} {\Box} ( pc [ i ] \.{=}\@w{ncs} )\@s{4.1}}%
+\@y{\@s{0}%
+ stuck in non-\ensuremath{cs
+}}%
+\@xx{}%
+\@x{\@s{69.33} \.{\lor} {\Box} {\Diamond} ( pc [ i ] \.{=}\@w{cs} )\@s{9.26}}%
+\@y{\@s{0}%
+ keeps on entering \ensuremath{cs
+}}%
+\@xx{}%
+\@pvspace{16.0pt}%
 \@x{}\bottombar\@xx{}%
 \setboolean{shading}{false}
 \begin{lcom}{0}%
@@ -1097,8 +1114,8 @@
 \ensuremath{\.{\,\backslash\,}\.{*}} Modification History
 \end{cpar}%
 \begin{cpar}{0}{F}{F}{0}{0}{}%
- \ensuremath{\.{\,\backslash\,}\.{*}} Last modified \ensuremath{Wed}
- \ensuremath{Feb} 09 19:58:34 \ensuremath{MSK} 2022 by \ensuremath{kirr
+ \ensuremath{\.{\,\backslash\,}\.{*}} Last modified \ensuremath{Thu}
+ \ensuremath{Feb} 10 12:40:56 \ensuremath{MSK} 2022 by \ensuremath{kirr
 }%
 \end{cpar}%
 \begin{cpar}{0}{F}{F}{0}{0}{}%

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="90"/>
+    <intAttribute key="fpIndex" value="117"/>
     <booleanAttribute key="fpIndexRandom" value="true"/>
     <intAttribute key="maxHeapSize" value="25"/>
     <intAttribute key="maxSetSize" value="1000000"/>
@@ -32,6 +32,8 @@
     <listAttribute key="modelCorrectnessProperties">
         <listEntry value="1ME!Spec"/>
         <listEntry value="1ME!Liveness"/>
+        <listEntry value="1KeepsEnteringCS"/>
+        <listEntry value="0Stuck"/>
     </listAttribute>
     <intAttribute key="modelEditorOpenTabs" value="8"/>
     <stringAttribute key="modelExpressionEval" value=""/>
@@ -49,6 +51,7 @@
     <intAttribute key="simuSeed" value="-1"/>
     <stringAttribute key="specName" value="Alternate"/>
     <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <listAttribute key="traceExploreExpressions"/>
     <stringAttribute key="view" value=""/>
     <booleanAttribute key="visualizeStateGraph" value="true"/>
 </launchConfiguration>