.

MutualExclusionSpec.toolbox/Model_1/MC.cfg

@@ -5,7 +5,7 @@ p2 = p2
 \* MV CONSTANT definitions
 
 CONSTANT
-    Procs <- const_1644487129023939000
+    Procs <- const_1644487333852943000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
@@ -16,4 +16,4 @@ MutualExclusion
 \* PROPERTY definition
 PROPERTY
 Liveness
-\* Generated on Thu Feb 10 12:58:49 MSK 2022
\ No newline at end of file
+\* Generated on Thu Feb 10 13:02:13 MSK 2022
\ No newline at end of file

MutualExclusionSpec.toolbox/Model_1/MC.tla

----- MODULE MC ----
-EXTENDS MutualExclusionSpec, TLC
-
-\* MV CONSTANT declarations@modelParameterConstants
-CONSTANTS
-p1, p2
-----
-
-\* MV CONSTANT definitions Procs
-const_1644487129023939000 == 
-{p1, p2}
-----
-
-=============================================================================
-\* Modification History
-\* Created Thu Feb 10 12:58:49 MSK 2022 by kirr

MutualExclusionSpec.toolbox/Model_1/Model_1.dot

-strict digraph DiskGraph {
-edge [colorscheme="paired12"]
-nodesep=0.35;
-subgraph cluster_graph {
-color="white";
-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 ]
-WantCS [label="WantCS",fillcolor=2]
-ExitCS [label="ExitCS",fillcolor=4]
-EnterCS [label="EnterCS",fillcolor=3]
-}}
\ No newline at end of file