.

Alternate.toolbox/Model_1/MC.cfg

-\* CONSTANT definitions
-
-CONSTANT
-    Procs <- const_1644485925128909000
-\* SPECIFICATION definition
-SPECIFICATION
-Spec
-\* INVARIANT definition
-INVARIANT
-inv_1644485925128910000
-inv_1644485925128911000
-\* PROPERTY definition
-PROPERTY
-prop_1644485925128912000
-prop_1644485925128913000
-KeepsEnteringCS
-\* Generated on Thu Feb 10 12:38:45 MSK 2022
\ No newline at end of file

Alternate.toolbox/Model_1/MC.tla

----- MODULE MC ----
-EXTENDS Alternate, TLC
-
-\* CONSTANT definitions @modelParameterConstants:0Procs
-const_1644485925128909000 == 
-0..1
-----
-
-\* INVARIANT definition @modelCorrectnessInvariants:0
-inv_1644485925128910000 ==
-ME!MutualExclusion
-----
-\* INVARIANT definition @modelCorrectnessInvariants:1
-inv_1644485925128911000 ==
-\A i \in Procs : (pc[i] = "cs") => (turn = i)
-----
-\* PROPERTY definition @modelCorrectnessProperties:0
-prop_1644485925128912000 ==
-ME!Spec
-----
-\* PROPERTY definition @modelCorrectnessProperties:1
-prop_1644485925128913000 ==
-ME!Liveness
-----
-=============================================================================
-\* Modification History
-\* Created Thu Feb 10 12:38:45 MSK 2022 by kirr