.

Alternate.tla

+----------------------------- MODULE Alternate -----------------------------
+\* Module Alternate specifies turn-based solution for mutual-exclusion problem.
+EXTENDS Integers
+
+CONSTANT Procs
+\*ASSUME \E N \in Nat : Procs = 0..N
+ASSUME \E N \in 0..10 : Procs = 0..N
+
+Max(s) == CHOOSE x \in s :
+                    /\ \A y \in s: y =< x
+                    /\ \E z \in s: z = x
+
+NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
+
+
+(********
+--fair algorithm Alternate {
+  variable turn \in Procs;
+  process (p \in Procs) {
+    ncs: while (TRUE) {
+            skip;   \* non-critical section
+
+  enter:    await turn = self;
+
+     cs:    skip;   \* critical section
+
+\*   exit:    turn := 1 - self
+   exit:    turn := ((self + 1) % NProcs)
+         };
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
+VARIABLES turn, pc
+
+vars == << turn, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ turn \in Procs
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ turn' = turn
+
+enter(self) == /\ pc[self] = "enter"
+               /\ turn = self
+               /\ pc' = [pc EXCEPT ![self] = "cs"]
+               /\ turn' = turn
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ turn' = turn
+
+exit(self) == /\ pc[self] = "exit"
+              /\ turn' = ((self + 1) % NProcs)
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
+
+Next == (\E self \in Procs: p(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+\* END TRANSLATION 
+
+
+--------
+
+
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  IF pc[proc] = "cs" THEN "cs"
+                                                               ELSE "non-cs"]
+
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 18:03:45 MSK 2022 by kirr
+\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr

Alternate.toolbox/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>Alternate</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+		<buildCommand>
+			<name>toolbox.builder.TLAParserBuilder</name>
+			<arguments>
+			</arguments>
+		</buildCommand>
+	</buildSpec>
+	<natures>
+		<nature>toolbox.natures.TLANature</nature>
+	</natures>
+	<linkedResources>
+		<link>
+			<name>Alternate.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/Alternate.tla</locationURI>
+		</link>
+		<link>
+			<name>MutualExclusionSpec.tla</name>
+			<type>1</type>
+			<location>/home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.tla</location>
+		</link>
+	</linkedResources>
+</projectDescription>

Alternate.toolbox/.settings/org.lamport.tla.toolbox.prefs

+ProjectRootFile=PARENT-1-PROJECT_LOC/Alternate.tla
+eclipse.preferences.version=1

Alternate.toolbox/Alternate.aux

+\relax 
+\gdef \@abspage@last{1}

Alternate.toolbox/Alternate.log

+This is pdfTeX, Version 3.14159265-2.6-1.40.21 (TeX Live 2020/Debian) (preloaded format=pdflatex 2021.6.9)  9 FEB 2022 17:49
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**Alternate.tex
+(./Alternate.tex
+LaTeX2e <2020-10-01> patch level 4
+L3 programming layer <2021-01-09> xparse <2020-03-03>
+(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
+Document Class: article 2020/04/10 v1.4m Standard LaTeX document class
+(/usr/share/texlive/texmf-dist/tex/latex/base/size10.clo
+File: size10.clo 2020/04/10 v1.4m Standard LaTeX file (size option)
+)
+\c@part=\count177
+\c@section=\count178
+\c@subsection=\count179
+\c@subsubsection=\count180
+\c@paragraph=\count181
+\c@subparagraph=\count182
+\c@figure=\count183
+\c@table=\count184
+\abovecaptionskip=\skip47
+\belowcaptionskip=\skip48
+\bibindent=\dimen138
+) (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
+Package: color 2020/02/24 v1.2b Standard LaTeX Color (DPC)
+(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/color.cfg
+File: color.cfg 2016/01/02 v1.6 sample color configuration
+)
+Package color Info: Driver file: pdftex.def on input line 147.
+(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def
+File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex
+)) (/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty
+Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols)
+\symlasy=\mathgroup4
+LaTeX Font Info:    Overwriting symbol font `lasy' in version `bold'
+(Font)                  U/lasy/m/n --> U/lasy/b/n on input line 52.
+) (/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty
+Package: ifthen 2014/09/29 v1.1c Standard LaTeX ifthen package (DPC)
+)
+\symlength=\skip49
+\equalswidth=\skip50
+\charwidth=\skip51
+\boxrulewd=\skip52
+\boxlineht=\skip53
+\boxruleht=\skip54
+\boxruledp=\skip55
+\pcalvspace=\skip56
+\lcomindent=\skip57
+\@xlen=\skip58
+\templena=\skip59
+\templenb=\skip60
+\tempboxa=\box47
+\vshadelen=\skip61
+\boxwidth=\skip62
+\multicommentdepth=\skip63
+\c@pardepth=\count185
+\tempsbox=\box48
+\@cparht=\skip64
+\@cpardp=\skip65
+\xmcomlen=\skip66
+\spacewidth=\skip67
+\alignboxwidth=\skip68
+\alignwidth=\skip69
+\alignbox=\box49
+\symtlaitalics=\mathgroup5
+\c@tlx@ctr=\count186
+(/usr/share/texlive/texmf-dist/tex/latex/tools/verbatim.sty
+Package: verbatim 2020-07-07 v1.5u LaTeX2e package for verbatim enhancements
+\every@verbatim=\toks15
+\verbatim@line=\toks16
+\verbatim@in@stream=\read2
+) (/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
+File: l3backend-pdftex.def 2020-01-29 L3 backend support: PDF output (pdfTeX)
+\l__color_backend_stack_int=\count187
+\l__pdf_internal_box=\box50
+) (./Alternate.aux)
+\openout1 = `Alternate.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 939.
+LaTeX Font Info:    ... okay on input line 939.
+(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count188
+\scratchdimen=\dimen139
+\scratchbox=\box51
+\nofMPsegments=\count189
+\nofMParguments=\count190
+\everyMPshowfont=\toks17
+\MPscratchCnt=\count191
+\MPscratchDim=\dimen140
+\MPnumerator=\count192
+\makeMPintoPDFobject=\count193
+\everyMPtoPDFconversion=\toks18
+)
+LaTeX Font Info:    External font `cmex10' loaded for size
+(Font)              <7> on input line 942.
+LaTeX Font Info:    External font `cmex10' loaded for size
+(Font)              <5> on input line 942.
+LaTeX Font Info:    Trying to load font information for U+lasy on input line 94
+2.
+(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd
+File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions
+)
+LaTeX Font Info:    External font `cmex10' loaded for size
+(Font)              <8> on input line 947.
+LaTeX Font Info:    External font `cmex10' loaded for size
+(Font)              <6> on input line 947.
+LaTeX Font Info:    Trying to load font information for OMS+cmr on input line 9
+79.
+(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd
+File: omscmr.fd 2019/12/16 v2.5j Standard LaTeX font definitions
+)
+LaTeX Font Info:    Font shape `OMS/cmr/bx/n' in size <10> not available
+(Font)              Font shape `OMS/cmsy/b/n' tried instead on input line 979.
+[1
+
+{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] (./Alternate.aux) ) 
+Here is how much of TeX's memory you used:
+ 1331 strings out of 479304
+ 18714 string characters out of 5869780
+ 316183 words of memory out of 5000000
+ 18554 multiletter control sequences out of 15000+600000
+ 409464 words of font info for 50 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 44i,10n,50p,223b,320s stack positions out of 5000i,500n,10000p,200000b,80000s
+</usr/s
+hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/
+texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texliv
+e/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/tex
+mf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dis
+t/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts
+/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/
+public/amsfonts/cm/cmr5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
+msfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
+cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmss1
+0.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb>
+</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/s
+hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/t
+exlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/
+texmf-dist/fonts/type1/public/amsfonts/latxfont/lasy10.pfb>
+Output written on Alternate.pdf (1 page, 145876 bytes).
+PDF statistics:
+ 68 PDF objects out of 1000 (max. 8388607)
+ 49 compressed objects within 1 object stream
+ 0 named destinations out of 1000 (max. 500000)
+ 1 words of extra memory for PDF output out of 10000 (max. 10000000)
+

Alternate.toolbox/Alternate___Model_1.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="107"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1\A i \in Procs : (pc[i] = &quot;cs&quot;) =&gt; (turn = i)"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644418425669.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644418425669"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="96"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644418436130.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644418436130"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="55"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644418452332.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644418452332"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="26"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644418501814.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644418501814"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="112"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644418927867.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644418927867"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="0"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644419029182.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644419029182"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="88"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644419381553.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644419381553"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="29"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644421337435.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644421337435"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="21"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1\A i \in Procs : (pc[i] = &quot;cs&quot;) =&gt; (turn = i)"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644421349719.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644421349719"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="46"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1\A i \in Procs : (pc[i] = &quot;cs&quot;) =&gt; (turn = i+1)"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Alternate___Model_1_SnapShot_1644421372999.launch

+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
+    <stringAttribute key="TLCCmdLineParameters" value=""/>
+    <stringAttribute key="alias" value=""/>
+    <intAttribute key="collectCoverage" value="1"/>
+    <stringAttribute key="configurationName" value="Model_1_SnapShot_1644421372999"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.122.1"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="107"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="25"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value=""/>
+    <stringAttribute key="modelBehaviorNext" value=""/>
+    <stringAttribute key="modelBehaviorSpec" value="Spec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <stringAttribute key="modelBehaviorVars" value="pc, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1\A i \in Procs : (pc[i] = &quot;cs&quot;) =&gt; (turn = i)"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="Procs;;0..1;0;0"/>
+    </listAttribute>
+    <intAttribute key="modelVersion" value="20191005"/>
+    <intAttribute key="numberOfWorkers" value="2"/>
+    <stringAttribute key="postCondition" value=""/>
+    <booleanAttribute key="recover" value="false"/>
+    <stringAttribute key="result.mail.address" value=""/>
+    <intAttribute key="simuAril" value="-1"/>
+    <intAttribute key="simuDepth" value="100"/>
+    <stringAttribute key="simuNumTraces" value="9223372036854775807"/>
+    <intAttribute key="simuSeed" value="-1"/>
+    <stringAttribute key="specName" value="Alternate"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

Alternate.toolbox/Model_1/Alternate.tla

+----------------------------- MODULE Alternate -----------------------------
+\* Module Alternate specifies turn-based solution for mutual-exclusion problem.
+EXTENDS Integers
+
+CONSTANT Procs
+\*ASSUME \E N \in Nat : Procs = 0..N
+ASSUME \E N \in 0..10 : Procs = 0..N
+
+Max(s) == CHOOSE x \in s :
+                    /\ \A y \in s: y =< x
+                    /\ \E z \in s: z = x
+
+NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
+
+
+(********
+--fair algorithm Alternate {
+  variable turn \in Procs;
+  process (p \in Procs) {
+    ncs: while (TRUE) {
+            skip;   \* non-critical section
+
+  enter:    await turn = self;
+
+     cs:    skip;   \* critical section
+
+\*   exit:    turn := 1 - self
+   exit:    turn := ((self + 1) % NProcs)
+         };
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
+VARIABLES turn, pc
+
+vars == << turn, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ turn \in Procs
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ turn' = turn
+
+enter(self) == /\ pc[self] = "enter"
+               /\ turn = self
+               /\ pc' = [pc EXCEPT ![self] = "cs"]
+               /\ turn' = turn
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ turn' = turn
+
+exit(self) == /\ pc[self] = "exit"
+              /\ turn' = ((self + 1) % NProcs)
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
+
+Next == (\E self \in Procs: p(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+\* END TRANSLATION 
+
+
+--------
+
+
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  IF pc[proc] = "cs" THEN "cs"
+                                                               ELSE "non-cs"]
+
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 18:03:45 MSK 2022 by kirr
+\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr

Alternate.toolbox/Model_1/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    Procs <- const_1644421370985520000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644421370985521000
+inv_1644421370985522000
+\* PROPERTY definition
+PROPERTY
+prop_1644421370985523000
+prop_1644421370985524000
+\* Generated on Wed Feb 09 18:42:50 MSK 2022
\ No newline at end of file

Alternate.toolbox/Model_1/MC.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 107 and seed 6844394497227079726 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 73860] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 18:42:51)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 2 distinct states generated at 2022-02-09 18:42:52.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 18:42:52: 26 states generated, 16 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 80 total distinct states at (2022-02-09 18:42:52)
+@!@!@ENDMSG 2192 @!@!@
+@!@!@STARTMSG 2267:0 @!@!@
+Finished checking temporal properties in 00s at 2022-02-09 18:42:52
+@!@!@ENDMSG 2267 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+  Estimates of the probability that TLC did not check all reachable states
+  because two distinct states had the same fingerprint:
+  calculated (optimistic):  val = 8.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 18:42:52
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 12 to line 41, col 25 of module Alternate: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 42, col 12 to line 42, col 44 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 42, col 17 to line 42, col 44 of module Alternate: 2:4
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 42, col 27 to line 42, col 33 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:24
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 17 to line 44, col 32 of module Alternate: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 44, col 17 to line 44, col 24 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 17 to line 45, col 20 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 46, col 17 to line 46, col 51 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 17 to line 47, col 28 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:4
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 19 to line 49, col 36 of module Alternate: 52
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 49, col 19 to line 49, col 26 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 19 to line 50, col 29 of module Alternate: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 19 to line 50, col 22 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 26 to line 50, col 29 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 19 to line 51, col 50 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 52, col 19 to line 52, col 30 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 30 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 54, col 16 to line 54, col 23 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 19 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 56, col 16 to line 56, col 49 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 27 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 18 to line 59, col 34 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 59, col 18 to line 59, col 25 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 18 to line 60, col 46 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 61, col 18 to line 61, col 50 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644421370985521000 line 10, col 1 to line 10, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 11, col 1 to line 11, col 18 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 78, col 23 to line 79, col 77 of module Alternate: 98:148
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 78, col 33 to line 78, col 37 of module Alternate: 98
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 77, col 1 to line 79, col 77 of module Alternate: 42
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644421370985522000 line 14, col 1 to line 14, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 15, col 1 to line 15, col 45 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 15, col 18 to line 15, col 45 of module MC: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 15, col 19 to line 15, col 30 of module MC: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 15, col 37 to line 15, col 44 of module MC: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 15, col 10 to line 15, col 14 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 18:42:52: 26 states generated (1 042 s/min), 16 distinct states found (641 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+26 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 5.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2268:0 @!@!@
+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 1515ms at (2022-02-09 18:42:52)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1/MC.tla

+---- MODULE MC ----
+EXTENDS Alternate, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0Procs
+const_1644421370985520000 == 
+0..1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644421370985521000 ==
+ME!MutualExclusion
+----
+\* INVARIANT definition @modelCorrectnessInvariants:1
+inv_1644421370985522000 ==
+\A i \in Procs : (pc[i] = "cs") => (turn = i)
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644421370985523000 ==
+ME!Spec
+----
+\* PROPERTY definition @modelCorrectnessProperties:1
+prop_1644421370985524000 ==
+ME!Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 18:42:50 MSK 2022 by kirr

Alternate.toolbox/Model_1/MC_TE.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 107 and seed 6844394497227079726 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 73860] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 18:42:51)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 2 distinct states generated at 2022-02-09 18:42:52.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 18:42:52: 26 states generated, 16 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 80 total distinct states at (2022-02-09 18:42:52)
+@!@!@ENDMSG 2192 @!@!@
+@!@!@STARTMSG 2267:0 @!@!@
+Finished checking temporal properties in 00s at 2022-02-09 18:42:52
+@!@!@ENDMSG 2267 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+  Estimates of the probability that TLC did not check all reachable states
+  because two distinct states had the same fingerprint:
+  calculated (optimistic):  val = 8.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 18:42:52
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 12 to line 41, col 25 of module Alternate: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 42, col 12 to line 42, col 44 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 42, col 17 to line 42, col 44 of module Alternate: 2:4
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 42, col 27 to line 42, col 33 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:24
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 17 to line 44, col 32 of module Alternate: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 44, col 17 to line 44, col 24 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 17 to line 45, col 20 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 46, col 17 to line 46, col 51 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 17 to line 47, col 28 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:4
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 19 to line 49, col 36 of module Alternate: 52
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 49, col 19 to line 49, col 26 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 19 to line 50, col 29 of module Alternate: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 19 to line 50, col 22 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 26 to line 50, col 29 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 19 to line 51, col 50 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 52, col 19 to line 52, col 30 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 30 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 54, col 16 to line 54, col 23 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 19 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 56, col 16 to line 56, col 49 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 27 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 18 to line 59, col 34 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 59, col 18 to line 59, col 25 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 18 to line 60, col 46 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 61, col 18 to line 61, col 50 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644421370985521000 line 10, col 1 to line 10, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 11, col 1 to line 11, col 18 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 78, col 23 to line 79, col 77 of module Alternate: 98:148
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 78, col 33 to line 78, col 37 of module Alternate: 98
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 77, col 1 to line 79, col 77 of module Alternate: 42
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644421370985522000 line 14, col 1 to line 14, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 15, col 1 to line 15, col 45 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 15, col 18 to line 15, col 45 of module MC: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 15, col 19 to line 15, col 30 of module MC: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 15, col 37 to line 15, col 44 of module MC: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 15, col 10 to line 15, col 14 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 18:42:52: 26 states generated (1 042 s/min), 16 distinct states found (641 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+26 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 5.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2268:0 @!@!@
+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 1515ms at (2022-02-09 18:42:52)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1/Model_1.dot

+strict digraph DiskGraph {
+edge [colorscheme="paired12"]
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+-400635202659742381 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
+-1182823203390725160 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
+-400635202659742381 -> -475001133580855070 [label="",color="2",fontcolor="2"];
+-475001133580855070 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
+-400635202659742381 -> 4659978677738564643 [label="",color="2",fontcolor="2"];
+4659978677738564643 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+-400635202659742381 -> -400635202659742381 [style="dashed"];
+-1182823203390725160 -> -1401437471233001879 [label="",color="2",fontcolor="2"];
+-1401437471233001879 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
+-1182823203390725160 -> 6147128843187323560 [label="",color="2",fontcolor="2"];
+6147128843187323560 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
+-1182823203390725160 -> -1182823203390725160 [style="dashed"];
+-475001133580855070 -> 5240454219582294627 [label="",color="3",fontcolor="3"];
+5240454219582294627 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
+-475001133580855070 -> 5064951816826678884 [label="",color="2",fontcolor="2"];
+5064951816826678884 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+-475001133580855070 -> -475001133580855070 [style="dashed"];
+4659978677738564643 -> 5064951816826678884 [label="",color="2",fontcolor="2"];
+4659978677738564643 -> 4659978677738564643 [style="dashed"];
+-1401437471233001879 -> 6030106734495858927 [label="",color="2",fontcolor="2"];
+6030106734495858927 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
+-1401437471233001879 -> -1401437471233001879 [style="dashed"];
+6147128843187323560 -> 6030106734495858927 [label="",color="2",fontcolor="2"];
+5240454219582294627 -> 7049503415477998762 [label="",color="4",fontcolor="4"];
+7049503415477998762 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
+6147128843187323560 -> 6211392433518555324 [label="",color="3",fontcolor="3"];
+6211392433518555324 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
+5240454219582294627 -> 3923823433829631963 [label="",color="2",fontcolor="2"];
+3923823433829631963 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+6147128843187323560 -> 6147128843187323560 [style="dashed"];
+5240454219582294627 -> 5240454219582294627 [style="dashed"];
+5064951816826678884 -> 3923823433829631963 [label="",color="3",fontcolor="3"];
+5064951816826678884 -> 5064951816826678884 [style="dashed"];
+6030106734495858927 -> 897235516867550670 [label="",color="3",fontcolor="3"];
+897235516867550670 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
+6030106734495858927 -> 6030106734495858927 [style="dashed"];
+7049503415477998762 -> -1182823203390725160 [label="",color="5",fontcolor="5"];
+7049503415477998762 -> 4069903303166039434 [label="",color="2",fontcolor="2"];
+4069903303166039434 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+7049503415477998762 -> 7049503415477998762 [style="dashed"];
+6211392433518555324 -> 897235516867550670 [label="",color="2",fontcolor="2"];
+6211392433518555324 -> -9152277194294045646 [label="",color="4",fontcolor="4"];
+-9152277194294045646 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
+6211392433518555324 -> 6211392433518555324 [style="dashed"];
+3923823433829631963 -> 4069903303166039434 [label="",color="4",fontcolor="4"];
+3923823433829631963 -> 3923823433829631963 [style="dashed"];
+897235516867550670 -> -2015577958311089194 [label="",color="4",fontcolor="4"];
+-2015577958311089194 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
+897235516867550670 -> 897235516867550670 [style="dashed"];
+4069903303166039434 -> 6147128843187323560 [label="",color="5",fontcolor="5"];
+4069903303166039434 -> 4069903303166039434 [style="dashed"];
+-9152277194294045646 -> -2015577958311089194 [label="",color="2",fontcolor="2"];
+-9152277194294045646 -> -400635202659742381 [label="",color="5",fontcolor="5"];
+-9152277194294045646 -> -9152277194294045646 [style="dashed"];
+-2015577958311089194 -> -475001133580855070 [label="",color="5",fontcolor="5"];
+-2015577958311089194 -> -2015577958311089194 [style="dashed"];
+{rank = same; -1182823203390725160;-400635202659742381;}
+{rank = same; 4659978677738564643;-1401437471233001879;6147128843187323560;-475001133580855070;}
+{rank = same; 6030106734495858927;6211392433518555324;5240454219582294627;5064951816826678884;}
+{rank = same; 3923823433829631963;7049503415477998762;897235516867550670;-9152277194294045646;}
+{rank = same; -2015577958311089194;4069903303166039434;}
+}
+subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
+node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
+cs [label="cs",fillcolor=4]
+exit [label="exit",fillcolor=5]
+enter [label="enter",fillcolor=3]
+ncs [label="ncs",fillcolor=2]
+}}
\ No newline at end of file

Alternate.toolbox/Model_1/MutualExclusionSpec.tla

+------------------------ MODULE MutualExclusionSpec ------------------------
+\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
+
+\* Procs is set of processes.
+\* Every process is assumed to loop and enter into "cs" state on every interation.
+\* States besides non-critical are represented as "non-cs".
+CONSTANT Procs
+VARIABLES pc
+
+TypeOK == pc \in [Procs -> {"non-cs", "cs"}]
+
+vars == <<pc>>
+
+\* All processes start from non-critical section.
+Init == pc \in [Procs -> {"non-cs"}]
+
+\* EnterCS(proc) is action when proc enters critical section.
+EnterCS(proc) ==
+        /\ \A i \in Procs: pc[i] /= "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "cs"]
+        
+\* ExitCS(proc) is action when proc leaves critical section.
+ExitCS(proc) ==
+        /\ pc[proc] = "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "non-cs"]
+
+Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
+
+
+Spec == /\ Init
+        /\ [][Next]_vars
+        /\ \A i \in Procs: (            \* fairness
+            /\ SF_vars(EnterCS(i))
+            /\ SF_vars(ExitCS(i)))
+
+----------------
+
+\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
+MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
+
+\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
+Liveness == \A i \in Procs:
+                    /\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
+                    /\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
+
+
+THEOREM Spec => []TypeOK        
+THEOREM Spec => []MutualExclusion
+THEOREM Spec => Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
+\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418425669/Alternate.tla

+----------------------------- MODULE Alternate -----------------------------
+\* Module Alternate specifies turn-based solution for mutual-exclusion problem.
+EXTENDS Integers
+
+CONSTANT Procs
+\*ASSUME \E N \in Nat : Procs = 0..N
+ASSUME \E N \in 0..10 : Procs = 0..N
+
+Max(s) == CHOOSE x \in s :
+                    /\ \A y \in s: y =< x
+                    /\ \E z \in s: z = x
+
+NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
+
+
+(********
+--fair algorithm Alternate {
+  variable turn \in Procs;
+  process (p \in Procs) {
+    ncs: while (TRUE) {
+            skip;   \* non-critical section
+
+  enter:    await turn = self;
+
+     cs:    skip;   \* critical section
+
+\*   exit:    turn := 1 - self
+   exit:    turn := ((self + 1) % NProcs)
+         };
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
+VARIABLES turn, pc
+
+vars == << turn, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ turn \in Procs
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ turn' = turn
+
+enter(self) == /\ pc[self] = "enter"
+               /\ turn = self
+               /\ pc' = [pc EXCEPT ![self] = "cs"]
+               /\ turn' = turn
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ turn' = turn
+
+exit(self) == /\ pc[self] = "exit"
+              /\ turn' = ((self + 1) % NProcs)
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
+
+Next == (\E self \in Procs: p(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+\* END TRANSLATION 
+
+
+--------
+
+
+
+(*
+PC2ME(xpc) == [proc \in Procs  |->  IF xpc[proc] = "cs" THEN "cs"
+                                                        ELSE "non-cs"]
+ME == INSTANCE MutualExclusionSpec WITH pc <- PC2ME(pc)
+*)
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  IF pc[proc] = "cs" THEN "cs"
+                                                               ELSE "non-cs"]
+
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 17:53:40 MSK 2022 by kirr
+\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418425669/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    Procs <- const_1644418423653463000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644418423653464000
+\* PROPERTY definition
+PROPERTY
+prop_1644418423653465000
+prop_1644418423653466000
+\* Generated on Wed Feb 09 17:53:43 MSK 2022
\ No newline at end of file

Alternate.toolbox/Model_1_SnapShot_1644418425669/MC.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 96 and seed -7115604794889667354 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71512] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 17:53:44)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 2 distinct states generated at 2022-02-09 17:53:44.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:53:45: 26 states generated, 16 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 80 total distinct states at (2022-02-09 17:53:45)
+@!@!@ENDMSG 2192 @!@!@
+@!@!@STARTMSG 2267:0 @!@!@
+Finished checking temporal properties in 00s at 2022-02-09 17:53:45
+@!@!@ENDMSG 2267 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+  Estimates of the probability that TLC did not check all reachable states
+  because two distinct states had the same fingerprint:
+  calculated (optimistic):  val = 8.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 17:53:45
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 12 to line 41, col 25 of module Alternate: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 42, col 12 to line 42, col 44 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 42, col 17 to line 42, col 44 of module Alternate: 2:4
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 42, col 27 to line 42, col 33 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:24
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 17 to line 44, col 32 of module Alternate: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 44, col 17 to line 44, col 24 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 17 to line 45, col 20 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 46, col 17 to line 46, col 51 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 17 to line 47, col 28 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:4
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 19 to line 49, col 36 of module Alternate: 52
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 49, col 19 to line 49, col 26 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 19 to line 50, col 29 of module Alternate: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 19 to line 50, col 22 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 26 to line 50, col 29 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 19 to line 51, col 50 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 52, col 19 to line 52, col 30 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 30 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 54, col 16 to line 54, col 23 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 19 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 56, col 16 to line 56, col 49 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 27 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 18 to line 59, col 34 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 59, col 18 to line 59, col 25 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 18 to line 60, col 46 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 61, col 18 to line 61, col 50 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644418423653464000 line 10, col 1 to line 10, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 11, col 1 to line 11, col 18 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 84, col 23 to line 85, col 77 of module Alternate: 98:148
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 84, col 33 to line 84, col 37 of module Alternate: 98
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 83, col 1 to line 85, col 77 of module Alternate: 42
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:53:45: 26 states generated (1 132 s/min), 16 distinct states found (697 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+26 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 5.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2268:0 @!@!@
+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 1384ms at (2022-02-09 17:53:45)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1_SnapShot_1644418425669/MC.tla

+---- MODULE MC ----
+EXTENDS Alternate, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0Procs
+const_1644418423653463000 == 
+0..1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644418423653464000 ==
+ME!MutualExclusion
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644418423653465000 ==
+ME!Spec
+----
+\* PROPERTY definition @modelCorrectnessProperties:1
+prop_1644418423653466000 ==
+ME!Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 17:53:43 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418425669/MC_TE.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 96 and seed -7115604794889667354 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71512] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 17:53:44)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 2 distinct states generated at 2022-02-09 17:53:44.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:53:45: 26 states generated, 16 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 80 total distinct states at (2022-02-09 17:53:45)
+@!@!@ENDMSG 2192 @!@!@
+@!@!@STARTMSG 2267:0 @!@!@
+Finished checking temporal properties in 00s at 2022-02-09 17:53:45
+@!@!@ENDMSG 2267 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+  Estimates of the probability that TLC did not check all reachable states
+  because two distinct states had the same fingerprint:
+  calculated (optimistic):  val = 8.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 17:53:45
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 12 to line 41, col 25 of module Alternate: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 42, col 12 to line 42, col 44 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 42, col 17 to line 42, col 44 of module Alternate: 2:4
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 42, col 27 to line 42, col 33 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:24
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 17 to line 44, col 32 of module Alternate: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 44, col 17 to line 44, col 24 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 17 to line 45, col 20 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 46, col 17 to line 46, col 51 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 17 to line 47, col 28 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:4
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 19 to line 49, col 36 of module Alternate: 52
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 49, col 19 to line 49, col 26 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 19 to line 50, col 29 of module Alternate: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 19 to line 50, col 22 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 26 to line 50, col 29 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 19 to line 51, col 50 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 52, col 19 to line 52, col 30 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 30 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 54, col 16 to line 54, col 23 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 19 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 56, col 16 to line 56, col 49 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 27 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 18 to line 59, col 34 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 59, col 18 to line 59, col 25 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 18 to line 60, col 46 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 61, col 18 to line 61, col 50 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644418423653464000 line 10, col 1 to line 10, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 11, col 1 to line 11, col 18 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 84, col 23 to line 85, col 77 of module Alternate: 98:148
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 84, col 33 to line 84, col 37 of module Alternate: 98
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 83, col 1 to line 85, col 77 of module Alternate: 42
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:53:45: 26 states generated (1 132 s/min), 16 distinct states found (697 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+26 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 5.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2268:0 @!@!@
+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 1384ms at (2022-02-09 17:53:45)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1_SnapShot_1644418425669/Model_1_SnapShot_1644418425669.dot

+strict digraph DiskGraph {
+edge [colorscheme="paired12"]
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+1402084145941851076 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
+264913071721429937 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
+264913071721429937 -> 1441589058236749349 [label="",color="2",fontcolor="2"];
+1441589058236749349 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
+1402084145941851076 -> 349469391966471760 [label="",color="2",fontcolor="2"];
+349469391966471760 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
+264913071721429937 -> -6190723150750739455 [label="",color="2",fontcolor="2"];
+-6190723150750739455 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
+1402084145941851076 -> -4985978420825095052 [label="",color="2",fontcolor="2"];
+-4985978420825095052 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+264913071721429937 -> 264913071721429937 [style="dashed"];
+1402084145941851076 -> 1402084145941851076 [style="dashed"];
+1441589058236749349 -> -4025760291280799090 [label="",color="2",fontcolor="2"];
+-4025760291280799090 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
+349469391966471760 -> -5049627876531235088 [label="",color="3",fontcolor="3"];
+-5049627876531235088 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
+1441589058236749349 -> 1441589058236749349 [style="dashed"];
+349469391966471760 -> -2812008362376975621 [label="",color="2",fontcolor="2"];
+-2812008362376975621 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+349469391966471760 -> 349469391966471760 [style="dashed"];
+-6190723150750739455 -> -4025760291280799090 [label="",color="2",fontcolor="2"];
+-6190723150750739455 -> -493897691022108030 [label="",color="3",fontcolor="3"];
+-493897691022108030 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
+-6190723150750739455 -> -6190723150750739455 [style="dashed"];
+-4985978420825095052 -> -2812008362376975621 [label="",color="2",fontcolor="2"];
+-4985978420825095052 -> -4985978420825095052 [style="dashed"];
+-4025760291280799090 -> 1306702513220175931 [label="",color="3",fontcolor="3"];
+1306702513220175931 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
+-5049627876531235088 -> -1782044937556263316 [label="",color="4",fontcolor="4"];
+-1782044937556263316 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
+-4025760291280799090 -> -4025760291280799090 [style="dashed"];
+-5049627876531235088 -> 562133816054668434 [label="",color="2",fontcolor="2"];
+562133816054668434 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+-5049627876531235088 -> -5049627876531235088 [style="dashed"];
+-2812008362376975621 -> 562133816054668434 [label="",color="3",fontcolor="3"];
+-2812008362376975621 -> -2812008362376975621 [style="dashed"];
+-493897691022108030 -> 1306702513220175931 [label="",color="2",fontcolor="2"];
+-493897691022108030 -> -1933917819784720848 [label="",color="4",fontcolor="4"];
+-1933917819784720848 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
+-493897691022108030 -> -493897691022108030 [style="dashed"];
+1306702513220175931 -> 7779513292595707742 [label="",color="4",fontcolor="4"];
+7779513292595707742 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
+1306702513220175931 -> 1306702513220175931 [style="dashed"];
+-1782044937556263316 -> 264913071721429937 [label="",color="5",fontcolor="5"];
+-1782044937556263316 -> 7488564517445007501 [label="",color="2",fontcolor="2"];
+7488564517445007501 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
+562133816054668434 -> 7488564517445007501 [label="",color="4",fontcolor="4"];
+-1782044937556263316 -> -1782044937556263316 [style="dashed"];
+562133816054668434 -> 562133816054668434 [style="dashed"];
+-1933917819784720848 -> 7779513292595707742 [label="",color="2",fontcolor="2"];
+-1933917819784720848 -> 1402084145941851076 [label="",color="5",fontcolor="5"];
+-1933917819784720848 -> -1933917819784720848 [style="dashed"];
+7779513292595707742 -> 349469391966471760 [label="",color="5",fontcolor="5"];
+7779513292595707742 -> 7779513292595707742 [style="dashed"];
+7488564517445007501 -> -6190723150750739455 [label="",color="5",fontcolor="5"];
+7488564517445007501 -> 7488564517445007501 [style="dashed"];
+{rank = same; 264913071721429937;1402084145941851076;}
+{rank = same; 1441589058236749349;-4985978420825095052;-6190723150750739455;349469391966471760;}
+{rank = same; -493897691022108030;-4025760291280799090;-5049627876531235088;-2812008362376975621;}
+{rank = same; 1306702513220175931;-1782044937556263316;562133816054668434;-1933917819784720848;}
+{rank = same; 7488564517445007501;7779513292595707742;}
+}
+subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
+node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
+cs [label="cs",fillcolor=4]
+exit [label="exit",fillcolor=5]
+enter [label="enter",fillcolor=3]
+ncs [label="ncs",fillcolor=2]
+}}
\ No newline at end of file

Alternate.toolbox/Model_1_SnapShot_1644418425669/MutualExclusionSpec.tla

+------------------------ MODULE MutualExclusionSpec ------------------------
+\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
+
+\* Procs is set of processes.
+\* Every process is assumed to loop and enter into "cs" state on every interation.
+\* States besides non-critical are represented as "non-cs".
+CONSTANT Procs
+VARIABLES pc
+
+TypeOK == pc \in [Procs -> {"non-cs", "cs"}]
+
+vars == <<pc>>
+
+\* All processes start from non-critical section.
+Init == pc \in [Procs -> {"non-cs"}]
+
+\* EnterCS(proc) is action when proc enters critical section.
+EnterCS(proc) ==
+        /\ \A i \in Procs: pc[i] /= "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "cs"]
+        
+\* ExitCS(proc) is action when proc leaves critical section.
+ExitCS(proc) ==
+        /\ pc[proc] = "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "non-cs"]
+
+Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
+
+
+Spec == /\ Init
+        /\ [][Next]_vars
+        /\ \A i \in Procs: (            \* fairness
+            /\ SF_vars(EnterCS(i))
+            /\ SF_vars(ExitCS(i)))
+
+----------------
+
+\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
+MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
+
+\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
+Liveness == \A i \in Procs:
+                    /\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
+                    /\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
+
+
+THEOREM Spec => []TypeOK        
+THEOREM Spec => []MutualExclusion
+THEOREM Spec => Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
+\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418436130/Alternate.tla

+----------------------------- MODULE Alternate -----------------------------
+\* Module Alternate specifies turn-based solution for mutual-exclusion problem.
+EXTENDS Integers
+
+CONSTANT Procs
+\*ASSUME \E N \in Nat : Procs = 0..N
+ASSUME \E N \in 0..10 : Procs = 0..N
+
+Max(s) == CHOOSE x \in s :
+                    /\ \A y \in s: y =< x
+                    /\ \E z \in s: z = x
+
+NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
+
+
+(********
+--fair algorithm Alternate {
+  variable turn \in Procs;
+  process (p \in Procs) {
+    ncs: while (TRUE) {
+            skip;   \* non-critical section
+
+  enter:    await turn = self;
+
+     cs:    skip;   \* critical section
+
+\*   exit:    turn := 1 - self
+   exit:    turn := ((self + 1) % NProcs)
+         };
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
+VARIABLES turn, pc
+
+vars == << turn, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ turn \in Procs
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ turn' = turn
+
+enter(self) == /\ pc[self] = "enter"
+               /\ turn = self
+               /\ pc' = [pc EXCEPT ![self] = "cs"]
+               /\ turn' = turn
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ turn' = turn
+
+exit(self) == /\ pc[self] = "exit"
+              /\ turn' = ((self + 1) % NProcs)
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
+
+Next == (\E self \in Procs: p(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+\* END TRANSLATION 
+
+
+--------
+
+
+
+(*
+PC2ME(xpc) == [proc \in Procs  |->  IF xpc[proc] = "cs" THEN "cs"
+                                                        ELSE "non-cs"]
+ME == INSTANCE MutualExclusionSpec WITH pc <- PC2ME(pc)
+*)
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  IF pc[proc] = "cs" THEN "cs"
+                                                               ELSE "Znon-cs"]
+
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 17:53:52 MSK 2022 by kirr
+\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418436130/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    Procs <- const_1644418434112467000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644418434112468000
+\* PROPERTY definition
+PROPERTY
+prop_1644418434112469000
+prop_1644418434112470000
+\* Generated on Wed Feb 09 17:53:54 MSK 2022
\ No newline at end of file

Alternate.toolbox/Model_1_SnapShot_1644418436130/MC.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 55 and seed 7390341523143387179 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71572] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 17:53:54)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2108:1 @!@!@
+Property Init is violated by the initial state:
+/\ pc = (0 :> "ncs" @@ 1 :> "ncs")
+/\ turn = 0
+
+@!@!@ENDMSG 2108 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished in 1232ms at (2022-02-09 17:53:55)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1_SnapShot_1644418436130/MC.tla

+---- MODULE MC ----
+EXTENDS Alternate, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0Procs
+const_1644418434112467000 == 
+0..1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644418434112468000 ==
+ME!MutualExclusion
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644418434112469000 ==
+ME!Spec
+----
+\* PROPERTY definition @modelCorrectnessProperties:1
+prop_1644418434112470000 ==
+ME!Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 17:53:54 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418436130/MC_TE.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 55 and seed 7390341523143387179 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71572] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 17:53:54)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2108:1 @!@!@
+Property Init is violated by the initial state:
+/\ pc = (0 :> "ncs" @@ 1 :> "ncs")
+/\ turn = 0
+
+@!@!@ENDMSG 2108 @!@!@
+@!@!@STARTMSG 2186:0 @!@!@
+Finished in 1232ms at (2022-02-09 17:53:55)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1_SnapShot_1644418436130/Model_1_SnapShot_1644418436130.dot

+strict digraph DiskGraph {
+edge [colorscheme="paired12"]
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";

Alternate.toolbox/Model_1_SnapShot_1644418436130/Model_1_liveness.dot

+digraph DiskGraph {
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";

Alternate.toolbox/Model_1_SnapShot_1644418436130/MutualExclusionSpec.tla

+------------------------ MODULE MutualExclusionSpec ------------------------
+\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
+
+\* Procs is set of processes.
+\* Every process is assumed to loop and enter into "cs" state on every interation.
+\* States besides non-critical are represented as "non-cs".
+CONSTANT Procs
+VARIABLES pc
+
+TypeOK == pc \in [Procs -> {"non-cs", "cs"}]
+
+vars == <<pc>>
+
+\* All processes start from non-critical section.
+Init == pc \in [Procs -> {"non-cs"}]
+
+\* EnterCS(proc) is action when proc enters critical section.
+EnterCS(proc) ==
+        /\ \A i \in Procs: pc[i] /= "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "cs"]
+        
+\* ExitCS(proc) is action when proc leaves critical section.
+ExitCS(proc) ==
+        /\ pc[proc] = "cs"
+        /\ pc' = [pc EXCEPT ![proc] = "non-cs"]
+
+Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
+
+
+Spec == /\ Init
+        /\ [][Next]_vars
+        /\ \A i \in Procs: (            \* fairness
+            /\ SF_vars(EnterCS(i))
+            /\ SF_vars(ExitCS(i)))
+
+----------------
+
+\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
+MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
+
+\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
+Liveness == \A i \in Procs:
+                    /\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
+                    /\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
+
+
+THEOREM Spec => []TypeOK        
+THEOREM Spec => []MutualExclusion
+THEOREM Spec => Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
+\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418452332/Alternate.tla

+----------------------------- MODULE Alternate -----------------------------
+\* Module Alternate specifies turn-based solution for mutual-exclusion problem.
+EXTENDS Integers
+
+CONSTANT Procs
+\*ASSUME \E N \in Nat : Procs = 0..N
+ASSUME \E N \in 0..10 : Procs = 0..N
+
+Max(s) == CHOOSE x \in s :
+                    /\ \A y \in s: y =< x
+                    /\ \E z \in s: z = x
+
+NProcs == Max(Procs)+1 \* XXX assumes procs are 0..N
+
+
+(********
+--fair algorithm Alternate {
+  variable turn \in Procs;
+  process (p \in Procs) {
+    ncs: while (TRUE) {
+            skip;   \* non-critical section
+
+  enter:    await turn = self;
+
+     cs:    skip;   \* critical section
+
+\*   exit:    turn := 1 - self
+   exit:    turn := ((self + 1) % NProcs)
+         };
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "dc237cc6")
+VARIABLES turn, pc
+
+vars == << turn, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ turn \in Procs
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ turn' = turn
+
+enter(self) == /\ pc[self] = "enter"
+               /\ turn = self
+               /\ pc' = [pc EXCEPT ![self] = "cs"]
+               /\ turn' = turn
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ turn' = turn
+
+exit(self) == /\ pc[self] = "exit"
+              /\ turn' = ((self + 1) % NProcs)
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+p(self) == ncs(self) \/ enter(self) \/ cs(self) \/ exit(self)
+
+Next == (\E self \in Procs: p(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+\* END TRANSLATION 
+
+
+--------
+
+
+
+(*
+PC2ME(xpc) == [proc \in Procs  |->  IF xpc[proc] = "cs" THEN "cs"
+                                                        ELSE "non-cs"]
+ME == INSTANCE MutualExclusionSpec WITH pc <- PC2ME(pc)
+*)
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  IF pc[proc] = "cs" THEN "cs"
+                                                               ELSE "non-cs"]
+
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 17:54:08 MSK 2022 by kirr
+\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418452332/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    Procs <- const_1644418450318471000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644418450318472000
+\* PROPERTY definition
+PROPERTY
+prop_1644418450318473000
+prop_1644418450318474000
+\* Generated on Wed Feb 09 17:54:10 MSK 2022
\ No newline at end of file

Alternate.toolbox/Model_1_SnapShot_1644418452332/MC.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 26 and seed -951008601140814114 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71623] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 17:54:10)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 2 distinct states generated at 2022-02-09 17:54:11.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:54:11: 26 states generated, 16 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 80 total distinct states at (2022-02-09 17:54:11)
+@!@!@ENDMSG 2192 @!@!@
+@!@!@STARTMSG 2267:0 @!@!@
+Finished checking temporal properties in 00s at 2022-02-09 17:54:11
+@!@!@ENDMSG 2267 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+  Estimates of the probability that TLC did not check all reachable states
+  because two distinct states had the same fingerprint:
+  calculated (optimistic):  val = 8.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 17:54:11
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 12 to line 41, col 25 of module Alternate: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 42, col 12 to line 42, col 44 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 42, col 17 to line 42, col 44 of module Alternate: 2:4
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 42, col 27 to line 42, col 33 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:24
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 17 to line 44, col 32 of module Alternate: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 44, col 17 to line 44, col 24 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 17 to line 45, col 20 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 46, col 17 to line 46, col 51 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 17 to line 47, col 28 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:4
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 19 to line 49, col 36 of module Alternate: 52
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 49, col 19 to line 49, col 26 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 19 to line 50, col 29 of module Alternate: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 19 to line 50, col 22 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 26 to line 50, col 29 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 19 to line 51, col 50 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 52, col 19 to line 52, col 30 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 30 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 54, col 16 to line 54, col 23 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 19 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 56, col 16 to line 56, col 49 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 27 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 18 to line 59, col 34 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 59, col 18 to line 59, col 25 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 18 to line 60, col 46 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 61, col 18 to line 61, col 50 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644418450318472000 line 10, col 1 to line 10, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 11, col 1 to line 11, col 18 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 84, col 23 to line 85, col 77 of module Alternate: 98:148
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 84, col 33 to line 84, col 37 of module Alternate: 98
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 83, col 1 to line 85, col 77 of module Alternate: 42
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:54:11: 26 states generated (1 142 s/min), 16 distinct states found (702 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+26 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 5.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2268:0 @!@!@
+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 1373ms at (2022-02-09 17:54:11)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1_SnapShot_1644418452332/MC.tla

+---- MODULE MC ----
+EXTENDS Alternate, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0Procs
+const_1644418450318471000 == 
+0..1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644418450318472000 ==
+ME!MutualExclusion
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644418450318473000 ==
+ME!Spec
+----
+\* PROPERTY definition @modelCorrectnessProperties:1
+prop_1644418450318474000 ==
+ME!Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 17:54:10 MSK 2022 by kirr

Alternate.toolbox/Model_1_SnapShot_1644418452332/MC_TE.out

+@!@!@STARTMSG 2262:0 @!@!@
+TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
+@!@!@ENDMSG 2262 @!@!@
+@!@!@STARTMSG 2187:0 @!@!@
+Running breadth-first search Model-Checking with fp 26 and seed -951008601140814114 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71623] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
+@!@!@ENDMSG 2187 @!@!@
+@!@!@STARTMSG 2220:0 @!@!@
+Starting SANY...
+@!@!@ENDMSG 2220 @!@!@
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
+Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
+Semantic processing of module Naturals
+Semantic processing of module Integers
+Semantic processing of module MutualExclusionSpec
+Semantic processing of module Alternate
+Semantic processing of module Sequences
+Semantic processing of module FiniteSets
+Semantic processing of module TLC
+Semantic processing of module MC
+@!@!@STARTMSG 2219:0 @!@!@
+SANY finished.
+@!@!@ENDMSG 2219 @!@!@
+@!@!@STARTMSG 2185:0 @!@!@
+Starting... (2022-02-09 17:54:10)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2212:0 @!@!@
+Implied-temporal checking--satisfiability problem has 5 branches.
+@!@!@ENDMSG 2212 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 2 distinct states generated at 2022-02-09 17:54:11.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:54:11: 26 states generated, 16 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 80 total distinct states at (2022-02-09 17:54:11)
+@!@!@ENDMSG 2192 @!@!@
+@!@!@STARTMSG 2267:0 @!@!@
+Finished checking temporal properties in 00s at 2022-02-09 17:54:11
+@!@!@ENDMSG 2267 @!@!@
+@!@!@STARTMSG 2193:0 @!@!@
+Model checking completed. No error has been found.
+  Estimates of the probability that TLC did not check all reachable states
+  because two distinct states had the same fingerprint:
+  calculated (optimistic):  val = 8.7E-18
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 17:54:11
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 40, col 1 to line 40, col 4 of module Alternate>: 2:2
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 12 to line 41, col 25 of module Alternate: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 42, col 12 to line 42, col 44 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 42, col 17 to line 42, col 44 of module Alternate: 2:4
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 42, col 27 to line 42, col 33 of module Alternate: 2
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 8:24
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 17 to line 44, col 32 of module Alternate: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 44, col 17 to line 44, col 24 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 17 to line 45, col 20 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 46, col 17 to line 46, col 51 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 17 to line 47, col 28 of module Alternate: 24
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 49, col 1 to line 49, col 11 of module Alternate>: 3:4
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 19 to line 49, col 36 of module Alternate: 52
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 49, col 19 to line 49, col 26 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 19 to line 50, col 29 of module Alternate: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 19 to line 50, col 22 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 50, col 26 to line 50, col 29 of module Alternate: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 19 to line 51, col 50 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 52, col 19 to line 52, col 30 of module Alternate: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 54, col 1 to line 54, col 8 of module Alternate>: 3:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 30 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 54, col 16 to line 54, col 23 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 19 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 56, col 16 to line 56, col 49 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 27 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:6
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 18 to line 59, col 34 of module Alternate: 54
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 59, col 18 to line 59, col 25 of module Alternate: 48
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 18 to line 60, col 46 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 61, col 18 to line 61, col 50 of module Alternate: 6
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644418450318472000 line 10, col 1 to line 10, col 23 of module MC>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 11, col 1 to line 11, col 18 of module MC: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 84, col 23 to line 85, col 77 of module Alternate: 98:148
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 84, col 33 to line 84, col 37 of module Alternate: 98
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 83, col 1 to line 85, col 77 of module Alternate: 42
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 16
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(5) at 2022-02-09 17:54:11: 26 states generated (1 142 s/min), 16 distinct states found (702 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+26 states generated, 16 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 5.
+@!@!@ENDMSG 2194 @!@!@
+@!@!@STARTMSG 2268:0 @!@!@
+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 1373ms at (2022-02-09 17:54:11)
+@!@!@ENDMSG 2186 @!@!@

Alternate.toolbox/Model_1_SnapShot_1644418501814/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    Procs <- const_1644418499799475000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644418499799476000
+\* PROPERTY definition
+PROPERTY
+prop_1644418499799477000
+prop_1644418499799478000
+\* Generated on Wed Feb 09 17:54:59 MSK 2022
\ No newline at end of file