Skip to content

K
KTLA Study
Commit 8699f9d6 authored by Kirill Smelkov's avatar Kirill Smelkov
Browse files
Options

.

parent 8507525a
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 0 additions and 68853 deletions
1Bit.toolbox/1Bit___Model_1_SnapShot_1644433294610.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644433294610"/>
<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="85"/>
<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_1644433925073.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644433925073"/>
<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="92"/>
<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_1644433946303.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644433946303"/>
<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="8"/>
<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="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_1644433971559.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644433971559"/>
<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="94"/>
<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="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_1644434035514.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644434035514"/>
<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="126"/>
<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"/>
</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_1644434045039.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644434045039"/>
<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="74"/>
<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="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_1644434259076.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644434259076"/>
<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="40"/>
<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="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_1644434267815.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644434267815"/>
<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="45"/>
<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="1ME!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_1644434389260.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644434389260"/>
<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="16"/>
<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="1ME!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_1644486204136.launch deleted 100644 → 0
View file @ 8507525a
<?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_1644486204136"/>
<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="77"/>
<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="1ME!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_SnapShot_1644433294610/1Bit.tla deleted 100644 → 0
View file @ 8507525a
-------------------------------- 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: if (self = 0) {
goto e2
}
else {
flag[self] := FALSE;
e4: await ~flag[1-self];
goto enter;
}
};
cs: skip ;
exit: flag[self] := FALSE ;
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "fe37cc8e")
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"
/\ IF self = 0
THEN /\ pc' = [pc EXCEPT ![self] = "e2"]
/\ flag' = flag
ELSE /\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "e4"]
e4(self) == /\ pc[self] = "e4"
/\ ~flag[1-self]
/\ pc' = [pc EXCEPT ![self] = "enter"]
/\ flag' = flag
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) \/ e4(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"}))
Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3","e4"}))
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] \in {"enter","e2","e3","e4","e5"} -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 22:01:10 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433294610/MC.cfg deleted 100644 → 0
View file @ 8507525a
\* CONSTANT definitions
CONSTANT
N <- const_1644433292600761000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644433292600762000
Inv
\* PROPERTY definition
PROPERTY
prop_1644433292600764000
\* Generated on Wed Feb 09 22:01:32 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644433294610/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433294610/MC.tla deleted 100644 → 0
View file @ 8507525a
---- MODULE MC ----
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644433292600761000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644433292600762000 ==
ME!MutualExclusion
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644433292600764000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 22:01:32 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433294610/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433294610/MutualExclusionSpec.tla deleted 100644 → 0
View file @ 8507525a
------------------------ 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_1644433925073/1Bit.tla deleted 100644 → 0
View file @ 8507525a
-------------------------------- 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], turn = 0 ;
process (P \in Procs) {
ncs: while (TRUE) {
skip ;
enter: flag[self] := TRUE ;
e2: if (flag[1-self]) {
e3: if (self /= turn) {
e4: flag[self] := FALSE;
goto e3;
}
else {
goto enter;
}
};
cs: skip ;
exit: flag[self] := FALSE ;
x2: turn := 1-self;
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "e4a49cfa" /\ chksum(tla) = "d8e21c7a")
VARIABLES flag, turn, pc
vars == << flag, turn, pc >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ flag = [i \in Procs |-> FALSE]
/\ turn = 0
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << flag, turn >>
enter(self) == /\ pc[self] = "enter"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "e2"]
/\ turn' = turn
e2(self) == /\ pc[self] = "e2"
/\ IF flag[1-self]
THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ UNCHANGED << flag, turn >>
e3(self) == /\ pc[self] = "e3"
/\ IF self /= turn
THEN /\ pc' = [pc EXCEPT ![self] = "e4"]
ELSE /\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << flag, turn >>
e4(self) == /\ pc[self] = "e4"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "e3"]
/\ turn' = turn
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ UNCHANGED << flag, turn >>
exit(self) == /\ pc[self] = "exit"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "x2"]
/\ turn' = turn
x2(self) == /\ pc[self] = "x2"
/\ turn' = 1-self
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ flag' = flag
P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(self)
\/ cs(self) \/ exit(self) \/ x2(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"}))
Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3","e4"}))
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] \in {"enter","e2","e3","e4","e5"} -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 22:11:57 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433925073/MC.cfg deleted 100644 → 0
View file @ 8507525a
\* CONSTANT definitions
CONSTANT
N <- const_1644433922629765000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644433922629766000
Inv
\* PROPERTY definition
PROPERTY
prop_1644433922629768000
\* Generated on Wed Feb 09 22:12:02 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644433925073/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433925073/MC.tla deleted 100644 → 0
View file @ 8507525a
---- MODULE MC ----
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644433922629765000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644433922629766000 ==
ME!MutualExclusion
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644433922629768000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 22:12:02 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433925073/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433925073/MutualExclusionSpec.tla deleted 100644 → 0
View file @ 8507525a
------------------------ 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_1644433946303/1Bit.tla deleted 100644 → 0
View file @ 8507525a
-------------------------------- 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], turn = 0 ;
process (P \in Procs) {
ncs: while (TRUE) {
skip ;
enter: flag[self] := TRUE ;
e2: if (flag[1-self]) {
e3: if (self /= turn) {
e4: flag[self] := FALSE;
goto e3;
}
else {
goto enter;
}
};
cs: skip ;
exit: flag[self] := FALSE ;
x2: turn := 1-self;
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "e4a49cfa" /\ chksum(tla) = "d8e21c7a")
VARIABLES flag, turn, pc
vars == << flag, turn, pc >>
ProcSet == (Procs)
Init == (* Global variables *)
/\ flag = [i \in Procs |-> FALSE]
/\ turn = 0
/\ pc = [self \in ProcSet |-> "ncs"]
ncs(self) == /\ pc[self] = "ncs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << flag, turn >>
enter(self) == /\ pc[self] = "enter"
/\ flag' = [flag EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "e2"]
/\ turn' = turn
e2(self) == /\ pc[self] = "e2"
/\ IF flag[1-self]
THEN /\ pc' = [pc EXCEPT ![self] = "e3"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ UNCHANGED << flag, turn >>
e3(self) == /\ pc[self] = "e3"
/\ IF self /= turn
THEN /\ pc' = [pc EXCEPT ![self] = "e4"]
ELSE /\ pc' = [pc EXCEPT ![self] = "enter"]
/\ UNCHANGED << flag, turn >>
e4(self) == /\ pc[self] = "e4"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "e3"]
/\ turn' = turn
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ UNCHANGED << flag, turn >>
exit(self) == /\ pc[self] = "exit"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "x2"]
/\ turn' = turn
x2(self) == /\ pc[self] = "x2"
/\ turn' = 1-self
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ flag' = flag
P(self) == ncs(self) \/ enter(self) \/ e2(self) \/ e3(self) \/ e4(self)
\/ cs(self) \/ exit(self) \/ x2(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"}))
Inv == \A i \in Procs : (pc[i] = "cs") => (flag[i] /\ (~flag[1-i] \/ pc[1-i] \in {"e2","e3","e4"}))
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] \in {"enter","e2","e3","e4","e5"} -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 22:11:57 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433946303/MC.cfg deleted 100644 → 0
View file @ 8507525a
\* CONSTANT definitions
CONSTANT
N <- const_1644433944293772000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644433944293773000
\* PROPERTY definition
PROPERTY
prop_1644433944293774000
\* Generated on Wed Feb 09 22:12:24 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644433946303/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433946303/MC.tla deleted 100644 → 0
View file @ 8507525a
---- MODULE MC ----
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644433944293772000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644433944293773000 ==
ME!MutualExclusion
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644433944293774000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 22:12:24 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433946303/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433946303/MutualExclusionSpec.tla deleted 100644 → 0
View file @ 8507525a
------------------------ 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_1644433971559/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433971559/MC.cfg deleted 100644 → 0
View file @ 8507525a
\* CONSTANT definitions
CONSTANT
N <- const_1644433968542775000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644433968543776000
\* PROPERTY definition
PROPERTY
prop_1644433968543777000
\* Generated on Wed Feb 09 22:12:48 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644433971559/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433971559/MC.tla deleted 100644 → 0
View file @ 8507525a
---- MODULE MC ----
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644433968542775000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644433968543776000 ==
ME!MutualExclusion
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644433968543777000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 22:12:48 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644433971559/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434035514/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434035514/MC.cfg deleted 100644 → 0
View file @ 8507525a
\* CONSTANT definitions
CONSTANT
N <- const_1644434033205780000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644434033205781000
\* Generated on Wed Feb 09 22:13:53 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644434035514/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434035514/MC.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434035514/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC.cfg deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/MC.cfg deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/MC.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC.cfg deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434389260/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434389260/MC.cfg deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434389260/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434389260/MC.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434389260/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644486204136/1Bit.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644486204136/MC.cfg deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644486204136/MC.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644486204136/MC.tla deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644486204136/MC_TE.out deleted 100644 → 0
View file @ 8507525a
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment
GitLab Nexedi Edition | About GitLab | About Nexedi | 沪ICP备2021021310号-2 | 沪ICP备2021021310号-7