.

.gitignore

 *.toolbox/*_SnapShot_*
+
+*.toolbox/*.tex
+*.toolbox/*.pdf
+*.toolbox/*.log

MutualExclusionSpec.toolbox/Model_1/MC.cfg

@@ -5,7 +5,7 @@ p2 = p2
 \* MV CONSTANT definitions
 
 CONSTANT
-    Procs <- const_1644486704196931000
+    Procs <- const_1644486948532935000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
@@ -16,4 +16,4 @@ MutualExclusion
 \* PROPERTY definition
 PROPERTY
 Liveness
-\* Generated on Thu Feb 10 12:51:44 MSK 2022
+\* Generated on Thu Feb 10 12:55:48 MSK 2022
\ No newline at end of file

MutualExclusionSpec.toolbox/Model_1/MC.out

@@ -2,7 +2,7 @@
 TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
 @!@!@ENDMSG 2262 @!@!@
 @!@!@STARTMSG 2187:0 @!@!@
-Running breadth-first search Model-Checking with fp 85 and seed 3064238861429399640 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 89815] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+Running breadth-first search Model-Checking with fp 109 and seed 2286890076366813791 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 90203] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
 @!@!@ENDMSG 2187 @!@!@
 @!@!@STARTMSG 2220:0 @!@!@
 Starting SANY...
@@ -23,7 +23,7 @@ Semantic processing of module MC
 SANY finished.
 @!@!@ENDMSG 2219 @!@!@
 @!@!@STARTMSG 2185:0 @!@!@
-Starting... (2022-02-10 12:51:44)
+Starting... (2022-02-10 12:55:48)
 @!@!@ENDMSG 2185 @!@!@
 @!@!@STARTMSG 2212:0 @!@!@
 Implied-temporal checking--satisfiability problem has 5 branches.
@@ -32,16 +32,16 @@ Implied-temporal checking--satisfiability problem has 5 branches.
 Computing initial states...
 @!@!@ENDMSG 2189 @!@!@
 @!@!@STARTMSG 2190:0 @!@!@
-Finished computing initial states: 1 distinct state generated at 2022-02-10 12:51:45.
+Finished computing initial states: 1 distinct state generated at 2022-02-10 12:55:49.
 @!@!@ENDMSG 2190 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-Progress(4) at 2022-02-10 12:51:45: 15 states generated, 8 distinct states found, 0 states left on queue.
+Progress(4) at 2022-02-10 12:55:49: 15 states generated, 8 distinct states found, 0 states left on queue.
 @!@!@ENDMSG 2200 @!@!@
 @!@!@STARTMSG 2192:0 @!@!@
-Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:51:45)
+Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:55:49)
 @!@!@ENDMSG 2192 @!@!@
 @!@!@STARTMSG 2267:0 @!@!@
-Finished checking temporal properties in 00s at 2022-02-10 12:51:45
+Finished checking temporal properties in 00s at 2022-02-10 12:55:49
 @!@!@ENDMSG 2267 @!@!@
 @!@!@STARTMSG 2193:0 @!@!@
 Model checking completed. No error has been found.
@@ -50,7 +50,7 @@ Model checking completed. No error has been found.
   calculated (optimistic):  val = 3.0E-18
 @!@!@ENDMSG 2193 @!@!@
 @!@!@STARTMSG 2201:0 @!@!@
-The coverage statistics at 2022-02-10 12:51:45
+The coverage statistics at 2022-02-10 12:55:49
 @!@!@ENDMSG 2201 @!@!@
 @!@!@STARTMSG 2773:0 @!@!@
 <Init line 16, col 1 to line 16, col 4 of module MutualExclusionSpec>: 1:1
@@ -173,7 +173,7 @@ The coverage statistics at 2022-02-10 12:51:45
 End of statistics.
 @!@!@ENDMSG 2202 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-Progress(4) at 2022-02-10 12:51:45: 15 states generated (717 s/min), 8 distinct states found (382 ds/min), 0 states left on queue.
+Progress(4) at 2022-02-10 12:55:49: 15 states generated (725 s/min), 8 distinct states found (387 ds/min), 0 states left on queue.
 @!@!@ENDMSG 2200 @!@!@
 @!@!@STARTMSG 2199:0 @!@!@
 15 states generated, 8 distinct states found, 0 states left on queue.
@@ -185,5 +185,5 @@ The depth of the complete state graph search is 4.
 The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
 @!@!@ENDMSG 2268 @!@!@
 @!@!@STARTMSG 2186:0 @!@!@
-Finished in 1261ms at (2022-02-10 12:51:45)
+Finished in 1252ms at (2022-02-10 12:55:49)
 @!@!@ENDMSG 2186 @!@!@

MutualExclusionSpec.toolbox/Model_1/MC.tla

@@ -7,10 +7,10 @@ p1, p2
 ----
 
 \* MV CONSTANT definitions Procs
-const_1644486704196931000 == 
+const_1644486948532935000 == 
 {p1, p2}
 ----
 
 =============================================================================
 \* Modification History
-\* Created Thu Feb 10 12:51:44 MSK 2022 by kirr
+\* Created Thu Feb 10 12:55:48 MSK 2022 by kirr

MutualExclusionSpec.toolbox/Model_1/MC_TE.out

@@ -2,7 +2,7 @@
 TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
 @!@!@ENDMSG 2262 @!@!@
 @!@!@STARTMSG 2187:0 @!@!@
-Running breadth-first search Model-Checking with fp 85 and seed 3064238861429399640 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 89815] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+Running breadth-first search Model-Checking with fp 109 and seed 2286890076366813791 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 90203] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
 @!@!@ENDMSG 2187 @!@!@
 @!@!@STARTMSG 2220:0 @!@!@
 Starting SANY...
@@ -23,7 +23,7 @@ Semantic processing of module MC
 SANY finished.
 @!@!@ENDMSG 2219 @!@!@
 @!@!@STARTMSG 2185:0 @!@!@
-Starting... (2022-02-10 12:51:44)
+Starting... (2022-02-10 12:55:48)
 @!@!@ENDMSG 2185 @!@!@
 @!@!@STARTMSG 2212:0 @!@!@
 Implied-temporal checking--satisfiability problem has 5 branches.
@@ -32,16 +32,16 @@ Implied-temporal checking--satisfiability problem has 5 branches.
 Computing initial states...
 @!@!@ENDMSG 2189 @!@!@
 @!@!@STARTMSG 2190:0 @!@!@
-Finished computing initial states: 1 distinct state generated at 2022-02-10 12:51:45.
+Finished computing initial states: 1 distinct state generated at 2022-02-10 12:55:49.
 @!@!@ENDMSG 2190 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-Progress(4) at 2022-02-10 12:51:45: 15 states generated, 8 distinct states found, 0 states left on queue.
+Progress(4) at 2022-02-10 12:55:49: 15 states generated, 8 distinct states found, 0 states left on queue.
 @!@!@ENDMSG 2200 @!@!@
 @!@!@STARTMSG 2192:0 @!@!@
-Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:51:45)
+Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:55:49)
 @!@!@ENDMSG 2192 @!@!@
 @!@!@STARTMSG 2267:0 @!@!@
-Finished checking temporal properties in 00s at 2022-02-10 12:51:45
+Finished checking temporal properties in 00s at 2022-02-10 12:55:49
 @!@!@ENDMSG 2267 @!@!@
 @!@!@STARTMSG 2193:0 @!@!@
 Model checking completed. No error has been found.
@@ -50,7 +50,7 @@ Model checking completed. No error has been found.
   calculated (optimistic):  val = 3.0E-18
 @!@!@ENDMSG 2193 @!@!@
 @!@!@STARTMSG 2201:0 @!@!@
-The coverage statistics at 2022-02-10 12:51:45
+The coverage statistics at 2022-02-10 12:55:49
 @!@!@ENDMSG 2201 @!@!@
 @!@!@STARTMSG 2773:0 @!@!@
 <Init line 16, col 1 to line 16, col 4 of module MutualExclusionSpec>: 1:1
@@ -173,7 +173,7 @@ The coverage statistics at 2022-02-10 12:51:45
 End of statistics.
 @!@!@ENDMSG 2202 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-Progress(4) at 2022-02-10 12:51:45: 15 states generated (717 s/min), 8 distinct states found (382 ds/min), 0 states left on queue.
+Progress(4) at 2022-02-10 12:55:49: 15 states generated (725 s/min), 8 distinct states found (387 ds/min), 0 states left on queue.
 @!@!@ENDMSG 2200 @!@!@
 @!@!@STARTMSG 2199:0 @!@!@
 15 states generated, 8 distinct states found, 0 states left on queue.
@@ -185,5 +185,5 @@ The depth of the complete state graph search is 4.
 The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
 @!@!@ENDMSG 2268 @!@!@
 @!@!@STARTMSG 2186:0 @!@!@
-Finished in 1261ms at (2022-02-10 12:51:45)
+Finished in 1252ms at (2022-02-10 12:55:49)
 @!@!@ENDMSG 2186 @!@!@

MutualExclusionSpec.toolbox/Model_1/Model_1.dot

@@ -3,40 +3,40 @@ edge [colorscheme="paired12"]
 nodesep=0.35;
 subgraph cluster_graph {
 color="white";
--6876585601359980216 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")",style = filled]
--6876585601359980216 -> 6125294884432588227 [label="",color="2",fontcolor="2"];
-6125294884432588227 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")"];
--6876585601359980216 -> -3658280094581664638 [label="",color="2",fontcolor="2"];
--3658280094581664638 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")"];
--6876585601359980216 -> -6876585601359980216 [style="dashed"];
-6125294884432588227 -> 8200666643011396758 [label="",color="3",fontcolor="3"];
-8200666643011396758 [label="pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\")"];
-6125294884432588227 -> -825492852127754843 [label="",color="2",fontcolor="2"];
--825492852127754843 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")"];
-6125294884432588227 -> 6125294884432588227 [style="dashed"];
--3658280094581664638 -> -825492852127754843 [label="",color="2",fontcolor="2"];
--3658280094581664638 -> -2602126512520471372 [label="",color="3",fontcolor="3"];
--2602126512520471372 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")"];
--3658280094581664638 -> -3658280094581664638 [style="dashed"];
-8200666643011396758 -> -6876585601359980216 [label="",color="4",fontcolor="4"];
-8200666643011396758 -> -5644674202921659548 [label="",color="2",fontcolor="2"];
--5644674202921659548 [label="pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")"];
-8200666643011396758 -> 8200666643011396758 [style="dashed"];
--825492852127754843 -> -5644674202921659548 [label="",color="3",fontcolor="3"];
--825492852127754843 -> -3230548181155136154 [label="",color="3",fontcolor="3"];
--3230548181155136154 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")"];
--825492852127754843 -> -825492852127754843 [style="dashed"];
--2602126512520471372 -> -3230548181155136154 [label="",color="2",fontcolor="2"];
--2602126512520471372 -> -6876585601359980216 [label="",color="4",fontcolor="4"];
--2602126512520471372 -> -2602126512520471372 [style="dashed"];
--5644674202921659548 -> -3658280094581664638 [label="",color="4",fontcolor="4"];
--5644674202921659548 -> -5644674202921659548 [style="dashed"];
--3230548181155136154 -> 6125294884432588227 [label="",color="4",fontcolor="4"];
--3230548181155136154 -> -3230548181155136154 [style="dashed"];
-{rank = same; -6876585601359980216;}
-{rank = same; 6125294884432588227;-3658280094581664638;}
-{rank = same; 8200666643011396758;-2602126512520471372;-825492852127754843;}
-{rank = same; -3230548181155136154;-5644674202921659548;}
+-9093351885969996355 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")",style = filled]
+-9093351885969996355 -> -2881408805600288180 [label="",color="2",fontcolor="2"];
+-2881408805600288180 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")"];
+-9093351885969996355 -> -3960690064856539301 [label="",color="2",fontcolor="2"];
+-3960690064856539301 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")"];
+-2881408805600288180 -> 1689967940869742290 [label="",color="3",fontcolor="3"];
+1689967940869742290 [label="pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\")"];
+-9093351885969996355 -> -9093351885969996355 [style="dashed"];
+-2881408805600288180 -> 8739640561908614467 [label="",color="2",fontcolor="2"];
+8739640561908614467 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")"];
+-2881408805600288180 -> -2881408805600288180 [style="dashed"];
+-3960690064856539301 -> 8739640561908614467 [label="",color="2",fontcolor="2"];
+-3960690064856539301 -> -1150495510335961815 [label="",color="3",fontcolor="3"];
+-1150495510335961815 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")"];
+-3960690064856539301 -> -3960690064856539301 [style="dashed"];
+1689967940869742290 -> -9093351885969996355 [label="",color="4",fontcolor="4"];
+1689967940869742290 -> -7469351656913119290 [label="",color="2",fontcolor="2"];
+-7469351656913119290 [label="pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")"];
+1689967940869742290 -> 1689967940869742290 [style="dashed"];
+8739640561908614467 -> -7469351656913119290 [label="",color="3",fontcolor="3"];
+8739640561908614467 -> 1306210985855028210 [label="",color="3",fontcolor="3"];
+1306210985855028210 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")"];
+8739640561908614467 -> 8739640561908614467 [style="dashed"];
+-1150495510335961815 -> 1306210985855028210 [label="",color="2",fontcolor="2"];
+-1150495510335961815 -> -9093351885969996355 [label="",color="4",fontcolor="4"];
+-1150495510335961815 -> -1150495510335961815 [style="dashed"];
+-7469351656913119290 -> -3960690064856539301 [label="",color="4",fontcolor="4"];
+-7469351656913119290 -> -7469351656913119290 [style="dashed"];
+1306210985855028210 -> -2881408805600288180 [label="",color="4",fontcolor="4"];
+1306210985855028210 -> 1306210985855028210 [style="dashed"];
+{rank = same; -9093351885969996355;}
+{rank = same; -3960690064856539301;-2881408805600288180;}
+{rank = same; -1150495510335961815;1689967940869742290;8739640561908614467;}
+{rank = same; 1306210985855028210;-7469351656913119290;}
 }
 subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
 node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]

MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla

@@ -53,7 +53,7 @@ Liveness == \A i \in Procs:
                     \/ <>[](pc[i] = "non-cs")                   \* either stuck in non-cs, or
                     \/ []<>(pc[i] = "csentry")                  \* keeps on reaching "enter cs"
                 /\
-                    /\ (pc[i] = "csentry") ~> (pc[i] = "cs")    \* if it wants to enter, it enters cs and leaves it 
+                    /\ (pc[i] = "csentry") ~> (pc[i] = "cs")    \* if it wants to enter, it enters cs and leaves it
                     /\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
 
 
@@ -64,5 +64,5 @@ THEOREM Spec => Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Thu Feb 10 12:51:42 MSK 2022 by kirr
+\* Last modified Thu Feb 10 12:53:17 MSK 2022 by kirr
 \* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

MutualExclusionSpec.toolbox/MutualExclusionSpec.log

-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:52
+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:55
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -169,7 +169,7 @@ s/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1
 c/amsfonts/cm/cmti7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
 nts/cm/cmti8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/lat
 xfont/lasy10.pfb>
-Output written on MutualExclusionSpec.pdf (2 pages, 147815 bytes).
+Output written on MutualExclusionSpec.pdf (2 pages, 147797 bytes).
 PDF statistics:
  71 PDF objects out of 1000 (max. 8388607)
  51 compressed objects within 1 object stream

MutualExclusionSpec.toolbox/MutualExclusionSpec.tex

@@ -1098,7 +1098,7 @@
 \end{cpar}%
 \begin{cpar}{0}{F}{F}{0}{0}{}%
  \ensuremath{\.{\,\backslash\,}\.{*}} Last modified \ensuremath{Thu}
- \ensuremath{Feb} 10 12:51:42 \ensuremath{MSK} 2022 by \ensuremath{kirr
+ \ensuremath{Feb} 10 12:53:17 \ensuremath{MSK} 2022 by \ensuremath{kirr
 }%
 \end{cpar}%
 \begin{cpar}{0}{F}{F}{0}{0}{}%