.

.gitignore

@@ -3,3 +3,8 @@
 *.toolbox/*.tex
 *.toolbox/*.pdf
 *.toolbox/*.log
+
+*.toolbox/*/*.tla
+*.toolbox/*/*.dot
+*.toolbox/*/*.pdf
+*.toolbox/*/*.out

MutualExclusionSpec.toolbox/Model_1/MC.cfg

@@ -5,7 +5,7 @@ p2 = p2
 \* MV CONSTANT definitions
 
 CONSTANT
-    Procs <- const_1644486948532935000
+    Procs <- const_1644487129023939000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
@@ -16,4 +16,4 @@ MutualExclusion
 \* PROPERTY definition
 PROPERTY
 Liveness
-\* Generated on Thu Feb 10 12:55:48 MSK 2022
+\* Generated on Thu Feb 10 12:58:49 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 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).
+Running breadth-first search Model-Checking with fp 19 and seed -2142680293908231447 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 90790] (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:55:48)
+Starting... (2022-02-10 12:58:49)
 @!@!@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:55:49.
+Finished computing initial states: 1 distinct state generated at 2022-02-10 12:58:50.
 @!@!@ENDMSG 2190 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-Progress(4) at 2022-02-10 12:55:49: 15 states generated, 8 distinct states found, 0 states left on queue.
+Progress(4) at 2022-02-10 12:58:50: 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:55:49)
+Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:58:50)
 @!@!@ENDMSG 2192 @!@!@
 @!@!@STARTMSG 2267:0 @!@!@
-Finished checking temporal properties in 00s at 2022-02-10 12:55:49
+Finished checking temporal properties in 00s at 2022-02-10 12:58:50
 @!@!@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:55:49
+The coverage statistics at 2022-02-10 12:58:50
 @!@!@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:55:49
 End of statistics.
 @!@!@ENDMSG 2202 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-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.
+Progress(4) at 2022-02-10 12:58:50: 15 states generated (706 s/min), 8 distinct states found (376 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 1252ms at (2022-02-10 12:55:49)
+Finished in 1285ms at (2022-02-10 12:58:50)
 @!@!@ENDMSG 2186 @!@!@

MutualExclusionSpec.toolbox/Model_1/MC.tla

@@ -7,10 +7,10 @@ p1, p2
 ----
 
 \* MV CONSTANT definitions Procs
-const_1644486948532935000 == 
+const_1644487129023939000 == 
 {p1, p2}
 ----
 
 =============================================================================
 \* Modification History
-\* Created Thu Feb 10 12:55:48 MSK 2022 by kirr
+\* Created Thu Feb 10 12:58:49 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 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).
+Running breadth-first search Model-Checking with fp 19 and seed -2142680293908231447 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 90790] (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:55:48)
+Starting... (2022-02-10 12:58:49)
 @!@!@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:55:49.
+Finished computing initial states: 1 distinct state generated at 2022-02-10 12:58:50.
 @!@!@ENDMSG 2190 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-Progress(4) at 2022-02-10 12:55:49: 15 states generated, 8 distinct states found, 0 states left on queue.
+Progress(4) at 2022-02-10 12:58:50: 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:55:49)
+Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:58:50)
 @!@!@ENDMSG 2192 @!@!@
 @!@!@STARTMSG 2267:0 @!@!@
-Finished checking temporal properties in 00s at 2022-02-10 12:55:49
+Finished checking temporal properties in 00s at 2022-02-10 12:58:50
 @!@!@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:55:49
+The coverage statistics at 2022-02-10 12:58:50
 @!@!@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:55:49
 End of statistics.
 @!@!@ENDMSG 2202 @!@!@
 @!@!@STARTMSG 2200:0 @!@!@
-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.
+Progress(4) at 2022-02-10 12:58:50: 15 states generated (706 s/min), 8 distinct states found (376 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 1252ms at (2022-02-10 12:55:49)
+Finished in 1285ms at (2022-02-10 12:58:50)
 @!@!@ENDMSG 2186 @!@!@

MutualExclusionSpec.toolbox/Model_1/Model_1.dot

@@ -3,40 +3,40 @@ edge [colorscheme="paired12"]
 nodesep=0.35;
 subgraph cluster_graph {
 color="white";
--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;}
+7826388974498231005 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")",style = filled]
+7826388974498231005 -> 7743948932593470164 [label="",color="2",fontcolor="2"];
+7743948932593470164 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")"];
+7826388974498231005 -> -7091387860856146872 [label="",color="2",fontcolor="2"];
+-7091387860856146872 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")"];
+7743948932593470164 -> 1520033749518464798 [label="",color="3",fontcolor="3"];
+1520033749518464798 [label="pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\")"];
+7826388974498231005 -> 7826388974498231005 [style="dashed"];
+7743948932593470164 -> 2891225834013969262 [label="",color="2",fontcolor="2"];
+2891225834013969262 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")"];
+7743948932593470164 -> 7743948932593470164 [style="dashed"];
+-7091387860856146872 -> 2891225834013969262 [label="",color="2",fontcolor="2"];
+-7091387860856146872 -> -7604993468008606684 [label="",color="3",fontcolor="3"];
+-7604993468008606684 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")"];
+-7091387860856146872 -> -7091387860856146872 [style="dashed"];
+1520033749518464798 -> 7826388974498231005 [label="",color="4",fontcolor="4"];
+1520033749518464798 -> 8048625394011437004 [label="",color="2",fontcolor="2"];
+8048625394011437004 [label="pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")"];
+1520033749518464798 -> 1520033749518464798 [style="dashed"];
+2891225834013969262 -> 8048625394011437004 [label="",color="3",fontcolor="3"];
+2891225834013969262 -> 6198530037439632960 [label="",color="3",fontcolor="3"];
+6198530037439632960 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")"];
+2891225834013969262 -> 2891225834013969262 [style="dashed"];
+-7604993468008606684 -> 6198530037439632960 [label="",color="2",fontcolor="2"];
+-7604993468008606684 -> 7826388974498231005 [label="",color="4",fontcolor="4"];
+-7604993468008606684 -> -7604993468008606684 [style="dashed"];
+8048625394011437004 -> -7091387860856146872 [label="",color="4",fontcolor="4"];
+8048625394011437004 -> 8048625394011437004 [style="dashed"];
+6198530037439632960 -> 7743948932593470164 [label="",color="4",fontcolor="4"];
+6198530037439632960 -> 6198530037439632960 [style="dashed"];
+{rank = same; 7826388974498231005;}
+{rank = same; 7743948932593470164;-7091387860856146872;}
+{rank = same; -7604993468008606684;1520033749518464798;2891225834013969262;}
+{rank = same; 6198530037439632960;8048625394011437004;}
 }
 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

@@ -64,5 +64,5 @@ THEOREM Spec => Liveness
 
 =============================================================================
 \* Modification History
-\* Last modified Thu Feb 10 12:53:17 MSK 2022 by kirr
+\* Last modified Thu Feb 10 12:58:08 MSK 2022 by kirr
 \* Created Wed Feb 09 13:11:29 MSK 2022 by kirr