.

.gitignore

@@ -6,6 +6,7 @@
 *.toolbox/*.aux
 
 *.toolbox/*/*.tla
+!*.toolbox/*/MC.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_1644487382552947000
+    Procs <- const_1644487564216951000
 \* SPECIFICATION definition
 SPECIFICATION
 Spec
@@ -16,4 +16,4 @@ MutualExclusion
 \* PROPERTY definition
 PROPERTY
 Liveness
-\* Generated on Thu Feb 10 13:03:02 MSK 2022
+\* Generated on Thu Feb 10 13:06:04 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_1644487564216951000 == 
+{p1, p2}
+----
+
+=============================================================================
+\* Modification History
+\* Created Thu Feb 10 13:06:04 MSK 2022 by kirr