.

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="64"/>
+    <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, turn"/>
+    <stringAttribute key="modelComments" value=""/>
+    <booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
+    <listAttribute key="modelCorrectnessInvariants">
+        <listEntry value="1ME!MutualExclusion"/>
+        <listEntry value="0Inv"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties">
+        <listEntry value="0ME!Spec"/>
+        <listEntry value="0ME!Liveness"/>
+        <listEntry value="0Live0"/>
+        <listEntry value="0Live1"/>
+    </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/MC.cfg

-\* CONSTANT definitions
-
-CONSTANT
-    N <- const_1644486201121915000
-\* SPECIFICATION definition
-SPECIFICATION
-Spec
-\* INVARIANT definition
-INVARIANT
-inv_1644486201121916000
-\* PROPERTY definition
-PROPERTY
-prop_1644486201121917000
-prop_1644486201121918000
-\* Generated on Thu Feb 10 12:43:21 MSK 2022
\ No newline at end of file

1Bit.toolbox/Model_1/MC.tla

----- MODULE MC ----
-EXTENDS 1Bit, TLC
-
-\* CONSTANT definitions @modelParameterConstants:0N
-const_1644486201121915000 == 
-1
-----
-
-\* INVARIANT definition @modelCorrectnessInvariants:0
-inv_1644486201121916000 ==
-ME!MutualExclusion
-----
-\* PROPERTY definition @modelCorrectnessProperties:0
-prop_1644486201121917000 ==
-ME!Spec
-----
-\* PROPERTY definition @modelCorrectnessProperties:1
-prop_1644486201121918000 ==
-ME!Liveness
-----
-=============================================================================
-\* Modification History
-\* Created Thu Feb 10 12:43:21 MSK 2022 by kirr