X 1Bit

1Bit.tla

+-------------------------------- MODULE 1Bit --------------------------------
+\* 1Bit implementation of mutual exclusion
+EXTENDS Integers
+
+CONSTANT N
+ASSUME N \in Nat
+
+Procs == 0..N
+
+(********
+--fair algorithm 1BitProtocol {
+    variables flag = [i \in Procs |-> FALSE] ;
+    process (P \in Procs) {
+     ncs: while (TRUE) {
+            skip ; 
+     enter: flag[self] := TRUE ; 
+        e2: if (flag[1-self]) {
+        e3:   flag[self] := FALSE;
+              goto enter;
+            };
+        cs: skip ;
+      exit: flag[self] := FALSE ;            
+    }
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "b89f1da2")
+VARIABLES flag, pc
+
+vars == << flag, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ flag = [i \in Procs |-> FALSE]
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ flag' = flag
+
+enter(self) == /\ pc[self] = "enter"
+               /\ flag' = [flag EXCEPT ![self] = TRUE]
+               /\ pc' = [pc EXCEPT ![self] = "e2"]
+
+e2(self) == /\ pc[self] = "e2"
+            /\ IF flag[1-self]
+                  THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
+                  ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
+            /\ flag' = flag
+
+e3(self) == /\ pc[self] = "e3"
+            /\ flag' = [flag EXCEPT ![self] = FALSE]
+            /\ pc' = [pc EXCEPT ![self] = "enter"]
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ flag' = flag
+
+exit(self) == /\ pc[self] = "exit"
+              /\ flag' = [flag EXCEPT ![self] = FALSE]
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ cs(self)
+              \/ exit(self)
+
+Next == (\E self \in Procs: P(self))
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+\* END TRANSLATION 
+
+--------
+
+\* Invariant which implies MutualExclusion
+\*Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] = "e2"))
+Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3"}))
+
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"             ->  "cs"
+                                              [] pc[proc] \in {"enter","e2","e3"} ->  "csentry"
+                                              [] OTHER                       ->  "non-cs"]
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 21:21:36 MSK 2022 by kirr
+\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

1Bit.toolbox/.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>1Bit</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>1Bit.tla</name>
+			<type>1</type>
+			<locationURI>PARENT-1-PROJECT_LOC/1Bit.tla</locationURI>
+		</link>
+		<link>
+			<name>MutualExclusionSpec.tla</name>
+			<type>1</type>
+			<location>/home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.tla</location>
+		</link>
+	</linkedResources>
+</projectDescription>

1Bit.toolbox/.settings/org.lamport.tla.toolbox.prefs

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

1Bit.toolbox/1Bit.aux

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

