Skip to content

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

.

parent 3b4c3b8d
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 42486 additions and 10178 deletions
1Bit.tla
View file @ ed1ebf84
......@@ -7,69 +7,92 @@ ASSUME N \in Nat
Procs == 0..N
\* PlusCal options (wf)
(********
--fair algorithm 1BitProtocol {
variables flag = [i \in Procs |-> FALSE] ;
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: flag[self] := FALSE;
goto enter;
e3: if (self /= turn) {
e4: flag[self] := FALSE;
goto e3;
}
else {
goto enter;
}
};
cs: skip ;
exit: flag[self] := FALSE ;
exit: flag[self] := FALSE ;
x2: turn := 1-self;
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "b89f1da2")
VARIABLES flag, pc
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "55b6bf32")
VARIABLES flag, turn, pc
vars == << flag, 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"]
/\ flag' = flag
/\ 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"]
/\ flag' = flag
/\ 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] = "enter"]
/\ pc' = [pc EXCEPT ![self] = "e3"]
/\ turn' = turn
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ flag' = flag
/\ UNCHANGED << flag, turn >>
exit(self) == /\ pc[self] = "exit"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ 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) \/ cs(self)
\/ exit(self)
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
/\ WF_vars(Next)
/\ \A self \in Procs : WF_vars(P(self))
\* END TRANSLATION
......@@ -77,12 +100,13 @@ Spec == /\ Init /\ [][Next]_vars
\* 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"}))
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"} -> "csentry"
[] pc[proc] \in {"enter","e2","e3","e4","e5"} -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
......@@ -92,5 +116,5 @@ THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 21:21:36 MSK 2022 by kirr
\* Last modified Wed Feb 09 22:17:21 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/1Bit___Model_1.launch
View file @ ed1ebf84
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="37"/>
<intAttribute key="fpIndex" value="45"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......@@ -22,15 +22,15 @@
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="flag, pc"/>
<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="1Inv"/>
<listEntry value="0Inv"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="0ME!Spec"/>
<listEntry value="1ME!Spec"/>
<listEntry value="1ME!Liveness"/>
</listAttribute>
<intAttribute key="modelEditorOpenTabs" value="8"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430451766.launch deleted 100644 → 0
View file @ 3b4c3b8d
<?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 deleted 100644 → 0
View file @ 3b4c3b8d
<?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 deleted 100644 → 0
View file @ 3b4c3b8d
<?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_1644430443440.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644433275573.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430443440"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644433275573"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="82"/>
<intAttribute key="fpIndex" value="87"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430556719.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644433283403.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430556719"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644433283403"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="76"/>
<intAttribute key="fpIndex" value="38"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430725151.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644433294610.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430725151"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644433294610"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="44"/>
<intAttribute key="fpIndex" value="85"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430518151.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644433925073.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430518151"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644433925073"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="93"/>
<intAttribute key="fpIndex" value="92"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430537188.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644433946303.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430537188"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644433946303"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="4"/>
<intAttribute key="fpIndex" value="8"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......@@ -22,12 +22,12 @@
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="flag, pc"/>
<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="1Inv"/>
<listEntry value="0Inv"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="0ME!Spec"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430854275.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644433971559.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430854275"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644433971559"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="37"/>
<intAttribute key="fpIndex" value="94"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......@@ -22,12 +22,12 @@
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="flag, pc"/>
<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="1Inv"/>
<listEntry value="0Inv"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="0ME!Spec"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644430548616.launch → 1Bit.toolbox/1Bit___Model_1_SnapShot_1644434035514.launch
View file @ ed1ebf84
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644430548616"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644434035514"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="70"/>
<intAttribute key="fpIndex" value="126"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......@@ -22,12 +22,12 @@
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="flag, pc"/>
<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="1Inv"/>
<listEntry value="0Inv"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="0ME!Spec"/>
......
1Bit.toolbox/1Bit___Model_1_SnapShot_1644434045039.launch 0 → 100644
View file @ ed1ebf84
<?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 0 → 100644
View file @ ed1ebf84
<?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 0 → 100644
View file @ ed1ebf84
<?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/Model_1/1Bit.tla
View file @ ed1ebf84
......@@ -7,68 +7,92 @@ ASSUME N \in Nat
Procs == 0..N
\* PlusCal options (wf)
(********
--algorithm 1BitProtocol {
variables flag = [i \in Procs |-> FALSE] ;
--fair 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: flag[self] := FALSE;
goto enter;
e3: if (self /= turn) {
e4: flag[self] := FALSE;
goto e3;
}
else {
goto enter;
}
};
cs: skip ;
exit: flag[self] := FALSE ;
exit: flag[self] := FALSE ;
x2: turn := 1-self;
}
}
}
********)
\* BEGIN TRANSLATION (chksum(pcal) = "b33e7cec" /\ chksum(tla) = "338dfe4c")
VARIABLES flag, pc
\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "55b6bf32")
VARIABLES flag, turn, pc
vars == << flag, 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"]
/\ flag' = flag
/\ 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"]
/\ flag' = flag
/\ 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] = "enter"]
/\ pc' = [pc EXCEPT ![self] = "e3"]
/\ turn' = turn
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "exit"]
/\ flag' = flag
/\ UNCHANGED << flag, turn >>
exit(self) == /\ pc[self] = "exit"
/\ flag' = [flag EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "ncs"]
/\ 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) \/ cs(self)
\/ exit(self)
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
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
/\ \A self \in Procs : WF_vars(P(self))
\* END TRANSLATION
......@@ -76,12 +100,13 @@ Spec == Init /\ [][Next]_vars
\* 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"}))
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"} -> "csentry"
[] pc[proc] \in {"enter","e2","e3","e4","e5"} -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
......@@ -91,5 +116,5 @@ THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 21:20:48 MSK 2022 by kirr
\* Last modified Wed Feb 09 22:17:21 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1/MC.cfg
View file @ ed1ebf84
\* CONSTANT definitions
CONSTANT
N <- const_1644430852007674000
N <- const_1644434264801795000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644430852007675000
Inv
inv_1644434264801796000
\* PROPERTY definition
PROPERTY
prop_1644430852007677000
\* Generated on Wed Feb 09 21:20:52 MSK 2022
\ No newline at end of file
prop_1644434264801797000
prop_1644434264801798000
\* Generated on Wed Feb 09 22:17:44 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1/MC.out
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1/MC.tla
View file @ ed1ebf84
......@@ -2,18 +2,22 @@
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644430852007674000 ==
const_1644434264801795000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644430852007675000 ==
inv_1644434264801796000 ==
ME!MutualExclusion
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644430852007677000 ==
prop_1644434264801797000 ==
ME!Spec
----
\* PROPERTY definition @modelCorrectnessProperties:1
prop_1644434264801798000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 21:20:52 MSK 2022 by kirr
\* Created Wed Feb 09 22:17:44 MSK 2022 by kirr
1Bit.toolbox/Model_1/MC_TE.out
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1/Model_1.dot
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1/Model_1_liveness.dot
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430443440/Model_1_SnapShot_1644430443440.dot deleted 100644 → 0
View file @ 3b4c3b8d
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_1644430451766/1Bit.tla deleted 100644 → 0
View file @ 3b4c3b8d
-------------------------------- 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.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430451766/MC.tla deleted 100644 → 0
View file @ 3b4c3b8d
---- 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_1644430451766/MC_TE.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430451766/Model_1_SnapShot_1644430451766.dot deleted 100644 → 0
View file @ 3b4c3b8d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
-8180625305189782138 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")",style = filled]
-8180625305189782138 -> -7609163839008188290 [label="",color="2",fontcolor="2"];
-7609163839008188290 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")"];
-7609163839008188290 -> -7922199982538667910 [label="",color="3",fontcolor="3"];
-7922199982538667910 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"ncs\")"];
-8180625305189782138 -> -4383264161169425949 [label="",color="2",fontcolor="2"];
-4383264161169425949 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")"];
-8180625305189782138 -> -8180625305189782138 [style="dashed"];
-7609163839008188290 -> -3675294217639243219 [label="",color="2",fontcolor="2"];
-3675294217639243219 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")"];
-7609163839008188290 -> -7609163839008188290 [style="dashed"];
-4383264161169425949 -> -3675294217639243219 [label="",color="2",fontcolor="2"];
-4383264161169425949 -> 9018875693532074086 [label="",color="3",fontcolor="3"];
9018875693532074086 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e2\")"];
-7922199982538667910 -> -7793968603789164143 [label="",color="4",fontcolor="4"];
-7793968603789164143 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")"];
-7922199982538667910 -> -3874340436594278200 [label="",color="2",fontcolor="2"];
-3874340436594278200 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"enter\")"];
-4383264161169425949 -> -4383264161169425949 [style="dashed"];
-7922199982538667910 -> -7922199982538667910 [style="dashed"];
-3675294217639243219 -> -3874340436594278200 [label="",color="3",fontcolor="3"];
-7793968603789164143 -> 4253599211768313444 [label="",color="5",fontcolor="5"];
4253599211768313444 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")"];
-7793968603789164143 -> 3711068830523647112 [label="",color="2",fontcolor="2"];
3711068830523647112 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")"];
-3675294217639243219 -> -5035101028236171738 [label="",color="3",fontcolor="3"];
-5035101028236171738 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e2\")"];
-7793968603789164143 -> -7793968603789164143 [style="dashed"];
-3675294217639243219 -> -3675294217639243219 [style="dashed"];
9018875693532074086 -> -5035101028236171738 [label="",color="2",fontcolor="2"];
9018875693532074086 -> 3988182878549589540 [label="",color="4",fontcolor="4"];
3988182878549589540 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")"];
-3874340436594278200 -> 3711068830523647112 [label="",color="4",fontcolor="4"];
-3874340436594278200 -> -2834413970213349273 [label="",color="3",fontcolor="3"];
-2834413970213349273 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e2\")"];
9018875693532074086 -> 9018875693532074086 [style="dashed"];
-3874340436594278200 -> -3874340436594278200 [style="dashed"];
4253599211768313444 -> -8180625305189782138 [label="",color="6",fontcolor="6"];
4253599211768313444 -> -1929385232942358230 [label="",color="2",fontcolor="2"];
-1929385232942358230 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")"];
3711068830523647112 -> -1929385232942358230 [label="",color="5",fontcolor="5"];
3711068830523647112 -> 6355215896392948780 [label="",color="3",fontcolor="3"];
6355215896392948780 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e2\")"];
4253599211768313444 -> 4253599211768313444 [style="dashed"];
3711068830523647112 -> 3711068830523647112 [style="dashed"];
-5035101028236171738 -> -2834413970213349273 [label="",color="3",fontcolor="3"];
3988182878549589540 -> -1121925374597724060 [label="",color="2",fontcolor="2"];
-1121925374597724060 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")"];
-5035101028236171738 -> -1121925374597724060 [label="",color="4",fontcolor="4"];
3988182878549589540 -> 6669566137860664447 [label="",color="5",fontcolor="5"];
6669566137860664447 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")"];
-5035101028236171738 -> -5035101028236171738 [style="dashed"];
3988182878549589540 -> 3988182878549589540 [style="dashed"];
-2834413970213349273 -> 7754420173991579283 [label="",color="4",fontcolor="4"];
7754420173991579283 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"e2\")"];
-1929385232942358230 -> -4383264161169425949 [label="",color="6",fontcolor="6"];
-1929385232942358230 -> 1062096503402119812 [label="",color="3",fontcolor="3"];
1062096503402119812 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e2\")"];
-1929385232942358230 -> -1929385232942358230 [style="dashed"];
6355215896392948780 -> 1062096503402119812 [label="",color="5",fontcolor="5"];
6355215896392948780 -> -5687246051361371229 [label="",color="4",fontcolor="4"];
-5687246051361371229 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e3\")"];
-2834413970213349273 -> -2834413970213349273 [style="dashed"];
6355215896392948780 -> 6355215896392948780 [style="dashed"];
{rank = same; -8180625305189782138;}
{rank = same; -4383264161169425949;-7609163839008188290;}
{rank = same; -3675294217639243219;9018875693532074086;-7922199982538667910;}
{rank = same; 3988182878549589540;-5035101028236171738;-7793968603789164143;-3874340436594278200;}
{rank = same; 4253599211768313444;-2834413970213349273;3711068830523647112;}
{rank = same; 6355215896392948780;-1929385232942358230;}
}
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]
ncs [label="ncs",fillcolor=2]
}}
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644430451766/Model_1_liveness.dot deleted 100644 → 0
View file @ 3b4c3b8d
digraph DiskGraph {
nodesep=0.35;
subgraph cluster_graph {
color="white";
-8180625305189782138 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")",style = filled]
-8180625305189782138 -> -4383264161169425949;
-4383264161169425949 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")"];
-8180625305189782138 -> -8180625305189782138;
-8180625305189782138 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")"];
-8180625305189782138 -> -7609163839008188290;
-7609163839008188290 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")"];
-7609163839008188290 -> -7922199982538667910;
-7922199982538667910 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"ncs\")"];
-7609163839008188290 -> -3675294217639243219;
-3675294217639243219 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")"];
-7609163839008188290 -> -7609163839008188290;
-7609163839008188290 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")"];
-4383264161169425949 -> -4383264161169425949;
-4383264161169425949 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")"];
-4383264161169425949 -> 9018875693532074086;
9018875693532074086 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e2\")"];
-4383264161169425949 -> -3675294217639243219;
-3675294217639243219 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")"];
-7922199982538667910 -> -7793968603789164143;
-7793968603789164143 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")"];
-7922199982538667910 -> -3874340436594278200;
-3874340436594278200 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"enter\")"];
-7922199982538667910 -> -7922199982538667910;
-7922199982538667910 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"ncs\")"];
-7793968603789164143 -> -7793968603789164143;
-7793968603789164143 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")"];
-7793968603789164143 -> 4253599211768313444;
4253599211768313444 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")"];
-7793968603789164143 -> 3711068830523647112;
3711068830523647112 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")"];
-3675294217639243219 -> -5035101028236171738;
-5035101028236171738 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e2\")"];
-3675294217639243219 -> -3874340436594278200;
-3874340436594278200 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"enter\")"];
-3675294217639243219 -> -3675294217639243219;
-3675294217639243219 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")"];
9018875693532074086 -> 3988182878549589540;
3988182878549589540 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")"];
9018875693532074086 -> -5035101028236171738;
-5035101028236171738 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e2\")"];
9018875693532074086 -> 9018875693532074086;
9018875693532074086 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e2\")"];
-3874340436594278200 -> -2834413970213349273;
-2834413970213349273 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e2\")"];
-3874340436594278200 -> 3711068830523647112;
3711068830523647112 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")"];
-3874340436594278200 -> -3874340436594278200;
-3874340436594278200 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"enter\")"];
4253599211768313444 -> 4253599211768313444;
4253599211768313444 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")"];
4253599211768313444 -> -8180625305189782138;
4253599211768313444 -> -1929385232942358230;
-1929385232942358230 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")"];
3711068830523647112 -> 3711068830523647112;
3711068830523647112 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")"];
3711068830523647112 -> -1929385232942358230;
-1929385232942358230 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")"];
3711068830523647112 -> 6355215896392948780;
6355215896392948780 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e2\")"];
-5035101028236171738 -> -1121925374597724060;
-1121925374597724060 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")"];
-5035101028236171738 -> -5035101028236171738;
-5035101028236171738 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e2\")"];
-5035101028236171738 -> -2834413970213349273;
-2834413970213349273 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e2\")"];
3988182878549589540 -> -1121925374597724060;
-1121925374597724060 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")"];
3988182878549589540 -> 3988182878549589540;
3988182878549589540 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")"];
3988182878549589540 -> 6669566137860664447;
6669566137860664447 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")"];
-1929385232942358230 -> -4383264161169425949;
-1929385232942358230 -> 1062096503402119812;
1062096503402119812 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e2\")"];
-1929385232942358230 -> -1929385232942358230;
-1929385232942358230 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")"];
-2834413970213349273 -> 7754420173991579283;
7754420173991579283 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"e2\")"];
-2834413970213349273 -> -2834413970213349273;
-2834413970213349273 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e2\")"];
6355215896392948780 -> -5687246051361371229;
-5687246051361371229 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e3\")"];
6355215896392948780 -> 1062096503402119812;
1062096503402119812 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e2\")"];
6355215896392948780 -> 6355215896392948780;
6355215896392948780 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e2\")"];
{rank = same; -8180625305189782138;}
{rank = same; -4383264161169425949;-7609163839008188290;}
{rank = same; -3675294217639243219;9018875693532074086;-7922199982538667910;}
{rank = same; 3988182878549589540;-5035101028236171738;-7793968603789164143;-3874340436594278200;}
{rank = same; 4253599211768313444;-2834413970213349273;3711068830523647112;}
{rank = same; 6355215896392948780;-1929385232942358230;}
}
}
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644430485644/MC.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430485644/MC_TE.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430510155/1Bit.tla deleted 100644 → 0
View file @ 3b4c3b8d
-------------------------------- 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:14:33 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644430510155/MC.tla deleted 100644 → 0
View file @ 3b4c3b8d
---- MODULE MC ----
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644430508144637000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644430508144638000 ==
ME!MutualExclusion
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 21:15:08 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644430510155/Model_1_SnapShot_1644430510155.dot deleted 100644 → 0
View file @ 3b4c3b8d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
-6515837008146365232 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")",style = filled]
-6515837008146365232 -> -4247917108933016673 [label="",color="2",fontcolor="2"];
-4247917108933016673 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")"];
-4247917108933016673 -> -898250698584901607 [label="",color="3",fontcolor="3"];
-898250698584901607 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"ncs\")"];
-6515837008146365232 -> 4036757553934324923 [label="",color="2",fontcolor="2"];
4036757553934324923 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")"];
-4247917108933016673 -> -4922100213422929728 [label="",color="2",fontcolor="2"];
-4922100213422929728 [label="/\\ flag = (0 :> FALSE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")"];
-898250698584901607 -> 7793522680819297578 [label="",color="4",fontcolor="4"];
7793522680819297578 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")"];
4036757553934324923 -> -4922100213422929728 [label="",color="2",fontcolor="2"];
4036757553934324923 -> -7287612873189951241 [label="",color="3",fontcolor="3"];
-7287612873189951241 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e2\")"];
-898250698584901607 -> 8653120271346862012 [label="",color="2",fontcolor="2"];
8653120271346862012 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"enter\")"];
-4922100213422929728 -> 8653120271346862012 [label="",color="3",fontcolor="3"];
7793522680819297578 -> 1785664340797347593 [label="",color="5",fontcolor="5"];
1785664340797347593 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")"];
-4922100213422929728 -> -4674815136845484689 [label="",color="3",fontcolor="3"];
-4674815136845484689 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e2\")"];
7793522680819297578 -> 4530344404360063248 [label="",color="2",fontcolor="2"];
4530344404360063248 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")"];
-7287612873189951241 -> -4674815136845484689 [label="",color="2",fontcolor="2"];
-7287612873189951241 -> 5128195396982357909 [label="",color="4",fontcolor="4"];
5128195396982357909 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")"];
8653120271346862012 -> 4530344404360063248 [label="",color="4",fontcolor="4"];
8653120271346862012 -> 3588732711430858786 [label="",color="3",fontcolor="3"];
3588732711430858786 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e2\")"];
1785664340797347593 -> -6515837008146365232 [label="",color="6",fontcolor="6"];
1785664340797347593 -> -9113897206107998634 [label="",color="2",fontcolor="2"];
-9113897206107998634 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")"];
4530344404360063248 -> -9113897206107998634 [label="",color="5",fontcolor="5"];
4530344404360063248 -> -2442406105713677994 [label="",color="3",fontcolor="3"];
-2442406105713677994 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e2\")"];
5128195396982357909 -> 7127377804322892301 [label="",color="2",fontcolor="2"];
7127377804322892301 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")"];
-4674815136845484689 -> 3588732711430858786 [label="",color="3",fontcolor="3"];
-4674815136845484689 -> 7127377804322892301 [label="",color="4",fontcolor="4"];
3588732711430858786 -> 2140554630751355069 [label="",color="4",fontcolor="4"];
2140554630751355069 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"e2\")"];
5128195396982357909 -> 5650706283625711273 [label="",color="5",fontcolor="5"];
5650706283625711273 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")"];
-9113897206107998634 -> 4036757553934324923 [label="",color="6",fontcolor="6"];
-9113897206107998634 -> -1779660285414009524 [label="",color="3",fontcolor="3"];
-1779660285414009524 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e2\")"];
-2442406105713677994 -> -1779660285414009524 [label="",color="5",fontcolor="5"];
-2442406105713677994 -> 9076914252222203863 [label="",color="4",fontcolor="4"];
9076914252222203863 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"cs\" @@ 1 :> \"e3\")"];
3588732711430858786 -> -7917111957982067037 [label="",color="4",fontcolor="4"];
-7917111957982067037 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"e3\")"];
7127377804322892301 -> -1424389430357594304 [label="",color="3",fontcolor="3"];
-1424389430357594304 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"cs\")"];
5650706283625711273 -> -7819575803077928763 [label="",color="2",fontcolor="2"];
-7819575803077928763 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")"];
7127377804322892301 -> -7819575803077928763 [label="",color="5",fontcolor="5"];
5650706283625711273 -> -6515837008146365232 [label="",color="6",fontcolor="6"];
-1779660285414009524 -> -7287612873189951241 [label="",color="6",fontcolor="6"];
-1779660285414009524 -> 4944980547195993037 [label="",color="4",fontcolor="4"];
4944980547195993037 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"exit\" @@ 1 :> \"e3\")"];
9076914252222203863 -> 4944980547195993037 [label="",color="5",fontcolor="5"];
9076914252222203863 -> 4530344404360063248 [label="",color="7",fontcolor="7"];
-7917111957982067037 -> -4730540040142000580 [label="",color="4",fontcolor="4"];
-4730540040142000580 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"e3\")"];
-7917111957982067037 -> 8653120271346862012 [label="",color="7",fontcolor="7"];
-1424389430357594304 -> -4592836921153075233 [label="",color="4",fontcolor="4"];
-4592836921153075233 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"cs\")"];
-1424389430357594304 -> -3889935132254212952 [label="",color="5",fontcolor="5"];
-3889935132254212952 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e2\" @@ 1 :> \"exit\")"];
-7819575803077928763 -> -3889935132254212952 [label="",color="3",fontcolor="3"];
-7819575803077928763 -> -4247917108933016673 [label="",color="6",fontcolor="6"];
4944980547195993037 -> 4120876439759263350 [label="",color="6",fontcolor="6"];
4120876439759263350 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"ncs\" @@ 1 :> \"e3\")"];
4944980547195993037 -> -9113897206107998634 [label="",color="7",fontcolor="7"];
-4730540040142000580 -> 2085942450272519150 [label="",color="7",fontcolor="7"];
2085942450272519150 [label="/\\ flag = (0 :> FALSE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"enter\" @@ 1 :> \"e3\")"];
-4730540040142000580 -> 6374315077046870841 [label="",color="7",fontcolor="7"];
6374315077046870841 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"enter\")"];
-4592836921153075233 -> 7127377804322892301 [label="",color="7",fontcolor="7"];
-4592836921153075233 -> -9199678861996253596 [label="",color="5",fontcolor="5"];
-9199678861996253596 [label="/\\ flag = (0 :> TRUE @@ 1 :> TRUE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"exit\")"];
-3889935132254212952 -> -9199678861996253596 [label="",color="4",fontcolor="4"];
-3889935132254212952 -> -898250698584901607 [label="",color="6",fontcolor="6"];
4120876439759263350 -> 2085942450272519150 [label="",color="2",fontcolor="2"];
4120876439759263350 -> 4036757553934324923 [label="",color="7",fontcolor="7"];
2085942450272519150 -> -7917111957982067037 [label="",color="3",fontcolor="3"];
2085942450272519150 -> -4922100213422929728 [label="",color="7",fontcolor="7"];
6374315077046870841 -> -4922100213422929728 [label="",color="7",fontcolor="7"];
6374315077046870841 -> 2140554630751355069 [label="",color="3",fontcolor="3"];
-9199678861996253596 -> -7819575803077928763 [label="",color="7",fontcolor="7"];
-9199678861996253596 -> -5313569148024031452 [label="",color="6",fontcolor="6"];
-5313569148024031452 [label="/\\ flag = (0 :> TRUE @@ 1 :> FALSE)\n/\\ pc = (0 :> \"e3\" @@ 1 :> \"ncs\")"];
2140554630751355069 -> -4674815136845484689 [label="",color="7",fontcolor="7"];
-5313569148024031452 -> -4247917108933016673 [label="",color="7",fontcolor="7"];
2140554630751355069 -> -4730540040142000580 [label="",color="4",fontcolor="4"];
-5313569148024031452 -> 6374315077046870841 [label="",color="2",fontcolor="2"];
{rank = same; -6515837008146365232;}
{rank = same; 4036757553934324923;-4247917108933016673;}
{rank = same; -4922100213422929728;-898250698584901607;-7287612873189951241;}
{rank = same; -4674815136845484689;5128195396982357909;7793522680819297578;8653120271346862012;}
{rank = same; 1785664340797347593;3588732711430858786;7127377804322892301;4530344404360063248;5650706283625711273;}
{rank = same; -1424389430357594304;2140554630751355069;-9113897206107998634;-7917111957982067037;-2442406105713677994;-7819575803077928763;}
{rank = same; -1779660285414009524;-4730540040142000580;-4592836921153075233;9076914252222203863;-3889935132254212952;}
{rank = same; 2085942450272519150;4944980547195993037;-9199678861996253596;6374315077046870841;}
{rank = same; -5313569148024031452;4120876439759263350;}
}
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_1644430518151/1Bit.tla deleted 100644 → 0
View file @ 3b4c3b8d
-------------------------------- 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:14:33 MSK 2022 by kirr
\* Created Wed Feb 09 20:01:56 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644430518151/MC.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430518151/MC_TE.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430548616/MC.cfg deleted 100644 → 0
View file @ 3b4c3b8d
\* CONSTANT definitions
CONSTANT
N <- const_1644430546606655000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644430546606656000
Inv
\* Generated on Wed Feb 09 21:15:46 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644430556719/MC.cfg deleted 100644 → 0
View file @ 3b4c3b8d
\* CONSTANT definitions
CONSTANT
N <- const_1644430554364662000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644430554365663000
Inv
\* PROPERTY definition
PROPERTY
prop_1644430554365665000
\* Generated on Wed Feb 09 21:15:54 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644430556719/MC.tla deleted 100644 → 0
View file @ 3b4c3b8d
---- MODULE MC ----
EXTENDS 1Bit, TLC
\* CONSTANT definitions @modelParameterConstants:0N
const_1644430554364662000 ==
1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644430554365663000 ==
ME!MutualExclusion
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644430554365665000 ==
ME!Spec
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 21:15:54 MSK 2022 by kirr
1Bit.toolbox/Model_1_SnapShot_1644430725151/MC.cfg deleted 100644 → 0
View file @ 3b4c3b8d
\* CONSTANT definitions
CONSTANT
N <- const_1644430722260670000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644430722260671000
Inv
\* PROPERTY definition
PROPERTY
prop_1644430722260673000
\* Generated on Wed Feb 09 21:18:42 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644430854275/1Bit.tla deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430854275/MC.cfg deleted 100644 → 0
View file @ 3b4c3b8d
\* 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_SnapShot_1644430854275/MC.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430854275/MC_TE.out deleted 100644 → 0
View file @ 3b4c3b8d
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644430443440/MC.cfg → 1Bit.toolbox/Model_1_SnapShot_1644433275573/MC.cfg
View file @ ed1ebf84
\* CONSTANT definitions
CONSTANT
N <- const_1644430441430619000
N <- const_1644433273561746000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644430441430620000
inv_1644433273561747000
Inv
\* Generated on Wed Feb 09 21:14:01 MSK 2022
\ No newline at end of file
\* Generated on Wed Feb 09 22:01:13 MSK 2022
\ No newline at end of file
1Bit.toolbox/Model_1_SnapShot_1644433925073/MC.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433925073/MC_TE.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433946303/MC.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433946303/MC_TE.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644433971559/MC.cfg 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434035514/1Bit.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/1Bit.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC.cfg 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434045039/MC_TE.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/1Bit.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/MC.cfg 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434259076/MC.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/1Bit.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC.cfg 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC.out 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC.tla 0 → 100644
View file @ ed1ebf84
This diff is collapsed.
1Bit.toolbox/Model_1_SnapShot_1644434267815/MC_TE.out 0 → 100644
View file @ ed1ebf84
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