.

MutualExclusionSpec.toolbox/Model_1/MC.cfg

-\* MV CONSTANT declarations
-CONSTANTS
-p1 = p1
-p2 = p2
-\* MV CONSTANT definitions
-
-CONSTANT
-    Procs <- const_1644487897396959000
-\* SPECIFICATION definition
-SPECIFICATION
-Spec
-\* INVARIANT definition
-INVARIANT
-TypeOK
-MutualExclusion
-\* PROPERTY definition
-PROPERTY
-Liveness
-\* Generated on Thu Feb 10 13:11:37 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_1644487897396959000 == 
-{p1, p2}
-----
-
-=============================================================================
-\* Modification History
-\* Created Thu Feb 10 13:11:37 MSK 2022 by kirr