1Bit.toolbox/1Bit.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 21:12
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**1Bit.tex
+(./1Bit.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
+) (./1Bit.aux)
+\openout1 = `1Bit.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 946.
+LaTeX Font Info:    External font `cmex10' loaded for size
+(Font)              <6> on input line 946.
+LaTeX Font Info:    Trying to load font information for OMS+cmr on input line 9
+63.
+(/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 963.
+[1
+
+{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
+Overfull \hbox (13.43173pt too wide) in paragraph at lines 1087--1089
+[][] 
+ []
+
+
+Overfull \hbox (83.84805pt too wide) in paragraph at lines 1089--1095
+[][][][] 
+ []
+
+
+Overfull \hbox (34.86755pt too wide) in paragraph at lines 1095--1096
+[][] 
+ []
+
+[2] (./1Bit.aux) ) 
+Here is how much of TeX's memory you used:
+ 1332 strings out of 479304
+ 18669 string characters out of 5869780
+ 316173 words of memory out of 5000000
+ 18554 multiletter control sequences out of 15000+600000
+ 409463 words of font info for 50 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 44i,11n,50p,213b,320s stack positions out of 5000i,500n,10000p,200000b,80000s
+</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
+/cmbsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx
+10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pf
+b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></us
+r/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/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-d
+ist/fonts/type1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/font
+s/type1/public/amsfonts/cm/cmss10.pfb></usr/share/texlive/texmf-dist/fonts/type
+1/public/amsfonts/cm/cmss8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
+c/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
+onts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
+/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10
+.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti7.pfb></
+usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/sha
+re/texlive/texmf-dist/fonts/type1/public/amsfonts/latxfont/lasy10.pfb>
+Output written on 1Bit.pdf (2 pages, 172310 bytes).
+PDF statistics:
+ 79 PDF objects out of 1000 (max. 8388607)
+ 57 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)
+

1Bit.toolbox/1Bit___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="37"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430443440.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_1644430443440"/>
+    <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="82"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430451766.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_1644430451766"/>
+    <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="119"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430485644.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_1644430485644"/>
+    <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="31"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430510155.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_1644430510155"/>
+    <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="30"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430518151.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_1644430518151"/>
+    <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="93"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430537188.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_1644430537188"/>
+    <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="4"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430548616.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_1644430548616"/>
+    <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="70"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430556719.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_1644430556719"/>
+    <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="76"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="1ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430725151.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_1644430725151"/>
+    <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="44"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/1Bit___Model_1_SnapShot_1644430854275.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_1644430854275"/>
+    <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="37"/>
+    <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="flag, pc"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="1Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="1ME!Liveness"/>
+    </listAttribute>
+    <intAttribute key="modelEditorOpenTabs" value="8"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="N;;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="1Bit"/>
+    <stringAttribute key="tlcResourcesProfile" value="local custom"/>
+    <stringAttribute key="view" value=""/>
+    <booleanAttribute key="visualizeStateGraph" value="true"/>
+</launchConfiguration>

1Bit.toolbox/Model_1/1Bit.tla

+-------------------------------- MODULE 1Bit --------------------------------
+\* 1Bit implementation of mutual exclusion
+EXTENDS Integers
+
+CONSTANT N
+ASSUME N \in Nat
+
+Procs == 0..N
+
+(********
+--algorithm 1BitProtocol {
+    variables flag = [i \in Procs |-> FALSE] ;
+    process (P \in Procs) {
+     ncs: while (TRUE) {
+            skip ; 
+     enter: flag[self] := TRUE ; 
+        e2: if (flag[1-self]) {
+        e3:   flag[self] := FALSE;
+              goto enter;
+            };
+        cs: skip ;
+      exit: flag[self] := FALSE ;            
+    }
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "b33e7cec" /\ chksum(tla) = "338dfe4c")
+VARIABLES flag, pc
+
+vars == << flag, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ flag = [i \in Procs |-> FALSE]
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ flag' = flag
+
+enter(self) == /\ pc[self] = "enter"
+               /\ flag' = [flag EXCEPT ![self] = TRUE]
+               /\ pc' = [pc EXCEPT ![self] = "e2"]
+
+e2(self) == /\ pc[self] = "e2"
+            /\ IF flag[1-self]
+                  THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
+                  ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
+            /\ flag' = flag
+
+e3(self) == /\ pc[self] = "e3"
+            /\ flag' = [flag EXCEPT ![self] = FALSE]
+            /\ pc' = [pc EXCEPT ![self] = "enter"]
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ flag' = flag
+
+exit(self) == /\ pc[self] = "exit"
+              /\ flag' = [flag EXCEPT ![self] = FALSE]
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ cs(self)
+              \/ exit(self)
+
+Next == (\E self \in Procs: P(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+--------
+
+\* Invariant which implies MutualExclusion
+\*Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] = "e2"))
+Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3"}))
+
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"             ->  "cs"
+                                              [] pc[proc] \in {"enter","e2","e3"} ->  "csentry"
+                                              [] OTHER                       ->  "non-cs"]
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 21:20:48 MSK 2022 by kirr
+\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

1Bit.toolbox/Model_1/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    N <- const_1644430852007674000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644430852007675000
+Inv
+\* PROPERTY definition
+PROPERTY
+prop_1644430852007677000
+\* Generated on Wed Feb 09 21:20:52 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1/MC.tla

+---- MODULE MC ----
+EXTENDS 1Bit, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_1644430852007674000 == 
+1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644430852007675000 ==
+ME!MutualExclusion
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644430852007677000 ==
+ME!Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 21:20:52 MSK 2022 by kirr

1Bit.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.
+\* Non-critical state is represented as "non-cs".
+\* When process decides it want to enter into critical-section, it first goes into "csentry" state.
+CONSTANT Procs
+VARIABLES pc
+
+TypeOK == pc \in [Procs -> {"non-cs", "csentry", "cs"}]
+
+vars == <<pc>>
+
+\* All processes start from non-critical section.
+Init == pc \in [Procs -> {"non-cs"}]
+
+\* WantCS(proc) is action when proc decides that it wants to enter into critical section.
+WantCS(proc) ==
+        /\ pc[proc] = "non-cs"
+        /\ pc' = [pc EXCEPT ![proc] = "csentry"]
+
+\* EnterCS(proc) is action when proc enters critical section.
+EnterCS(proc) ==
+        /\ pc[proc] = "csentry"
+        /\ \A i \in Procs \ {proc} : 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: WantCS(i) \/ EnterCS(i) \/ ExitCS(i)
+
+
+Spec == /\ Init
+        /\ [][Next]_vars
+        /\ \A i \in Procs: (            \* fairness
+            \* not fair for WantCS - it can pause and even hang there
+            /\ 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] = "csentry") ~> (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 19:11:11 MSK 2022 by kirr
+\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644430443440/1Bit.tla

+-------------------------------- MODULE 1Bit --------------------------------
+\* 1Bit implementation of mutual exclusion
+EXTENDS Integers
+
+CONSTANT N
+ASSUME N \in Nat
+
+Procs == 0..N
+
+(********
+--algorithm 1BitProtocol {
+    variables flag = [i \in Procs |-> FALSE] ;
+    process (P \in Procs) {
+     ncs: while (TRUE) {
+            skip ; 
+     enter: flag[self] := TRUE ; 
+        e2: if (flag[1-self]) {
+        e3:   flag[self] := FALSE;
+              goto enter;
+            };
+        cs: skip ;
+      exit: flag[self] := FALSE ;            
+    }
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "b33e7cec" /\ chksum(tla) = "338dfe4c")
+VARIABLES flag, pc
+
+vars == << flag, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ flag = [i \in Procs |-> FALSE]
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ flag' = flag
+
+enter(self) == /\ pc[self] = "enter"
+               /\ flag' = [flag EXCEPT ![self] = TRUE]
+               /\ pc' = [pc EXCEPT ![self] = "e2"]
+
+e2(self) == /\ pc[self] = "e2"
+            /\ IF flag[1-self]
+                  THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
+                  ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
+            /\ flag' = flag
+
+e3(self) == /\ pc[self] = "e3"
+            /\ flag' = [flag EXCEPT ![self] = FALSE]
+            /\ pc' = [pc EXCEPT ![self] = "enter"]
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ flag' = flag
+
+exit(self) == /\ pc[self] = "exit"
+              /\ flag' = [flag EXCEPT ![self] = FALSE]
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ cs(self)
+              \/ exit(self)
+
+Next == (\E self \in Procs: P(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+--------
+
+\* Invariant which implies MutualExclusion
+\*Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] = "e2"))
+Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3"}))
+
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"             ->  "cs"
+                                              [] pc[proc] \in {"enter","e2"} ->  "csentry"  \* XXX +e3
+                                              [] OTHER                       ->  "non-cs"]
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 21:13:48 MSK 2022 by kirr
+\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644430443440/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    N <- const_1644430441430619000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644430441430620000
+Inv
+\* Generated on Wed Feb 09 21:14:01 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1_SnapShot_1644430443440/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 82 and seed -655975556858912913 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 78566] (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/1Bit.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/1Bit.toolbox/Model_1/1Bit.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/1Bit.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 1Bit
+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 21:14:01)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 1 distinct state generated at 2022-02-09 21:14:02.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@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 = 5.7E-17
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 21:14:02
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 34, col 1 to line 34, col 4 of module 1Bit>: 1:1
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  line 35, col 19 to line 35, col 41 of module 1Bit: 1:2
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 35, col 26 to line 35, col 30 of module 1Bit: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 36, col 12 to line 36, col 44 of module 1Bit: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 36, col 17 to line 36, col 44 of module 1Bit: 1:2
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 36, col 27 to line 36, col 33 of module 1Bit: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 38, col 1 to line 38, col 9 of module 1Bit>: 3:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 38, col 17 to line 38, col 32 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 38, col 17 to line 38, col 24 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 39, col 17 to line 39, col 20 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 40, col 17 to line 40, col 51 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 17 to line 41, col 28 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 43, col 1 to line 43, col 11 of module 1Bit>: 8:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 43, col 19 to line 43, col 36 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 43, col 19 to line 43, col 26 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 19 to line 44, col 54 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 19 to line 45, col 50 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<e2 line 47, col 1 to line 47, col 8 of module 1Bit>: 10:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 16 to line 47, col 30 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 47, col 16 to line 47, col 23 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 48, col 19 to line 48, col 30 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 24 to line 49, col 58 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 24 to line 50, col 58 of module 1Bit: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 16 to line 51, col 27 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<e3 line 53, col 1 to line 53, col 8 of module 1Bit>: 2:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 53, col 16 to line 53, col 30 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 53, col 16 to line 53, col 23 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 52 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 50 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 57, col 1 to line 57, col 8 of module 1Bit>: 6:8
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 30 of module 1Bit: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 57, col 16 to line 57, col 23 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 58, col 16 to line 58, col 19 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 16 to line 59, col 49 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 16 to line 60, col 27 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 62, col 1 to line 62, col 10 of module 1Bit>: 2:8
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 62, col 18 to line 62, col 34 of module 1Bit: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 62, col 18 to line 62, col 25 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 63, col 18 to line 63, col 54 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 64, col 18 to line 64, col 50 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644430441430620000 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: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 83, col 23 to line 85, col 90 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 82, col 1 to line 85, col 90 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 128
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 128
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<Inv line 79, col 1 to line 79, col 3 of module 1Bit>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 79, col 8 to line 79, col 94 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 79, col 25 to line 79, col 94 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 79, col 26 to line 79, col 37 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 79, col 44 to line 79, col 93 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 79, col 44 to line 79, col 50 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 79, col 56 to line 79, col 92 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 79, col 56 to line 79, col 65 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 79, col 70 to line 79, col 92 of module 1Bit: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 79, col 17 to line 79, col 21 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(9) at 2022-02-09 21:14:02: 65 states generated (3 025 s/min), 32 distinct states found (1 489 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+65 states generated, 32 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 9.
+@!@!@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 1297ms at (2022-02-09 21:14:02)
+@!@!@ENDMSG 2186 @!@!@

1Bit.toolbox/Model_1_SnapShot_1644430443440/MC.tla

+---- MODULE MC ----
+EXTENDS 1Bit, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_1644430441430619000 == 
+1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644430441430620000 ==
+ME!MutualExclusion
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 21:14:01 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644430443440/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 82 and seed -655975556858912913 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 78566] (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/1Bit.toolbox/Model_1/MC.tla
+Parsing file /home/kirr/study/tla+/pluscal/ME/1Bit.toolbox/Model_1/1Bit.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/1Bit.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 1Bit
+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 21:14:01)
+@!@!@ENDMSG 2185 @!@!@
+@!@!@STARTMSG 2189:0 @!@!@
+Computing initial states...
+@!@!@ENDMSG 2189 @!@!@
+@!@!@STARTMSG 2190:0 @!@!@
+Finished computing initial states: 1 distinct state generated at 2022-02-09 21:14:02.
+@!@!@ENDMSG 2190 @!@!@
+@!@!@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 = 5.7E-17
+@!@!@ENDMSG 2193 @!@!@
+@!@!@STARTMSG 2201:0 @!@!@
+The coverage statistics at 2022-02-09 21:14:02
+@!@!@ENDMSG 2201 @!@!@
+@!@!@STARTMSG 2773:0 @!@!@
+<Init line 34, col 1 to line 34, col 4 of module 1Bit>: 1:1
+@!@!@ENDMSG 2773 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  line 35, col 19 to line 35, col 41 of module 1Bit: 1:2
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 35, col 26 to line 35, col 30 of module 1Bit: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 36, col 12 to line 36, col 44 of module 1Bit: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2775:0 @!@!@
+  |line 36, col 17 to line 36, col 44 of module 1Bit: 1:2
+@!@!@ENDMSG 2775 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 36, col 27 to line 36, col 33 of module 1Bit: 1
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<ncs line 38, col 1 to line 38, col 9 of module 1Bit>: 3:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 38, col 17 to line 38, col 32 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 38, col 17 to line 38, col 24 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 39, col 17 to line 39, col 20 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 40, col 17 to line 40, col 51 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 41, col 17 to line 41, col 28 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<enter line 43, col 1 to line 43, col 11 of module 1Bit>: 8:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 43, col 19 to line 43, col 36 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 43, col 19 to line 43, col 26 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 44, col 19 to line 44, col 54 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 45, col 19 to line 45, col 50 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<e2 line 47, col 1 to line 47, col 8 of module 1Bit>: 10:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 47, col 16 to line 47, col 30 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 47, col 16 to line 47, col 23 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 48, col 19 to line 48, col 30 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 49, col 24 to line 49, col 58 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 50, col 24 to line 50, col 58 of module 1Bit: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 51, col 16 to line 51, col 27 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<e3 line 53, col 1 to line 53, col 8 of module 1Bit>: 2:12
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 53, col 16 to line 53, col 30 of module 1Bit: 76
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 53, col 16 to line 53, col 23 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 54, col 16 to line 54, col 52 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 55, col 16 to line 55, col 50 of module 1Bit: 12
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<cs line 57, col 1 to line 57, col 8 of module 1Bit>: 6:8
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 57, col 16 to line 57, col 30 of module 1Bit: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 57, col 16 to line 57, col 23 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 58, col 16 to line 58, col 19 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 59, col 16 to line 59, col 49 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 60, col 16 to line 60, col 27 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2772:0 @!@!@
+<exit line 62, col 1 to line 62, col 10 of module 1Bit>: 2:8
+@!@!@ENDMSG 2772 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 62, col 18 to line 62, col 34 of module 1Bit: 72
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 62, col 18 to line 62, col 25 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 63, col 18 to line 63, col 54 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 64, col 18 to line 64, col 50 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<inv_1644430441430620000 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: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 83, col 23 to line 85, col 90 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 82, col 1 to line 85, col 90 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 128
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 128
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2774:0 @!@!@
+<Inv line 79, col 1 to line 79, col 3 of module 1Bit>
+@!@!@ENDMSG 2774 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  line 79, col 8 to line 79, col 94 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 79, col 25 to line 79, col 94 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 79, col 26 to line 79, col 37 of module 1Bit: 64
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||line 79, col 44 to line 79, col 93 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 79, col 44 to line 79, col 50 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |||line 79, col 56 to line 79, col 92 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 79, col 56 to line 79, col 65 of module 1Bit: 8
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  ||||line 79, col 70 to line 79, col 92 of module 1Bit: 4
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2221:0 @!@!@
+  |line 79, col 17 to line 79, col 21 of module 1Bit: 32
+@!@!@ENDMSG 2221 @!@!@
+@!@!@STARTMSG 2202:0 @!@!@
+End of statistics.
+@!@!@ENDMSG 2202 @!@!@
+@!@!@STARTMSG 2200:0 @!@!@
+Progress(9) at 2022-02-09 21:14:02: 65 states generated (3 025 s/min), 32 distinct states found (1 489 ds/min), 0 states left on queue.
+@!@!@ENDMSG 2200 @!@!@
+@!@!@STARTMSG 2199:0 @!@!@
+65 states generated, 32 distinct states found, 0 states left on queue.
+@!@!@ENDMSG 2199 @!@!@
+@!@!@STARTMSG 2194:0 @!@!@
+The depth of the complete state graph search is 9.
+@!@!@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 1297ms at (2022-02-09 21:14:02)
+@!@!@ENDMSG 2186 @!@!@

