Skip to content

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

Trying to satisfy Dijkstra II 

	Any processes may take arbitrarily long to execute its noncritical
	section, and may even halt there.  Other processes must be able to enter the
	critical section without having to wait for those processes to complete the
	noncritical section.
parent 253af10d
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 4946 additions and 2546 deletions
Alternate.tla
View file @ 7d001ca6
......@@ -75,9 +75,9 @@ Spec == /\ Init /\ [][Next]_vars
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> IF pc[proc] = "cs" THEN "cs"
ELSE "non-cs"]
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] = "enter" -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
......@@ -85,5 +85,5 @@ THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 18:03:45 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:58:34 MSK 2022 by kirr
\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr
Alternate.toolbox/Alternate___Model_1.launch
View file @ 7d001ca6
......@@ -13,7 +13,7 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="107"/>
<intAttribute key="fpIndex" value="90"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......
Alternate.toolbox/Alternate___Model_1_SnapShot_1644418425669.launch → Alternate.toolbox/Alternate___Model_1_SnapShot_1644425787608.launch
View file @ 7d001ca6
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644418425669"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644425787608"/>
<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="96"/>
<intAttribute key="fpIndex" value="88"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......@@ -27,6 +27,7 @@
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1ME!MutualExclusion"/>
<listEntry value="1\A i \in Procs : (pc[i] = &quot;cs&quot;) =&gt; (turn = i)"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1ME!Spec"/>
......
Alternate.toolbox/Alternate___Model_1_SnapShot_1644418436130.launch → Alternate.toolbox/Alternate___Model_1_SnapShot_1644425917721.launch
View file @ 7d001ca6
......@@ -3,7 +3,7 @@
<stringAttribute key="TLCCmdLineParameters" value=""/>
<stringAttribute key="alias" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644418436130"/>
<stringAttribute key="configurationName" value="Model_1_SnapShot_1644425917721"/>
<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="55"/>
<intAttribute key="fpIndex" value="90"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="25"/>
<intAttribute key="maxSetSize" value="1000000"/>
......@@ -27,6 +27,7 @@
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1ME!MutualExclusion"/>
<listEntry value="1\A i \in Procs : (pc[i] = &quot;cs&quot;) =&gt; (turn = i)"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties">
<listEntry value="1ME!Spec"/>
......
Alternate.toolbox/Model_1/Alternate.tla
View file @ 7d001ca6
......@@ -75,9 +75,9 @@ Spec == /\ Init /\ [][Next]_vars
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> IF pc[proc] = "cs" THEN "cs"
ELSE "non-cs"]
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] = "enter" -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
......@@ -85,5 +85,5 @@ THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 18:03:45 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:58:34 MSK 2022 by kirr
\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr
Alternate.toolbox/Model_1/MC.cfg
View file @ 7d001ca6
\* CONSTANT definitions
CONSTANT
Procs <- const_1644421370985520000
Procs <- const_1644425915701562000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644421370985521000
inv_1644421370985522000
inv_1644425915701563000
inv_1644425915701564000
\* PROPERTY definition
PROPERTY
prop_1644421370985523000
prop_1644421370985524000
\* Generated on Wed Feb 09 18:42:50 MSK 2022
\ No newline at end of file
prop_1644425915701565000
prop_1644425915701566000
\* Generated on Wed Feb 09 19:58:35 MSK 2022
\ No newline at end of file
Alternate.toolbox/Model_1/MC.out
View file @ 7d001ca6
This diff is collapsed.
Alternate.toolbox/Model_1/MC.tla
View file @ 7d001ca6
......@@ -2,26 +2,26 @@
EXTENDS Alternate, TLC
\* CONSTANT definitions @modelParameterConstants:0Procs
const_1644421370985520000 ==
const_1644425915701562000 ==
0..1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644421370985521000 ==
inv_1644425915701563000 ==
ME!MutualExclusion
----
\* INVARIANT definition @modelCorrectnessInvariants:1
inv_1644421370985522000 ==
inv_1644425915701564000 ==
\A i \in Procs : (pc[i] = "cs") => (turn = i)
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644421370985523000 ==
prop_1644425915701565000 ==
ME!Spec
----
\* PROPERTY definition @modelCorrectnessProperties:1
prop_1644421370985524000 ==
prop_1644425915701566000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 18:42:50 MSK 2022 by kirr
\* Created Wed Feb 09 19:58:35 MSK 2022 by kirr
Alternate.toolbox/Model_1/MC_TE.out
View file @ 7d001ca6
This diff is collapsed.
Alternate.toolbox/Model_1/Model_1.dot
View file @ 7d001ca6
......@@ -3,67 +3,67 @@ edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
-400635202659742381 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
-1182823203390725160 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
-400635202659742381 -> -475001133580855070 [label="",color="2",fontcolor="2"];
-475001133580855070 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-400635202659742381 -> 4659978677738564643 [label="",color="2",fontcolor="2"];
4659978677738564643 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-400635202659742381 -> -400635202659742381 [style="dashed"];
-1182823203390725160 -> -1401437471233001879 [label="",color="2",fontcolor="2"];
-1401437471233001879 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
-1182823203390725160 -> 6147128843187323560 [label="",color="2",fontcolor="2"];
6147128843187323560 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
-1182823203390725160 -> -1182823203390725160 [style="dashed"];
-475001133580855070 -> 5240454219582294627 [label="",color="3",fontcolor="3"];
5240454219582294627 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-475001133580855070 -> 5064951816826678884 [label="",color="2",fontcolor="2"];
5064951816826678884 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-475001133580855070 -> -475001133580855070 [style="dashed"];
4659978677738564643 -> 5064951816826678884 [label="",color="2",fontcolor="2"];
4659978677738564643 -> 4659978677738564643 [style="dashed"];
-1401437471233001879 -> 6030106734495858927 [label="",color="2",fontcolor="2"];
6030106734495858927 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
-1401437471233001879 -> -1401437471233001879 [style="dashed"];
6147128843187323560 -> 6030106734495858927 [label="",color="2",fontcolor="2"];
5240454219582294627 -> 7049503415477998762 [label="",color="4",fontcolor="4"];
7049503415477998762 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
6147128843187323560 -> 6211392433518555324 [label="",color="3",fontcolor="3"];
6211392433518555324 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
5240454219582294627 -> 3923823433829631963 [label="",color="2",fontcolor="2"];
3923823433829631963 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
6147128843187323560 -> 6147128843187323560 [style="dashed"];
5240454219582294627 -> 5240454219582294627 [style="dashed"];
5064951816826678884 -> 3923823433829631963 [label="",color="3",fontcolor="3"];
5064951816826678884 -> 5064951816826678884 [style="dashed"];
6030106734495858927 -> 897235516867550670 [label="",color="3",fontcolor="3"];
897235516867550670 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
6030106734495858927 -> 6030106734495858927 [style="dashed"];
7049503415477998762 -> -1182823203390725160 [label="",color="5",fontcolor="5"];
7049503415477998762 -> 4069903303166039434 [label="",color="2",fontcolor="2"];
4069903303166039434 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
7049503415477998762 -> 7049503415477998762 [style="dashed"];
6211392433518555324 -> 897235516867550670 [label="",color="2",fontcolor="2"];
6211392433518555324 -> -9152277194294045646 [label="",color="4",fontcolor="4"];
-9152277194294045646 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
6211392433518555324 -> 6211392433518555324 [style="dashed"];
3923823433829631963 -> 4069903303166039434 [label="",color="4",fontcolor="4"];
3923823433829631963 -> 3923823433829631963 [style="dashed"];
897235516867550670 -> -2015577958311089194 [label="",color="4",fontcolor="4"];
-2015577958311089194 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
897235516867550670 -> 897235516867550670 [style="dashed"];
4069903303166039434 -> 6147128843187323560 [label="",color="5",fontcolor="5"];
4069903303166039434 -> 4069903303166039434 [style="dashed"];
-9152277194294045646 -> -2015577958311089194 [label="",color="2",fontcolor="2"];
-9152277194294045646 -> -400635202659742381 [label="",color="5",fontcolor="5"];
-9152277194294045646 -> -9152277194294045646 [style="dashed"];
-2015577958311089194 -> -475001133580855070 [label="",color="5",fontcolor="5"];
-2015577958311089194 -> -2015577958311089194 [style="dashed"];
{rank = same; -1182823203390725160;-400635202659742381;}
{rank = same; 4659978677738564643;-1401437471233001879;6147128843187323560;-475001133580855070;}
{rank = same; 6030106734495858927;6211392433518555324;5240454219582294627;5064951816826678884;}
{rank = same; 3923823433829631963;7049503415477998762;897235516867550670;-9152277194294045646;}
{rank = same; -2015577958311089194;4069903303166039434;}
-2304256186017901240 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
3063590532813598594 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
-2304256186017901240 -> 4021501492038283011 [label="",color="2",fontcolor="2"];
4021501492038283011 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-2304256186017901240 -> -4661709328420890533 [label="",color="2",fontcolor="2"];
-4661709328420890533 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-2304256186017901240 -> -2304256186017901240 [style="dashed"];
3063590532813598594 -> -194057057360964151 [label="",color="2",fontcolor="2"];
-194057057360964151 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
3063590532813598594 -> 8489255053443179153 [label="",color="2",fontcolor="2"];
8489255053443179153 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
3063590532813598594 -> 3063590532813598594 [style="dashed"];
4021501492038283011 -> 543325479923207427 [label="",color="3",fontcolor="3"];
543325479923207427 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
4021501492038283011 -> 244470699041366076 [label="",color="2",fontcolor="2"];
244470699041366076 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
4021501492038283011 -> 4021501492038283011 [style="dashed"];
-4661709328420890533 -> 244470699041366076 [label="",color="2",fontcolor="2"];
-4661709328420890533 -> -4661709328420890533 [style="dashed"];
-194057057360964151 -> -3898669630605452554 [label="",color="2",fontcolor="2"];
-3898669630605452554 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
8489255053443179153 -> -3898669630605452554 [label="",color="2",fontcolor="2"];
-194057057360964151 -> -194057057360964151 [style="dashed"];
8489255053443179153 -> 6208733498515523769 [label="",color="3",fontcolor="3"];
6208733498515523769 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
8489255053443179153 -> 8489255053443179153 [style="dashed"];
543325479923207427 -> -6395493111282828260 [label="",color="4",fontcolor="4"];
-6395493111282828260 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
543325479923207427 -> 1580961522298426183 [label="",color="2",fontcolor="2"];
1580961522298426183 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
543325479923207427 -> 543325479923207427 [style="dashed"];
244470699041366076 -> 1580961522298426183 [label="",color="3",fontcolor="3"];
244470699041366076 -> 244470699041366076 [style="dashed"];
-3898669630605452554 -> 5921214264002221941 [label="",color="3",fontcolor="3"];
5921214264002221941 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
-3898669630605452554 -> -3898669630605452554 [style="dashed"];
6208733498515523769 -> 5921214264002221941 [label="",color="2",fontcolor="2"];
6208733498515523769 -> -8187951950540390906 [label="",color="4",fontcolor="4"];
-8187951950540390906 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
6208733498515523769 -> 6208733498515523769 [style="dashed"];
-6395493111282828260 -> 3063590532813598594 [label="",color="5",fontcolor="5"];
-6395493111282828260 -> 8639444591122381034 [label="",color="2",fontcolor="2"];
8639444591122381034 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-6395493111282828260 -> -6395493111282828260 [style="dashed"];
1580961522298426183 -> 8639444591122381034 [label="",color="4",fontcolor="4"];
5921214264002221941 -> -8265530133940623444 [label="",color="4",fontcolor="4"];
-8265530133940623444 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
1580961522298426183 -> 1580961522298426183 [style="dashed"];
5921214264002221941 -> 5921214264002221941 [style="dashed"];
-8187951950540390906 -> -8265530133940623444 [label="",color="2",fontcolor="2"];
-8187951950540390906 -> -2304256186017901240 [label="",color="5",fontcolor="5"];
8639444591122381034 -> 8489255053443179153 [label="",color="5",fontcolor="5"];
-8187951950540390906 -> -8187951950540390906 [style="dashed"];
8639444591122381034 -> 8639444591122381034 [style="dashed"];
-8265530133940623444 -> 4021501492038283011 [label="",color="5",fontcolor="5"];
-8265530133940623444 -> -8265530133940623444 [style="dashed"];
{rank = same; -2304256186017901240;3063590532813598594;}
{rank = same; -194057057360964151;4021501492038283011;8489255053443179153;-4661709328420890533;}
{rank = same; 543325479923207427;-3898669630605452554;244470699041366076;6208733498515523769;}
{rank = same; -6395493111282828260;5921214264002221941;1580961522298426183;-8187951950540390906;}
{rank = same; -8265530133940623444;8639444591122381034;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
......
Alternate.toolbox/Model_1/MutualExclusionSpec.tla
View file @ 7d001ca6
......@@ -3,20 +3,27 @@
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* States besides non-critical are represented as "non-cs".
\* 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", "cs"}]
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) ==
/\ \A i \in Procs: pc[i] /= "cs"
/\ 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.
......@@ -24,12 +31,13 @@ ExitCS(proc) ==
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
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)))
......@@ -40,7 +48,7 @@ MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "c
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
Liveness == \A i \in Procs:
/\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
/\ (pc[i] = "csentry") ~> (pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
......@@ -51,5 +59,5 @@ THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:11:11 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
Alternate.toolbox/Model_1_SnapShot_1644418425669/MC.cfg deleted 100644 → 0
View file @ 253af10d
\* CONSTANT definitions
CONSTANT
Procs <- const_1644418423653463000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644418423653464000
\* PROPERTY definition
PROPERTY
prop_1644418423653465000
prop_1644418423653466000
\* Generated on Wed Feb 09 17:53:43 MSK 2022
\ No newline at end of file
Alternate.toolbox/Model_1_SnapShot_1644418425669/Model_1_SnapShot_1644418425669.dot deleted 100644 → 0
View file @ 253af10d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
1402084145941851076 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
264913071721429937 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
264913071721429937 -> 1441589058236749349 [label="",color="2",fontcolor="2"];
1441589058236749349 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
1402084145941851076 -> 349469391966471760 [label="",color="2",fontcolor="2"];
349469391966471760 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
264913071721429937 -> -6190723150750739455 [label="",color="2",fontcolor="2"];
-6190723150750739455 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
1402084145941851076 -> -4985978420825095052 [label="",color="2",fontcolor="2"];
-4985978420825095052 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
264913071721429937 -> 264913071721429937 [style="dashed"];
1402084145941851076 -> 1402084145941851076 [style="dashed"];
1441589058236749349 -> -4025760291280799090 [label="",color="2",fontcolor="2"];
-4025760291280799090 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
349469391966471760 -> -5049627876531235088 [label="",color="3",fontcolor="3"];
-5049627876531235088 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
1441589058236749349 -> 1441589058236749349 [style="dashed"];
349469391966471760 -> -2812008362376975621 [label="",color="2",fontcolor="2"];
-2812008362376975621 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
349469391966471760 -> 349469391966471760 [style="dashed"];
-6190723150750739455 -> -4025760291280799090 [label="",color="2",fontcolor="2"];
-6190723150750739455 -> -493897691022108030 [label="",color="3",fontcolor="3"];
-493897691022108030 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
-6190723150750739455 -> -6190723150750739455 [style="dashed"];
-4985978420825095052 -> -2812008362376975621 [label="",color="2",fontcolor="2"];
-4985978420825095052 -> -4985978420825095052 [style="dashed"];
-4025760291280799090 -> 1306702513220175931 [label="",color="3",fontcolor="3"];
1306702513220175931 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
-5049627876531235088 -> -1782044937556263316 [label="",color="4",fontcolor="4"];
-1782044937556263316 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-4025760291280799090 -> -4025760291280799090 [style="dashed"];
-5049627876531235088 -> 562133816054668434 [label="",color="2",fontcolor="2"];
562133816054668434 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-5049627876531235088 -> -5049627876531235088 [style="dashed"];
-2812008362376975621 -> 562133816054668434 [label="",color="3",fontcolor="3"];
-2812008362376975621 -> -2812008362376975621 [style="dashed"];
-493897691022108030 -> 1306702513220175931 [label="",color="2",fontcolor="2"];
-493897691022108030 -> -1933917819784720848 [label="",color="4",fontcolor="4"];
-1933917819784720848 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
-493897691022108030 -> -493897691022108030 [style="dashed"];
1306702513220175931 -> 7779513292595707742 [label="",color="4",fontcolor="4"];
7779513292595707742 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
1306702513220175931 -> 1306702513220175931 [style="dashed"];
-1782044937556263316 -> 264913071721429937 [label="",color="5",fontcolor="5"];
-1782044937556263316 -> 7488564517445007501 [label="",color="2",fontcolor="2"];
7488564517445007501 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
562133816054668434 -> 7488564517445007501 [label="",color="4",fontcolor="4"];
-1782044937556263316 -> -1782044937556263316 [style="dashed"];
562133816054668434 -> 562133816054668434 [style="dashed"];
-1933917819784720848 -> 7779513292595707742 [label="",color="2",fontcolor="2"];
-1933917819784720848 -> 1402084145941851076 [label="",color="5",fontcolor="5"];
-1933917819784720848 -> -1933917819784720848 [style="dashed"];
7779513292595707742 -> 349469391966471760 [label="",color="5",fontcolor="5"];
7779513292595707742 -> 7779513292595707742 [style="dashed"];
7488564517445007501 -> -6190723150750739455 [label="",color="5",fontcolor="5"];
7488564517445007501 -> 7488564517445007501 [style="dashed"];
{rank = same; 264913071721429937;1402084145941851076;}
{rank = same; 1441589058236749349;-4985978420825095052;-6190723150750739455;349469391966471760;}
{rank = same; -493897691022108030;-4025760291280799090;-5049627876531235088;-2812008362376975621;}
{rank = same; 1306702513220175931;-1782044937556263316;562133816054668434;-1933917819784720848;}
{rank = same; 7488564517445007501;7779513292595707742;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
cs [label="cs",fillcolor=4]
exit [label="exit",fillcolor=5]
enter [label="enter",fillcolor=3]
ncs [label="ncs",fillcolor=2]
}}
\ No newline at end of file
Alternate.toolbox/Model_1_SnapShot_1644418436130/MC.out deleted 100644 → 0
View file @ 253af10d
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 55 and seed 7390341523143387179 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71572] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module MutualExclusionSpec
Semantic processing of module Alternate
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 17:53:54)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 5 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2108:1 @!@!@
Property Init is violated by the initial state:
/\ pc = (0 :> "ncs" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2108 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1232ms at (2022-02-09 17:53:55)
@!@!@ENDMSG 2186 @!@!@
Alternate.toolbox/Model_1_SnapShot_1644418436130/MC_TE.out deleted 100644 → 0
View file @ 253af10d
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 55 and seed 7390341523143387179 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 71572] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module MutualExclusionSpec
Semantic processing of module Alternate
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 17:53:54)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 5 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2108:1 @!@!@
Property Init is violated by the initial state:
/\ pc = (0 :> "ncs" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2108 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1232ms at (2022-02-09 17:53:55)
@!@!@ENDMSG 2186 @!@!@
Alternate.toolbox/Model_1_SnapShot_1644418436130/Model_1_SnapShot_1644418436130.dot deleted 100644 → 0
View file @ 253af10d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
Alternate.toolbox/Model_1_SnapShot_1644418436130/Model_1_liveness.dot deleted 100644 → 0
View file @ 253af10d
digraph DiskGraph {
nodesep=0.35;
subgraph cluster_graph {
color="white";
Alternate.toolbox/Model_1_SnapShot_1644418425669/Alternate.tla → Alternate.toolbox/Model_1_SnapShot_1644425787608/Alternate.tla
View file @ 7d001ca6
......@@ -74,12 +74,6 @@ Spec == /\ Init /\ [][Next]_vars
(*
PC2ME(xpc) == [proc \in Procs |-> IF xpc[proc] = "cs" THEN "cs"
ELSE "non-cs"]
ME == INSTANCE MutualExclusionSpec WITH pc <- PC2ME(pc)
*)
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> IF pc[proc] = "cs" THEN "cs"
ELSE "non-cs"]
......@@ -91,5 +85,5 @@ THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 17:53:40 MSK 2022 by kirr
\* Last modified Wed Feb 09 18:03:45 MSK 2022 by kirr
\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644410890486/MC.cfg → Alternate.toolbox/Model_1_SnapShot_1644425787608/MC.cfg
View file @ 7d001ca6
\* CONSTANT definitions
CONSTANT
Procs <- const_1644410888466290000
Procs <- const_1644425785595557000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
TypeOK
MutualExclusion
inv_1644425785595558000
inv_1644425785595559000
\* PROPERTY definition
PROPERTY
Liveness
\* Generated on Wed Feb 09 15:48:08 MSK 2022
\ No newline at end of file
prop_1644425785595560000
prop_1644425785595561000
\* Generated on Wed Feb 09 19:56:25 MSK 2022
\ No newline at end of file
Alternate.toolbox/Model_1_SnapShot_1644425787608/MC.out 0 → 100644
View file @ 7d001ca6
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 88 and seed -405408752417771537 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 76540] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module MutualExclusionSpec
Semantic processing of module Alternate
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 19:56:26)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 5 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 2 distinct states generated at 2022-02-09 19:56:26.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2112:1 @!@!@
Action property line 38, col 12 to line 38, col 24 of module MutualExclusionSpec is violated.
@!@!@ENDMSG 2112 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ pc = (0 :> "ncs" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <ncs line 44, col 14 to line 47, col 28 of module Alternate>
/\ pc = (0 :> "enter" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <enter line 49, col 16 to line 52, col 30 of module Alternate>
/\ pc = (0 :> "cs" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-09 19:56:26
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 40, col 1 to line 40, col 4 of module Alternate>: 4:4
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 41, col 12 to line 41, col 25 of module Alternate: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 42, col 12 to line 42, col 44 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 42, col 17 to line 42, col 44 of module Alternate: 4:8
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 42, col 27 to line 42, col 33 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 6:8
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 44, col 17 to line 44, col 32 of module Alternate: 21
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 44, col 17 to line 44, col 24 of module Alternate: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 45, col 17 to line 45, col 20 of module Alternate: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 46, col 17 to line 46, col 51 of module Alternate: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 47, col 17 to line 47, col 28 of module Alternate: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<enter line 49, col 1 to line 49, col 11 of module Alternate>: 2:3
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 49, col 19 to line 49, col 36 of module Alternate: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 49, col 19 to line 49, col 26 of module Alternate: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 50, col 19 to line 50, col 29 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 19 to line 50, col 22 of module Alternate: 5
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 26 to line 50, col 29 of module Alternate: 5
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 51, col 19 to line 51, col 50 of module Alternate: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 51, col 25 to line 51, col 50 of module Alternate: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 52, col 19 to line 52, col 30 of module Alternate: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 52, col 27 to line 52, col 30 of module Alternate: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<cs line 54, col 1 to line 54, col 8 of module Alternate>: 0:0
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 54, col 16 to line 54, col 30 of module Alternate: 9
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 56, col 16 to line 56, col 49 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 57, col 16 to line 57, col 27 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:0
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 59, col 18 to line 59, col 34 of module Alternate: 9
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 60, col 18 to line 60, col 46 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 61, col 18 to line 61, col 50 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644425785595558000 line 10, col 1 to line 10, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 11, col 1 to line 11, col 18 of module MC: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 78, col 23 to line 79, col 77 of module Alternate: 48:76
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 78, col 33 to line 78, col 37 of module Alternate: 48
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 77, col 1 to line 79, col 77 of module Alternate: 21
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644425785595559000 line 14, col 1 to line 14, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 15, col 1 to line 15, col 45 of module MC: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 18 to line 15, col 45 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 19 to line 15, col 30 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 37 to line 15, col 44 of module MC: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 10 to line 15, col 14 of module MC: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(3) at 2022-02-09 19:56:26: 11 states generated (517 s/min), 10 distinct states found (470 ds/min), 2 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
11 states generated, 10 distinct states found, 2 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 3.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1287ms at (2022-02-09 19:56:26)
@!@!@ENDMSG 2186 @!@!@
Alternate.toolbox/Model_1_SnapShot_1644418425669/MC.tla → Alternate.toolbox/Model_1_SnapShot_1644425787608/MC.tla
View file @ 7d001ca6
......@@ -2,22 +2,26 @@
EXTENDS Alternate, TLC
\* CONSTANT definitions @modelParameterConstants:0Procs
const_1644418423653463000 ==
const_1644425785595557000 ==
0..1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644418423653464000 ==
inv_1644425785595558000 ==
ME!MutualExclusion
----
\* INVARIANT definition @modelCorrectnessInvariants:1
inv_1644425785595559000 ==
\A i \in Procs : (pc[i] = "cs") => (turn = i)
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644418423653465000 ==
prop_1644425785595560000 ==
ME!Spec
----
\* PROPERTY definition @modelCorrectnessProperties:1
prop_1644418423653466000 ==
prop_1644425785595561000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 17:53:43 MSK 2022 by kirr
\* Created Wed Feb 09 19:56:25 MSK 2022 by kirr
Alternate.toolbox/Model_1_SnapShot_1644425787608/MC_TE.out 0 → 100644
View file @ 7d001ca6
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 88 and seed -405408752417771537 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 76540] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/Alternate.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Integers.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/Alternate.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module MutualExclusionSpec
Semantic processing of module Alternate
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 19:56:26)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 5 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 2 distinct states generated at 2022-02-09 19:56:26.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2112:1 @!@!@
Action property line 38, col 12 to line 38, col 24 of module MutualExclusionSpec is violated.
@!@!@ENDMSG 2112 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ pc = (0 :> "ncs" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <ncs line 44, col 14 to line 47, col 28 of module Alternate>
/\ pc = (0 :> "enter" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <enter line 49, col 16 to line 52, col 30 of module Alternate>
/\ pc = (0 :> "cs" @@ 1 :> "ncs")
/\ turn = 0
@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-09 19:56:26
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 40, col 1 to line 40, col 4 of module Alternate>: 4:4
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 41, col 12 to line 41, col 25 of module Alternate: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 42, col 12 to line 42, col 44 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 42, col 17 to line 42, col 44 of module Alternate: 4:8
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 42, col 27 to line 42, col 33 of module Alternate: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ncs line 44, col 1 to line 44, col 9 of module Alternate>: 6:8
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 44, col 17 to line 44, col 32 of module Alternate: 21
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 44, col 17 to line 44, col 24 of module Alternate: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 45, col 17 to line 45, col 20 of module Alternate: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 46, col 17 to line 46, col 51 of module Alternate: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 47, col 17 to line 47, col 28 of module Alternate: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<enter line 49, col 1 to line 49, col 11 of module Alternate>: 2:3
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 49, col 19 to line 49, col 36 of module Alternate: 13
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 49, col 19 to line 49, col 26 of module Alternate: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 50, col 19 to line 50, col 29 of module Alternate: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 19 to line 50, col 22 of module Alternate: 5
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 50, col 26 to line 50, col 29 of module Alternate: 5
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 51, col 19 to line 51, col 50 of module Alternate: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 51, col 25 to line 51, col 50 of module Alternate: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 52, col 19 to line 52, col 30 of module Alternate: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 52, col 27 to line 52, col 30 of module Alternate: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<cs line 54, col 1 to line 54, col 8 of module Alternate>: 0:0
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 54, col 16 to line 54, col 30 of module Alternate: 9
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 56, col 16 to line 56, col 49 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 57, col 16 to line 57, col 27 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<exit line 59, col 1 to line 59, col 10 of module Alternate>: 0:0
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 59, col 18 to line 59, col 34 of module Alternate: 9
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 60, col 18 to line 60, col 46 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 61, col 18 to line 61, col 50 of module Alternate: 0
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644425785595558000 line 10, col 1 to line 10, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 11, col 1 to line 11, col 18 of module MC: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 78, col 23 to line 79, col 77 of module Alternate: 48:76
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 78, col 33 to line 78, col 37 of module Alternate: 48
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 77, col 1 to line 79, col 77 of module Alternate: 21
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 40
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<inv_1644425785595559000 line 14, col 1 to line 14, col 23 of module MC>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 15, col 1 to line 15, col 45 of module MC: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 18 to line 15, col 45 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 19 to line 15, col 30 of module MC: 20
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 37 to line 15, col 44 of module MC: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 15, col 10 to line 15, col 14 of module MC: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(3) at 2022-02-09 19:56:26: 11 states generated (517 s/min), 10 distinct states found (470 ds/min), 2 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
11 states generated, 10 distinct states found, 2 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 3.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1287ms at (2022-02-09 19:56:26)
@!@!@ENDMSG 2186 @!@!@
Alternate.toolbox/Model_1_SnapShot_1644425787608/Model_1_SnapShot_1644425787608.dot 0 → 100644
View file @ 7d001ca6
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
-4385412785220897332 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
-7792006210643843233 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
-4385412785220897332 -> -2121727716720394216 [label="",color="2",fontcolor="2"];
-2121727716720394216 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-4385412785220897332 -> -3757412970352516297 [label="",color="2",fontcolor="2"];
-3757412970352516297 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-7792006210643843233 -> -5588753771789561205 [label="",color="2",fontcolor="2"];
-5588753771789561205 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
-4385412785220897332 -> -4385412785220897332 [style="dashed"];
-7792006210643843233 -> -7267643063291514460 [label="",color="2",fontcolor="2"];
-7267643063291514460 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
-7792006210643843233 -> -7792006210643843233 [style="dashed"];
-2121727716720394216 -> 8435757444235712431 [label="",color="3",fontcolor="3"];
8435757444235712431 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-3757412970352516297 -> 4039947853683791371 [label="",color="2",fontcolor="2"];
4039947853683791371 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-3757412970352516297 -> -3757412970352516297 [style="dashed"];
-5588753771789561205 -> 7561014664456340632 [label="",color="2",fontcolor="2"];
7561014664456340632 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
-5588753771789561205 -> -5588753771789561205 [style="dashed"];
-7267643063291514460 -> 7561014664456340632 [label="",color="2",fontcolor="2"];
-7267643063291514460 -> 9009807488935807510 [label="",color="3",fontcolor="3"];
9009807488935807510 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
-2121727716720394216 -> -2121727716720394216 [style="dashed"];
-7267643063291514460 -> -7267643063291514460 [style="dashed"];
{rank = same; -4385412785220897332;-7792006210643843233;}
{rank = same; -2121727716720394216;-3757412970352516297;-5588753771789561205;-7267643063291514460;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
enter [label="enter",fillcolor=3]
ncs [label="ncs",fillcolor=2]
}}
\ No newline at end of file
Alternate.toolbox/Model_1_SnapShot_1644425787608/Model_1_liveness.dot 0 → 100644
View file @ 7d001ca6
digraph DiskGraph {
nodesep=0.35;
subgraph cluster_graph {
color="white";
"-4385412785220897332.1" [style = filled] [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0
#-4385412785220897332.1#"]
"-7792006210643843233.1" [style = filled] [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1
#-7792006210643843233.1#"]
"-7792006210643843233.1" -> "-7267643063291514460.1" [label="[t]"];
"-7267643063291514460.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1
#-7267643063291514460.1#"];
"-7792006210643843233.1" -> "-5588753771789561205.1" [label="[t]"];
"-5588753771789561205.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1
#-5588753771789561205.1#"];
"-7792006210643843233.1" -> "-7792006210643843233.1" [label="[f]"];
"-7792006210643843233.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1
#-7792006210643843233.1#"];
"-4385412785220897332.1" -> "-3757412970352516297.1" [label="[t]"];
"-3757412970352516297.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0
#-3757412970352516297.1#"];
"-4385412785220897332.1" -> "-2121727716720394216.1" [label="[t]"];
"-2121727716720394216.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0
#-2121727716720394216.1#"];
"-4385412785220897332.1" -> "-4385412785220897332.1" [label="[f]"];
"-4385412785220897332.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0
#-4385412785220897332.1#"];
"-3757412970352516297.1" -> "-3757412970352516297.1" [label="[f]"];
"-3757412970352516297.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0
#-3757412970352516297.1#"];
"-3757412970352516297.1" -> "4039947853683791371.1" [label="[t]"];
"4039947853683791371.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0
#4039947853683791371.1#"];
"-5588753771789561205.1" -> "7561014664456340632.1" [label="[t]"];
"7561014664456340632.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1
#7561014664456340632.1#"];
"-5588753771789561205.1" -> "-5588753771789561205.1" [label="[f]"];
"-5588753771789561205.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1
#-5588753771789561205.1#"];
"-2121727716720394216.1" -> "-2121727716720394216.1" [label="[f]"];
"-2121727716720394216.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0
#-2121727716720394216.1#"];
"-2121727716720394216.1" -> "8435757444235712431.1" [label="[t]"];
"8435757444235712431.1" [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0
#8435757444235712431.1#"];
"-7267643063291514460.1" -> "-7267643063291514460.1" [label="[f]"];
"-7267643063291514460.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1
#-7267643063291514460.1#"];
"-7267643063291514460.1" -> "9009807488935807510.0" [label="[t]"];
"9009807488935807510.0" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1
#9009807488935807510.0#"];
"-7267643063291514460.1" -> "9009807488935807510.1" [label="[t]"];
"9009807488935807510.1" [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1
#9009807488935807510.1#"];
"-7267643063291514460.1" -> "7561014664456340632.1" [label="[t]"];
"7561014664456340632.1" [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1
#7561014664456340632.1#"];
}
}
\ No newline at end of file
Alternate.toolbox/Model_1_SnapShot_1644418436130/MutualExclusionSpec.tla → Alternate.toolbox/Model_1_SnapShot_1644425787608/MutualExclusionSpec.tla
View file @ 7d001ca6
......@@ -3,20 +3,27 @@
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* States besides non-critical are represented as "non-cs".
\* 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", "cs"}]
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) ==
/\ \A i \in Procs: pc[i] /= "cs"
/\ 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.
......@@ -24,12 +31,13 @@ ExitCS(proc) ==
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
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)))
......@@ -40,7 +48,7 @@ MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "c
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
Liveness == \A i \in Procs:
/\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
/\ (pc[i] = "csentry") ~> (pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
......@@ -51,5 +59,5 @@ THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:11:11 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
Alternate.toolbox/Model_1_SnapShot_1644418436130/Alternate.tla → Alternate.toolbox/Model_1_SnapShot_1644425917721/Alternate.tla
View file @ 7d001ca6
......@@ -74,16 +74,10 @@ Spec == /\ Init /\ [][Next]_vars
(*
PC2ME(xpc) == [proc \in Procs |-> IF xpc[proc] = "cs" THEN "cs"
ELSE "non-cs"]
ME == INSTANCE MutualExclusionSpec WITH pc <- PC2ME(pc)
*)
ME == INSTANCE MutualExclusionSpec WITH
pc <- [proc \in Procs |-> IF pc[proc] = "cs" THEN "cs"
ELSE "Znon-cs"]
pc <- [proc \in Procs |-> CASE pc[proc] = "cs" -> "cs"
[] pc[proc] = "enter" -> "csentry"
[] OTHER -> "non-cs"]
THEOREM Spec => ME!Spec
THEOREM Spec => []ME!MutualExclusion
......@@ -91,5 +85,5 @@ THEOREM Spec => ME!Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 17:53:52 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:58:34 MSK 2022 by kirr
\* Created Wed Feb 09 16:13:49 MSK 2022 by kirr
Alternate.toolbox/Model_1_SnapShot_1644418436130/MC.cfg → Alternate.toolbox/Model_1_SnapShot_1644425917721/MC.cfg
View file @ 7d001ca6
\* CONSTANT definitions
CONSTANT
Procs <- const_1644418434112467000
Procs <- const_1644425915701562000
\* SPECIFICATION definition
SPECIFICATION
Spec
\* INVARIANT definition
INVARIANT
inv_1644418434112468000
inv_1644425915701563000
inv_1644425915701564000
\* PROPERTY definition
PROPERTY
prop_1644418434112469000
prop_1644418434112470000
\* Generated on Wed Feb 09 17:53:54 MSK 2022
\ No newline at end of file
prop_1644425915701565000
prop_1644425915701566000
\* Generated on Wed Feb 09 19:58:35 MSK 2022
\ No newline at end of file
Alternate.toolbox/Model_1_SnapShot_1644418436130/MC.tla → Alternate.toolbox/Model_1_SnapShot_1644425917721/MC.tla
View file @ 7d001ca6
......@@ -2,22 +2,26 @@
EXTENDS Alternate, TLC
\* CONSTANT definitions @modelParameterConstants:0Procs
const_1644418434112467000 ==
const_1644425915701562000 ==
0..1
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1644418434112468000 ==
inv_1644425915701563000 ==
ME!MutualExclusion
----
\* INVARIANT definition @modelCorrectnessInvariants:1
inv_1644425915701564000 ==
\A i \in Procs : (pc[i] = "cs") => (turn = i)
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_1644418434112469000 ==
prop_1644425915701565000 ==
ME!Spec
----
\* PROPERTY definition @modelCorrectnessProperties:1
prop_1644418434112470000 ==
prop_1644425915701566000 ==
ME!Liveness
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 17:53:54 MSK 2022 by kirr
\* Created Wed Feb 09 19:58:35 MSK 2022 by kirr
Alternate.toolbox/Model_1_SnapShot_1644425917721/Model_1_SnapShot_1644425917721.dot 0 → 100644
View file @ 7d001ca6
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
-2304256186017901240 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 0",style = filled]
3063590532813598594 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"ncs\")\n/\\ turn = 1",style = filled]
-2304256186017901240 -> 4021501492038283011 [label="",color="2",fontcolor="2"];
4021501492038283011 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
-2304256186017901240 -> -4661709328420890533 [label="",color="2",fontcolor="2"];
-4661709328420890533 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-2304256186017901240 -> -2304256186017901240 [style="dashed"];
3063590532813598594 -> -194057057360964151 [label="",color="2",fontcolor="2"];
-194057057360964151 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"ncs\")\n/\\ turn = 1"];
3063590532813598594 -> 8489255053443179153 [label="",color="2",fontcolor="2"];
8489255053443179153 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
3063590532813598594 -> 3063590532813598594 [style="dashed"];
4021501492038283011 -> 543325479923207427 [label="",color="3",fontcolor="3"];
543325479923207427 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
4021501492038283011 -> 244470699041366076 [label="",color="2",fontcolor="2"];
244470699041366076 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
4021501492038283011 -> 4021501492038283011 [style="dashed"];
-4661709328420890533 -> 244470699041366076 [label="",color="2",fontcolor="2"];
-4661709328420890533 -> -4661709328420890533 [style="dashed"];
-194057057360964151 -> -3898669630605452554 [label="",color="2",fontcolor="2"];
-3898669630605452554 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"enter\")\n/\\ turn = 1"];
8489255053443179153 -> -3898669630605452554 [label="",color="2",fontcolor="2"];
-194057057360964151 -> -194057057360964151 [style="dashed"];
8489255053443179153 -> 6208733498515523769 [label="",color="3",fontcolor="3"];
6208733498515523769 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
8489255053443179153 -> 8489255053443179153 [style="dashed"];
543325479923207427 -> -6395493111282828260 [label="",color="4",fontcolor="4"];
-6395493111282828260 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"ncs\")\n/\\ turn = 0"];
543325479923207427 -> 1580961522298426183 [label="",color="2",fontcolor="2"];
1580961522298426183 [label="/\\ pc = (0 :> \"cs\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
543325479923207427 -> 543325479923207427 [style="dashed"];
244470699041366076 -> 1580961522298426183 [label="",color="3",fontcolor="3"];
244470699041366076 -> 244470699041366076 [style="dashed"];
-3898669630605452554 -> 5921214264002221941 [label="",color="3",fontcolor="3"];
5921214264002221941 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"cs\")\n/\\ turn = 1"];
-3898669630605452554 -> -3898669630605452554 [style="dashed"];
6208733498515523769 -> 5921214264002221941 [label="",color="2",fontcolor="2"];
6208733498515523769 -> -8187951950540390906 [label="",color="4",fontcolor="4"];
-8187951950540390906 [label="/\\ pc = (0 :> \"ncs\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
6208733498515523769 -> 6208733498515523769 [style="dashed"];
-6395493111282828260 -> 3063590532813598594 [label="",color="5",fontcolor="5"];
-6395493111282828260 -> 8639444591122381034 [label="",color="2",fontcolor="2"];
8639444591122381034 [label="/\\ pc = (0 :> \"exit\" @@ 1 :> \"enter\")\n/\\ turn = 0"];
-6395493111282828260 -> -6395493111282828260 [style="dashed"];
1580961522298426183 -> 8639444591122381034 [label="",color="4",fontcolor="4"];
5921214264002221941 -> -8265530133940623444 [label="",color="4",fontcolor="4"];
-8265530133940623444 [label="/\\ pc = (0 :> \"enter\" @@ 1 :> \"exit\")\n/\\ turn = 1"];
1580961522298426183 -> 1580961522298426183 [style="dashed"];
5921214264002221941 -> 5921214264002221941 [style="dashed"];
-8187951950540390906 -> -8265530133940623444 [label="",color="2",fontcolor="2"];
-8187951950540390906 -> -2304256186017901240 [label="",color="5",fontcolor="5"];
8639444591122381034 -> 8489255053443179153 [label="",color="5",fontcolor="5"];
-8187951950540390906 -> -8187951950540390906 [style="dashed"];
8639444591122381034 -> 8639444591122381034 [style="dashed"];
-8265530133940623444 -> 4021501492038283011 [label="",color="5",fontcolor="5"];
-8265530133940623444 -> -8265530133940623444 [style="dashed"];
{rank = same; -2304256186017901240;3063590532813598594;}
{rank = same; -194057057360964151;4021501492038283011;8489255053443179153;-4661709328420890533;}
{rank = same; 543325479923207427;-3898669630605452554;244470699041366076;6208733498515523769;}
{rank = same; -6395493111282828260;5921214264002221941;1580961522298426183;-8187951950540390906;}
{rank = same; -8265530133940623444;8639444591122381034;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
cs [label="cs",fillcolor=4]
exit [label="exit",fillcolor=5]
enter [label="enter",fillcolor=3]
ncs [label="ncs",fillcolor=2]
}}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644410890486/MutualExclusionSpec.tla → Alternate.toolbox/Model_1_SnapShot_1644425917721/MutualExclusionSpec.tla
View file @ 7d001ca6
------------------------ MODULE MutualExclusionSpec ------------------------
\* Module MutualExclusionSpec provides specification for mutual-exclusion problem
\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* States besides non-critical are represented as "non-cs".
\* 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", "cs"}]
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) ==
/\ \A i \in Procs: pc[i] /= "cs"
/\ 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" \* XXX also check others are not in cs here?
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
Next == \E i \in Procs: WantCS(i) \/ EnterCS(i) \/ ExitCS(i)
Spec == /\ Init
/\ [][Next]_vars
/\ \A i \in Procs: (
/\ \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] = "non-cs") ~> <>(pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs") \* XXX pc -> pc'
\* Liveness == (pc[0] = "cs") => <>(pc[0] = "ZZZZ")
\* Liveness == (pc[0] = "cs") => <>(pc[0] = "ZZZZ")
\*Liveness == (pc[0] = "cs") ~> <>(pc[0] = "non-cs")
/\ (pc[i] = "csentry") ~> (pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
THEOREM Spec => []TypeOK
......@@ -56,5 +59,5 @@ THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 15:48:07 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:11:11 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
MutualExclusionSpec.pdf
View file @ 7d001ca6
No preview for this file type
MutualExclusionSpec.tla
View file @ 7d001ca6
......@@ -3,20 +3,27 @@
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* States besides non-critical are represented as "non-cs".
\* 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", "cs"}]
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) ==
/\ \A i \in Procs: pc[i] /= "cs"
/\ 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.
......@@ -24,12 +31,13 @@ ExitCS(proc) ==
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
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)))
......@@ -40,7 +48,7 @@ MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "c
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
Liveness == \A i \in Procs:
/\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
/\ (pc[i] = "csentry") ~> (pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
......@@ -51,5 +59,5 @@ THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:11:11 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1/MC.cfg
View file @ 7d001ca6
......@@ -2,11 +2,10 @@
CONSTANTS
p1 = p1
p2 = p2
p3 = p3
\* MV CONSTANT definitions
CONSTANT
Procs <- const_1644419360528487000
Procs <- const_1644425758311553000
\* SPECIFICATION definition
SPECIFICATION
Spec
......@@ -17,4 +16,4 @@ MutualExclusion
\* PROPERTY definition
PROPERTY
Liveness
\* Generated on Wed Feb 09 18:09:20 MSK 2022
\ No newline at end of file
\* Generated on Wed Feb 09 19:55:58 MSK 2022
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1/MC.out
View file @ 7d001ca6
This diff is collapsed.
MutualExclusionSpec.toolbox/Model_1/MC.tla
View file @ 7d001ca6
......@@ -3,14 +3,14 @@ EXTENDS MutualExclusionSpec, TLC
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
p1, p2, p3
p1, p2
----
\* MV CONSTANT definitions Procs
const_1644419360528487000 ==
{p1, p2, p3}
const_1644425758311553000 ==
{p1, p2}
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 18:09:20 MSK 2022 by kirr
\* Created Wed Feb 09 19:55:58 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1/Model_1.dot
View file @ 7d001ca6
......@@ -3,25 +3,44 @@ edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
4634416839099240645 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\" @@ p3 :> \"non-cs\")",style = filled]
4634416839099240645 -> 5434594326082262714 [label="",color="2",fontcolor="2"];
5434594326082262714 [label="pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\" @@ p3 :> \"non-cs\")"];
5434594326082262714 -> 4634416839099240645 [label="",color="3",fontcolor="3"];
4634416839099240645 -> -8039079448462160139 [label="",color="2",fontcolor="2"];
-8039079448462160139 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\" @@ p3 :> \"non-cs\")"];
5434594326082262714 -> 5434594326082262714 [style="dashed"];
4634416839099240645 -> -1387407517741503287 [label="",color="2",fontcolor="2"];
-1387407517741503287 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\" @@ p3 :> \"cs\")"];
4634416839099240645 -> 4634416839099240645 [style="dashed"];
-8039079448462160139 -> 4634416839099240645 [label="",color="3",fontcolor="3"];
-8039079448462160139 -> -8039079448462160139 [style="dashed"];
-1387407517741503287 -> 4634416839099240645 [label="",color="3",fontcolor="3"];
-1387407517741503287 -> -1387407517741503287 [style="dashed"];
{rank = same; 4634416839099240645;}
{rank = same; 5434594326082262714;-8039079448462160139;-1387407517741503287;}
-7824571988019409220 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")",style = filled]
-7824571988019409220 -> 5080291979216001926 [label="",color="2",fontcolor="2"];
5080291979216001926 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")"];
-7824571988019409220 -> -8272984896072399991 [label="",color="2",fontcolor="2"];
-8272984896072399991 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")"];
5080291979216001926 -> 897139957786517708 [label="",color="3",fontcolor="3"];
897139957786517708 [label="pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\")"];
-7824571988019409220 -> -7824571988019409220 [style="dashed"];
5080291979216001926 -> 4489738507008100367 [label="",color="2",fontcolor="2"];
4489738507008100367 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")"];
5080291979216001926 -> 5080291979216001926 [style="dashed"];
-8272984896072399991 -> 4489738507008100367 [label="",color="2",fontcolor="2"];
-8272984896072399991 -> -9137926712894874236 [label="",color="3",fontcolor="3"];
-9137926712894874236 [label="pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")"];
-8272984896072399991 -> -8272984896072399991 [style="dashed"];
897139957786517708 -> -7824571988019409220 [label="",color="4",fontcolor="4"];
897139957786517708 -> -1529149678030047826 [label="",color="2",fontcolor="2"];
-1529149678030047826 [label="pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")"];
897139957786517708 -> 897139957786517708 [style="dashed"];
4489738507008100367 -> -1529149678030047826 [label="",color="3",fontcolor="3"];
4489738507008100367 -> 1143334986297935796 [label="",color="3",fontcolor="3"];
1143334986297935796 [label="pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")"];
4489738507008100367 -> 4489738507008100367 [style="dashed"];
-9137926712894874236 -> 1143334986297935796 [label="",color="2",fontcolor="2"];
-9137926712894874236 -> -7824571988019409220 [label="",color="4",fontcolor="4"];
-9137926712894874236 -> -9137926712894874236 [style="dashed"];
-1529149678030047826 -> -8272984896072399991 [label="",color="4",fontcolor="4"];
-1529149678030047826 -> -1529149678030047826 [style="dashed"];
1143334986297935796 -> 5080291979216001926 [label="",color="4",fontcolor="4"];
1143334986297935796 -> 1143334986297935796 [style="dashed"];
{rank = same; -7824571988019409220;}
{rank = same; -8272984896072399991;5080291979216001926;}
{rank = same; -9137926712894874236;897139957786517708;4489738507008100367;}
{rank = same; 1143334986297935796;-1529149678030047826;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
ExitCS [label="ExitCS",fillcolor=3]
EnterCS [label="EnterCS",fillcolor=2]
WantCS [label="WantCS",fillcolor=2]
ExitCS [label="ExitCS",fillcolor=4]
EnterCS [label="EnterCS",fillcolor=3]
}}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
View file @ 7d001ca6
......@@ -3,20 +3,27 @@
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* States besides non-critical are represented as "non-cs".
\* 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", "cs"}]
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) ==
/\ \A i \in Procs: pc[i] /= "cs"
/\ 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.
......@@ -24,12 +31,13 @@ ExitCS(proc) ==
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
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)))
......@@ -40,7 +48,7 @@ MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "c
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
Liveness == \A i \in Procs:
/\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
/\ (pc[i] = "csentry") ~> (pc[i] = "cs")
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
......@@ -51,5 +59,5 @@ THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 17:36:37 MSK 2022 by kirr
\* Last modified Wed Feb 09 19:11:11 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644410890486/Model_1_SnapShot_1644410890486.dot deleted 100644 → 0
View file @ 253af10d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
678051584500975225 [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")",style = filled]
678051584500975225 -> 723320521238198925 [label="",color="2",fontcolor="2"];
723320521238198925 [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")"];
678051584500975225 -> 896249248177462194 [label="",color="2",fontcolor="2"];
896249248177462194 [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")"];
678051584500975225 -> 678051584500975225 [style="dashed"];
723320521238198925 -> 678051584500975225 [label="",color="3",fontcolor="3"];
723320521238198925 -> 723320521238198925 [style="dashed"];
896249248177462194 -> 678051584500975225 [label="",color="3",fontcolor="3"];
896249248177462194 -> 896249248177462194 [style="dashed"];
{rank = same; 678051584500975225;}
{rank = same; 896249248177462194;723320521238198925;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
ExitCS [label="ExitCS",fillcolor=3]
EnterCS [label="EnterCS",fillcolor=2]
}}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644410890486/Model_1_liveness.dot deleted 100644 → 0
View file @ 253af10d
digraph DiskGraph {
nodesep=0.35;
subgraph cluster_graph {
color="white";
"678051584500975225.1" [style = filled] [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.1#"]
"678051584500975225.1" -> "896249248177462194.0" [label="[fftftftf]"];
"896249248177462194.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.0#"];
"678051584500975225.1" -> "896249248177462194.1" [label="[fftftftf]"];
"896249248177462194.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.1#"];
"678051584500975225.1" -> "678051584500975225.1" [label="[fffftftf]"];
"678051584500975225.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.1#"];
"678051584500975225.1" -> "723320521238198925.1" [label="[tffftftf]"];
"723320521238198925.1" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#723320521238198925.1#"];
"723320521238198925.1" -> "678051584500975225.1" [style="dotted"] [label="[ftffttft]"];
"896249248177462194.0" -> "896249248177462194.2" [label="[fffffttt]"];
"896249248177462194.2" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.2#"];
"896249248177462194.1" -> "896249248177462194.0" [label="[fffffttt]"];
"896249248177462194.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.0#"];
"896249248177462194.1" -> "896249248177462194.1" [label="[fffffttt]"];
"896249248177462194.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.1#"];
"896249248177462194.1" -> "678051584500975225.1" [label="[ffftfttt]"];
"678051584500975225.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.1#"];
}
}98925.1" [label="[tffftftf]"];
"723320521238198925.1" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#723320521238198925.1#"];
"723320521238198925.1" -> "678051584500975225.0" [style="dotted"] [label="[ftffttft]"];
"723320521238198925.1" -> "678051584500975225.1" [style="dotted"] [label="[ftffttft]"];
"896249248177462194.1" -> "896249248177462194.1" [label="[fffffttt]"];
"896249248177462194.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.1#"];
"896249248177462194.1" -> "678051584500975225.0" [label="[ffftfttt]"];
"678051584500975225.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.0#"];
"896249248177462194.1" -> "678051584500975225.1" [label="[ffftfttt]"];
"678051584500975225.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.1#"];
}
}.0" -> "896249248177462194.2" [label="[fffffttt]"];
"896249248177462194.2" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.2#"];
"896249248177462194.0" -> "678051584500975225.2" [label="[ffftfttt]"];
"678051584500975225.2" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.2#"];
"896249248177462194.1" -> "896249248177462194.0" [label="[fffffttt]"];
"896249248177462194.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.0#"];
"896249248177462194.1" -> "896249248177462194.1" [label="[fffffttt]"];
"896249248177462194.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#896249248177462194.1#"];
"896249248177462194.1" -> "678051584500975225.0" [label="[ffftfttt]"];
"678051584500975225.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.0#"];
"896249248177462194.1" -> "678051584500975225.1" [label="[ffftfttt]"];
"678051584500975225.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#678051584500975225.1#"];
}
}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644410902348/Model_1_SnapShot_1644410902348.dot deleted 100644 → 0
View file @ 253af10d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
2926185554924883776 [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")",style = filled]
2926185554924883776 -> -9028380718502956592 [label="",color="2",fontcolor="2"];
-9028380718502956592 [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")"];
2926185554924883776 -> -239195827483615975 [label="",color="2",fontcolor="2"];
-239195827483615975 [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")"];
-9028380718502956592 -> 2926185554924883776 [label="",color="3",fontcolor="3"];
2926185554924883776 -> 2926185554924883776 [style="dashed"];
-9028380718502956592 -> -9028380718502956592 [style="dashed"];
-239195827483615975 -> 2926185554924883776 [label="",color="3",fontcolor="3"];
-239195827483615975 -> -239195827483615975 [style="dashed"];
{rank = same; 2926185554924883776;}
{rank = same; -9028380718502956592;-239195827483615975;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
ExitCS [label="ExitCS",fillcolor=3]
EnterCS [label="EnterCS",fillcolor=2]
}}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644410902348/Model_1_liveness.dot deleted 100644 → 0
View file @ 253af10d
digraph DiskGraph {
nodesep=0.35;
subgraph cluster_graph {
color="white";
"2926185554924883776.1" [style = filled] [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#2926185554924883776.1#"]
"2926185554924883776.1" -> "-9028380718502956592.1" [label="[tffftftf]"];
"-9028380718502956592.1" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#-9028380718502956592.1#"];
"-9028380718502956592.1" -> "2926185554924883776.1" [style="dotted"] [label="[ftffttft]"];
"2926185554924883776.1" -> "2926185554924883776.1" [label="[fffftftf]"];
"2926185554924883776.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#2926185554924883776.1#"];
"2926185554924883776.1" -> "-239195827483615975.0" [label="[fftftftf]"];
"-239195827483615975.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#-239195827483615975.0#"];
"2926185554924883776.1" -> "-239195827483615975.1" [label="[fftftftf]"];
"-239195827483615975.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#-239195827483615975.1#"];
"-239195827483615975.1" -> "2926185554924883776.1" [style="dotted"] [label="[ffftfttt]"];
}
}[style="dotted"] [label="[ftffttft]"];
"2926185554924883776.1" -> "-9028380718502956592.1" [label="[tffftftf]"];
"-9028380718502956592.1" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#-9028380718502956592.1#"];
"-9028380718502956592.1" -> "2926185554924883776.0" [style="dotted"] [label="[ftffttft]"];
"-9028380718502956592.1" -> "2926185554924883776.1" [style="dotted"] [label="[ftffttft]"];
"2926185554924883776.1" -> "2926185554924883776.0" [label="[fffftftf]"];
"2926185554924883776.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#2926185554924883776.0#"];
"2926185554924883776.1" -> "2926185554924883776.1" [label="[fffftftf]"];
"2926185554924883776.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#2926185554924883776.1#"];
"2926185554924883776.1" -> "-239195827483615975.1" [label="[fftftftf]"];
"-239195827483615975.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#-239195827483615975.1#"];
"-239195827483615975.1" -> "2926185554924883776.0" [style="dotted"] [label="[ffftfttt]"];
"-239195827483615975.1" -> "2926185554924883776.1" [style="dotted"] [label="[ffftfttt]"];
}
}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411040591/MC.out deleted 100644 → 0
View file @ 253af10d
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 58 and seed -6328379916666862350 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 64864] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module MutualExclusionSpec
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 15:50:40)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2214:1 @!@!@
Temporal formulas containing actions must be of forms <>[]A or []<>A.
@!@!@ENDMSG 2214 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 433ms at (2022-02-09 15:50:40)
@!@!@ENDMSG 2186 @!@!@
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411040591/MC.tla deleted 100644 → 0
View file @ 253af10d
---- MODULE MC ----
EXTENDS MutualExclusionSpec, TLC
\* CONSTANT definitions @modelParameterConstants:0Procs
const_1644411039581298000 ==
{0, 1}
----
=============================================================================
\* Modification History
\* Created Wed Feb 09 15:50:39 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411040591/MC_TE.out deleted 100644 → 0
View file @ 253af10d
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 58 and seed -6328379916666862350 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 64864] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module MutualExclusionSpec
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 15:50:40)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2214:1 @!@!@
Temporal formulas containing actions must be of forms <>[]A or []<>A.
@!@!@ENDMSG 2214 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 433ms at (2022-02-09 15:50:40)
@!@!@ENDMSG 2186 @!@!@
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411040591/Model_1_SnapShot_1644411040591.dot deleted 100644 → 0
View file @ 253af10d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411040591/MutualExclusionSpec.tla deleted 100644 → 0
View file @ 253af10d
------------------------ MODULE MutualExclusionSpec ------------------------
\* Module MutualExclusionSpec provides specification for mutual-exclusion problem
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* States besides non-critical are represented as "non-cs".
CONSTANT Procs
VARIABLES pc
TypeOK == pc \in [Procs -> {"non-cs", "cs"}]
vars == <<pc>>
\* All processes start from non-critical section.
Init == pc \in [Procs -> {"non-cs"}]
\* EnterCS(proc) is action when proc enters critical section.
EnterCS(proc) ==
/\ \A i \in Procs: pc[i] /= "cs"
/\ pc' = [pc EXCEPT ![proc] = "cs"]
\* ExitCS(proc) is action when proc leaves critical section.
ExitCS(proc) ==
/\ pc[proc] = "cs" \* XXX also check others are not in cs here?
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: EnterCS(i) \/ ExitCS(i)
Spec == /\ Init
/\ [][Next]_vars
/\ \A i \in Procs: (
/\ SF_vars(EnterCS(i))
/\ SF_vars(ExitCS(i)))
--------
\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
Liveness == \A i \in Procs:
/\ (pc[i] = "non-cs") ~> (pc[i] = "cs")
/\ [][(pc[i] = "cs") => (pc'[i] = "non-cs")]_vars \* XXX pc -> pc' "no eventually"
\* Liveness == (pc[0] = "cs") => <>(pc[0] = "ZZZZ")
\* Liveness == (pc[0] = "cs") => <>(pc[0] = "ZZZZ")
\*Liveness == (pc[0] = "cs") ~> <>(pc[0] = "non-cs")
THEOREM Spec => []TypeOK
THEOREM Spec => []MutualExclusion
THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Wed Feb 09 15:50:11 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411621096/MC.out deleted 100644 → 0
View file @ 253af10d
@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.16 of Day Month 20?? (rev: 9310ee7)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 53 and seed -4049060676733912034 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 65295] (Linux 5.10.0-10-amd64 amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.toolbox/Model_1/MC.tla
Parsing file /home/kirr/study/tla+/pluscal/ME/MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/TLC.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Naturals.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/Sequences.tla
Parsing file /home/kirr/src/tools/tla+/bin/toolbox/plugins/org.lamport.tlatools_1.0.0.202201240352/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module MutualExclusionSpec
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2022-02-09 16:00:19)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 4 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 1 distinct state generated at 2022-02-09 16:00:20.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(2) at 2022-02-09 16:00:20: 5 states generated, 3 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 4 branches of temporal properties for the complete state space with 12 total distinct states at (2022-02-09 16:00:20)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2022-02-09 16:00:20
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2193:0 @!@!@
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic): val = 3.3E-19
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-09 16:00:20
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 15, col 1 to line 15, col 4 of module MutualExclusionSpec>: 1:1
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 15, col 9 to line 15, col 36 of module MutualExclusionSpec: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 15, col 16 to line 15, col 36 of module MutualExclusionSpec: 1:2
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 15, col 17 to line 15, col 21 of module MutualExclusionSpec: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 15, col 26 to line 15, col 35 of module MutualExclusionSpec: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<EnterCS line 18, col 1 to line 18, col 13 of module MutualExclusionSpec>: 2:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 19, col 28 to line 19, col 40 of module MutualExclusionSpec: 78
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 19, col 28 to line 19, col 32 of module MutualExclusionSpec: 66
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 19, col 21 to line 19, col 25 of module MutualExclusionSpec: 42
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 6, col 1 to line 6, col 6 of module MC: 42:126
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 20, col 12 to line 20, col 43 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ExitCS line 23, col 1 to line 23, col 12 of module MutualExclusionSpec>: 0:18
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 24, col 12 to line 24, col 26 of module MutualExclusionSpec: 60
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 24, col 12 to line 24, col 19 of module MutualExclusionSpec: 42
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 25, col 12 to line 25, col 47 of module MutualExclusionSpec: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<TypeOK line 10, col 1 to line 10, col 6 of module MutualExclusionSpec>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 10, col 11 to line 10, col 44 of module MutualExclusionSpec: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<MutualExclusion line 39, col 1 to line 39, col 15 of module MutualExclusionSpec>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 39, col 20 to line 39, col 84 of module MutualExclusionSpec: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 39, col 38 to line 39, col 84 of module MutualExclusionSpec: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 39, col 39 to line 39, col 44 of module MutualExclusionSpec: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 39, col 50 to line 39, col 84 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 39, col 52 to line 39, col 83 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 39, col 53 to line 39, col 64 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 39, col 71 to line 39, col 82 of module MutualExclusionSpec: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 39, col 31 to line 39, col 35 of module MutualExclusionSpec: 3
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 6, col 1 to line 6, col 6 of module MC: 3:30
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(2) at 2022-02-09 16:00:20: 5 states generated (248 s/min), 3 distinct states found (149 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
5 states generated, 3 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 2.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1213ms at (2022-02-09 16:00:20)
@!@!@ENDMSG 2186 @!@!@
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411621096/Model_1_SnapShot_1644411621096.dot deleted 100644 → 0
View file @ 253af10d
strict digraph DiskGraph {
edge [colorscheme="paired12"]
nodesep=0.35;
subgraph cluster_graph {
color="white";
-7649361877716949000 [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")",style = filled]
-7649361877716949000 -> -6931778146122684311 [label="",color="2",fontcolor="2"];
-6931778146122684311 [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")"];
-6931778146122684311 -> -7649361877716949000 [label="",color="3",fontcolor="3"];
-7649361877716949000 -> -7872711117459500480 [label="",color="2",fontcolor="2"];
-7872711117459500480 [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")"];
-6931778146122684311 -> -6931778146122684311 [style="dashed"];
-7649361877716949000 -> -7649361877716949000 [style="dashed"];
-7872711117459500480 -> -7649361877716949000 [label="",color="3",fontcolor="3"];
-7872711117459500480 -> -7872711117459500480 [style="dashed"];
{rank = same; -7649361877716949000;}
{rank = same; -7872711117459500480;-6931778146122684311;}
}
subgraph cluster_legend {graph[style=bold];label = "Next State Actions" style="solid"
node [ labeljust="l",colorscheme="paired12",style=filled,shape=record ]
ExitCS [label="ExitCS",fillcolor=3]
EnterCS [label="EnterCS",fillcolor=2]
}}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1_SnapShot_1644411621096/Model_1_liveness.dot deleted 100644 → 0
View file @ 253af10d
digraph DiskGraph {
nodesep=0.35;
subgraph cluster_graph {
color="white";
"-7649361877716949000.1" [style = filled] [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#-7649361877716949000.1#"]
"-7649361877716949000.1" -> "-7872711117459500480.0" [label="[fftftftf]"];
"-7872711117459500480.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#-7872711117459500480.0#"];
"-7649361877716949000.1" -> "-7872711117459500480.1" [label="[fftftftf]"];
"-7872711117459500480.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"cs\")
#-7872711117459500480.1#"];
"-7872711117459500480.1" -> "-7649361877716949000.1" [style="dotted"] [label="[ffftfttt]"];
"-7649361877716949000.1" -> "-7649361877716949000.1" [label="[fffftftf]"];
"-7649361877716949000.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#-7649361877716949000.1#"];
"-7649361877716949000.1" -> "-6931778146122684311.1" [label="[tffftftf]"];
"-6931778146122684311.1" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#-6931778146122684311.1#"];
"-6931778146122684311.1" -> "-7649361877716949000.1" [style="dotted"] [label="[ftffttft]"];
}
}e="dotted"] [label="[ffftfttt]"];
"-7872711117459500480.1" -> "-7649361877716949000.1" [style="dotted"] [label="[ffftfttt]"];
"-7649361877716949000.1" -> "-7649361877716949000.0" [label="[fffftftf]"];
"-7649361877716949000.0" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#-7649361877716949000.0#"];
"-7649361877716949000.1" -> "-7649361877716949000.1" [label="[fffftftf]"];
"-7649361877716949000.1" [label="pc = (0 :> \"non-cs\" @@ 1 :> \"non-cs\")
#-7649361877716949000.1#"];
"-7649361877716949000.1" -> "-6931778146122684311.0" [label="[tffftftf]"];
"-6931778146122684311.0" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#-6931778146122684311.0#"];
"-6931778146122684311.0" -> "-7649361877716949000.2" [style="dotted"] [label="[ftffttft]"];
"-7649361877716949000.1" -> "-6931778146122684311.1" [label="[tffftftf]"];
"-6931778146122684311.1" [label="pc = (0 :> \"cs\" @@ 1 :> \"non-cs\")
#-6931778146122684311.1#"];
"-6931778146122684311.1" -> "-7649361877716949000.0" [style="dotted"] [label="[ftffttft]"];
"-6931778146122684311.1" -> "-7649361877716949000.1" [style="dotted"] [label="[ftffttft]"];
}
}
\ No newline at end of file
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