1Bit.toolbox/Model_1_SnapShot_1644430443440/Model_1_SnapShot_1644430443440.dot

+strict digraph DiskGraph {
+edge [colorscheme="paired12"]
+nodesep=0.35;
+subgraph cluster_graph {
+color="white";
+-8207800682143011604 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")",style = filled]
+-8207800682143011604 -> -1898859409693584170 [label="",color="2",fontcolor="2"];
+-1898859409693584170 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")"];
+-8207800682143011604 -> 8680679855716785430 [label="",color="2",fontcolor="2"];
+8680679855716785430 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")"];
+8680679855716785430 -> 2609446035001071015 [label="",color="2",fontcolor="2"];
+2609446035001071015 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")"];
+-1898859409693584170 -> 649276215269042678 [label="",color="3",fontcolor="3"];
+649276215269042678 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"ncs\")"];
+8680679855716785430 -> -3513800155198664853 [label="",color="3",fontcolor="3"];
+-3513800155198664853 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e2\")"];
+-1898859409693584170 -> 2609446035001071015 [label="",color="2",fontcolor="2"];
+2609446035001071015 -> 8566278427511381018 [label="",color="3",fontcolor="3"];
+8566278427511381018 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"enter\")"];
+649276215269042678 -> -7515084137797002991 [label="",color="4",fontcolor="4"];
+-7515084137797002991 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")"];
+2609446035001071015 -> -4134979692026463607 [label="",color="3",fontcolor="3"];
+-4134979692026463607 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e2\")"];
+649276215269042678 -> 8566278427511381018 [label="",color="2",fontcolor="2"];
+-3513800155198664853 -> -4134979692026463607 [label="",color="2",fontcolor="2"];
+8566278427511381018 -> -9205930425329188375 [label="",color="4",fontcolor="4"];
+-9205930425329188375 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")"];
+-3513800155198664853 -> 7641499007996120982 [label="",color="4",fontcolor="4"];
+7641499007996120982 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")"];
+8566278427511381018 -> -638942661406916565 [label="",color="3",fontcolor="3"];
+-638942661406916565 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e2\")"];
+-7515084137797002991 -> 8770575480411227391 [label="",color="5",fontcolor="5"];
+8770575480411227391 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")"];
+-4134979692026463607 -> -638942661406916565 [label="",color="3",fontcolor="3"];
+-7515084137797002991 -> -9205930425329188375 [label="",color="2",fontcolor="2"];
+-4134979692026463607 -> 7182659061744073332 [label="",color="4",fontcolor="4"];
+7182659061744073332 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")"];
+-9205930425329188375 -> -6790909092300373228 [label="",color="5",fontcolor="5"];
+-6790909092300373228 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")"];
+7641499007996120982 -> 7182659061744073332 [label="",color="2",fontcolor="2"];
+-9205930425329188375 -> -8172443221505060476 [label="",color="3",fontcolor="3"];
+-8172443221505060476 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e2\")"];
+-638942661406916565 -> -6573916343649216732 [label="",color="4",fontcolor="4"];
+-6573916343649216732 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"e2\")"];
+7641499007996120982 -> 735209579287226230 [label="",color="5",fontcolor="5"];
+735209579287226230 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")"];
+-638942661406916565 -> 8121221749300902528 [label="",color="4",fontcolor="4"];
+8121221749300902528 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e3\")"];
+8770575480411227391 -> -8207800682143011604 [label="",color="6",fontcolor="6"];
+7182659061744073332 -> 5913915379457949910 [label="",color="3",fontcolor="3"];
+5913915379457949910 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"cs\")"];
+8770575480411227391 -> -6790909092300373228 [label="",color="2",fontcolor="2"];
+7182659061744073332 -> -1702765690716794846 [label="",color="5",fontcolor="5"];
+-1702765690716794846 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")"];
+-6790909092300373228 -> 8680679855716785430 [label="",color="6",fontcolor="6"];
+-6790909092300373228 -> -5317099644774915964 [label="",color="3",fontcolor="3"];
+-5317099644774915964 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e2\")"];
+-8172443221505060476 -> -5317099644774915964 [label="",color="5",fontcolor="5"];
+-8172443221505060476 -> 649577310333856559 [label="",color="4",fontcolor="4"];
+649577310333856559 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e3\")"];
+-6573916343649216732 -> -4134979692026463607 [label="",color="7",fontcolor="7"];
+-6573916343649216732 -> 2545277908219948431 [label="",color="4",fontcolor="4"];
+2545277908219948431 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"e3\")"];
+8121221749300902528 -> 2545277908219948431 [label="",color="4",fontcolor="4"];
+8121221749300902528 -> 8566278427511381018 [label="",color="7",fontcolor="7"];
+5913915379457949910 -> 140937972380293081 [label="",color="4",fontcolor="4"];
+140937972380293081 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"cs\")"];
+5913915379457949910 -> -7176741646622990333 [label="",color="5",fontcolor="5"];
+-7176741646622990333 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"exit\")"];
+-1702765690716794846 -> -7176741646622990333 [label="",color="3",fontcolor="3"];
+-1702765690716794846 -> -1898859409693584170 [label="",color="6",fontcolor="6"];
+-5317099644774915964 -> -3513800155198664853 [label="",color="6",fontcolor="6"];
+-5317099644774915964 -> 3576908294812064303 [label="",color="4",fontcolor="4"];
+3576908294812064303 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e3\")"];
+649577310333856559 -> 3576908294812064303 [label="",color="5",fontcolor="5"];
+649577310333856559 -> -9205930425329188375 [label="",color="7",fontcolor="7"];
+2545277908219948431 -> 4687117803347558434 [label="",color="7",fontcolor="7"];
+4687117803347558434 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e3\")"];
+2545277908219948431 -> -3663462464026719478 [label="",color="7",fontcolor="7"];
+-3663462464026719478 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"enter\")"];
+140937972380293081 -> 7182659061744073332 [label="",color="7",fontcolor="7"];
+140937972380293081 -> 5212372912309122395 [label="",color="5",fontcolor="5"];
+5212372912309122395 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"exit\")"];
+-7176741646622990333 -> 5212372912309122395 [label="",color="4",fontcolor="4"];
+735209579287226230 -> -1702765690716794846 [label="",color="2",fontcolor="2"];
+735209579287226230 -> -8207800682143011604 [label="",color="6",fontcolor="6"];
+3576908294812064303 -> 5236028646528251328 [label="",color="6",fontcolor="6"];
+5236028646528251328 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e3\")"];
+3576908294812064303 -> -6790909092300373228 [label="",color="7",fontcolor="7"];
+4687117803347558434 -> 8121221749300902528 [label="",color="3",fontcolor="3"];
+4687117803347558434 -> 2609446035001071015 [label="",color="7",fontcolor="7"];
+-3663462464026719478 -> 2609446035001071015 [label="",color="7",fontcolor="7"];
+-3663462464026719478 -> -6573916343649216732 [label="",color="3",fontcolor="3"];
+5212372912309122395 -> -1702765690716794846 [label="",color="7",fontcolor="7"];
+5212372912309122395 -> 1953735775303871838 [label="",color="6",fontcolor="6"];
+1953735775303871838 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"ncs\")"];
+5236028646528251328 -> 4687117803347558434 [label="",color="2",fontcolor="2"];
+5236028646528251328 -> 8680679855716785430 [label="",color="7",fontcolor="7"];
+1953735775303871838 -> -1898859409693584170 [label="",color="7",fontcolor="7"];
+1953735775303871838 -> -3663462464026719478 [label="",color="2",fontcolor="2"];
+-7176741646622990333 -> 649276215269042678 [label="",color="6",fontcolor="6"];
+{rank = same; -8207800682143011604;}
+{rank = same; -1898859409693584170;8680679855716785430;}
+{rank = same; 649276215269042678;2609446035001071015;-3513800155198664853;}
+{rank = same; -7515084137797002991;8566278427511381018;-4134979692026463607;7641499007996120982;}
+{rank = same; -9205930425329188375;735209579287226230;7182659061744073332;-638942661406916565;8770575480411227391;}
+{rank = same; 8121221749300902528;-8172443221505060476;-1702765690716794846;-6790909092300373228;-6573916343649216732;5913915379457949910;}
+{rank = same; 2545277908219948431;-7176741646622990333;649577310333856559;140937972380293081;-5317099644774915964;}
+{rank = same; 3576908294812064303;4687117803347558434;-3663462464026719478;5212372912309122395;}
+{rank = same; 5236028646528251328;1953735775303871838;}
+}
+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=5]
+exit [label="exit",fillcolor=6]
+enter [label="enter",fillcolor=3]
+e2 [label="e2",fillcolor=4]
+e3 [label="e3",fillcolor=7]
+ncs [label="ncs",fillcolor=2]
+}}
\ No newline at end of file

1Bit.toolbox/Model_1_SnapShot_1644430443440/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.
+\* Non-critical state is represented as "non-cs".
+\* When process decides it want to enter into critical-section, it first goes into "csentry" state.
+CONSTANT Procs
+VARIABLES pc
+
+TypeOK == pc \in [Procs -> {"non-cs", "csentry", "cs"}]
+
+vars == <<pc>>
+
+\* All processes start from non-critical section.
+Init == pc \in [Procs -> {"non-cs"}]
+
+\* WantCS(proc) is action when proc decides that it wants to enter into critical section.
+WantCS(proc) ==
+        /\ pc[proc] = "non-cs"
+        /\ pc' = [pc EXCEPT ![proc] = "csentry"]
+
+\* EnterCS(proc) is action when proc enters critical section.
+EnterCS(proc) ==
+        /\ pc[proc] = "csentry"
+        /\ \A i \in Procs \ {proc} : 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: WantCS(i) \/ EnterCS(i) \/ ExitCS(i)
+
+
+Spec == /\ Init
+        /\ [][Next]_vars
+        /\ \A i \in Procs: (            \* fairness
+            \* not fair for WantCS - it can pause and even hang there
+            /\ 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] = "csentry") ~> (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 19:11:11 MSK 2022 by kirr
+\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644430451766/1Bit.tla

+-------------------------------- MODULE 1Bit --------------------------------
+\* 1Bit implementation of mutual exclusion
+EXTENDS Integers
+
+CONSTANT N
+ASSUME N \in Nat
+
+Procs == 0..N
+
+(********
+--algorithm 1BitProtocol {
+    variables flag = [i \in Procs |-> FALSE] ;
+    process (P \in Procs) {
+     ncs: while (TRUE) {
+            skip ; 
+     enter: flag[self] := TRUE ; 
+        e2: if (flag[1-self]) {
+        e3:   flag[self] := FALSE;
+              goto enter;
+            };
+        cs: skip ;
+      exit: flag[self] := FALSE ;            
+    }
+  }
+}
+********)
+\* BEGIN TRANSLATION (chksum(pcal) = "b33e7cec" /\ chksum(tla) = "338dfe4c")
+VARIABLES flag, pc
+
+vars == << flag, pc >>
+
+ProcSet == (Procs)
+
+Init == (* Global variables *)
+        /\ flag = [i \in Procs |-> FALSE]
+        /\ pc = [self \in ProcSet |-> "ncs"]
+
+ncs(self) == /\ pc[self] = "ncs"
+             /\ TRUE
+             /\ pc' = [pc EXCEPT ![self] = "enter"]
+             /\ flag' = flag
+
+enter(self) == /\ pc[self] = "enter"
+               /\ flag' = [flag EXCEPT ![self] = TRUE]
+               /\ pc' = [pc EXCEPT ![self] = "e2"]
+
+e2(self) == /\ pc[self] = "e2"
+            /\ IF flag[1-self]
+                  THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
+                  ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
+            /\ flag' = flag
+
+e3(self) == /\ pc[self] = "e3"
+            /\ flag' = [flag EXCEPT ![self] = FALSE]
+            /\ pc' = [pc EXCEPT ![self] = "enter"]
+
+cs(self) == /\ pc[self] = "cs"
+            /\ TRUE
+            /\ pc' = [pc EXCEPT ![self] = "exit"]
+            /\ flag' = flag
+
+exit(self) == /\ pc[self] = "exit"
+              /\ flag' = [flag EXCEPT ![self] = FALSE]
+              /\ pc' = [pc EXCEPT ![self] = "ncs"]
+
+P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ cs(self)
+              \/ exit(self)
+
+Next == (\E self \in Procs: P(self))
+
+Spec == Init /\ [][Next]_vars
+
+\* END TRANSLATION 
+
+--------
+
+\* Invariant which implies MutualExclusion
+\*Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] = "e2"))
+Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3"}))
+
+
+ME == INSTANCE MutualExclusionSpec WITH
+                pc <- [proc \in Procs  |->  CASE pc[proc] = "cs"             ->  "cs"
+                                              [] pc[proc] \in {"enter","e2"} ->  "csentry"  \* XXX +e3
+                                              [] OTHER                       ->  "non-cs"]
+
+THEOREM Spec => ME!Spec
+THEOREM Spec => []ME!MutualExclusion
+THEOREM Spec => ME!Liveness
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Feb 09 21:13:48 MSK 2022 by kirr
+\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644430451766/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    N <- const_1644430449414626000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644430449414627000
+Inv
+\* PROPERTY definition
+PROPERTY
+prop_1644430449414629000
+\* Generated on Wed Feb 09 21:14:09 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1_SnapShot_1644430451766/MC.tla

+---- MODULE MC ----
+EXTENDS 1Bit, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_1644430449414626000 == 
+1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644430449414627000 ==
+ME!MutualExclusion
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644430449414629000 ==
+ME!Spec
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 21:14:09 MSK 2022 by kirr

1Bit.toolbox/Model_1_SnapShot_1644430485644/MC.cfg

+\* CONSTANT definitions
+
+CONSTANT
+    N <- const_1644430483467630000
+\* SPECIFICATION definition
+SPECIFICATION
+Spec
+\* INVARIANT definition
+INVARIANT
+inv_1644430483467631000
+Inv
+\* PROPERTY definition
+PROPERTY
+prop_1644430483467633000
+\* Generated on Wed Feb 09 21:14:43 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1_SnapShot_1644430485644/MC.tla

+---- MODULE MC ----
+EXTENDS 1Bit, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_1644430483467630000 == 
+1
+----
+
+\* INVARIANT definition @modelCorrectnessInvariants:0
+inv_1644430483467631000 ==
+ME!MutualExclusion
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_1644430483467633000 ==
+ME!Spec
+----
+=============================================================================
+\* Modification History
+\* Created Wed Feb 09 21:14:43 MSK 2022 by kirr