Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
K
KTLA Study
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Kirill Smelkov
KTLA Study
Commits
b852b1f1
Commit
b852b1f1
authored
Feb 10, 2022
by
Kirill Smelkov
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
.
parent
fe52d654
Changes
5
Hide whitespace changes
Inline
Side-by-side
Showing
5 changed files
with
0 additions
and
581 deletions
+0
-581
MutualExclusionSpec.toolbox/Model_1/MC.out
MutualExclusionSpec.toolbox/Model_1/MC.out
+0
-189
MutualExclusionSpec.toolbox/Model_1/MC_TE.out
MutualExclusionSpec.toolbox/Model_1/MC_TE.out
+0
-189
MutualExclusionSpec.toolbox/Model_1/Model_1.pdf
MutualExclusionSpec.toolbox/Model_1/Model_1.pdf
+0
-0
MutualExclusionSpec.toolbox/Model_1/Model_1_liveness.dot
MutualExclusionSpec.toolbox/Model_1/Model_1_liveness.dot
+0
-135
MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
+0
-68
No files found.
MutualExclusionSpec.toolbox/Model_1/MC.out
deleted
100644 → 0
View file @
fe52d654
@!@!@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 19 and seed -2142680293908231447 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 90790] (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-10 12:58:49)
@!@!@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: 1 distinct state generated at 2022-02-10 12:58:50.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(4) at 2022-02-10 12:58:50: 15 states generated, 8 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:58:50)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2022-02-10 12:58:50
@!@!@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.0E-18
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-10 12:58:50
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 16, col 1 to line 16, col 4 of module MutualExclusionSpec>: 1:1
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 16, col 9 to line 16, col 36 of module MutualExclusionSpec: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 16, col 16 to line 16, col 36 of module MutualExclusionSpec: 1:2
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 16, col 17 to line 16, col 21 of module MutualExclusionSpec: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 16, col 26 to line 16, col 35 of module MutualExclusionSpec: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<WantCS line 19, col 1 to line 19, col 12 of module MutualExclusionSpec>: 4:10
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 20, col 12 to line 20, col 30 of module MutualExclusionSpec: 34
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 20, col 12 to line 20, col 19 of module MutualExclusionSpec: 24
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 21, col 12 to line 21, col 48 of module MutualExclusionSpec: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<EnterCS line 24, col 1 to line 24, col 13 of module MutualExclusionSpec>: 3:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 25, col 12 to line 25, col 31 of module MutualExclusionSpec: 30
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 25, col 12 to line 25, col 19 of module MutualExclusionSpec: 24
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 26, col 38 to line 26, col 50 of module MutualExclusionSpec: 14
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 26, col 38 to line 26, col 42 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 26, col 21 to line 26, col 34 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 26, col 21 to line 26, col 25 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 11, col 1 to line 11, col 8 of module MC: 8:16
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 2 to line 11, col 3 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 6 to line 11, col 7 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 26, col 29 to line 26, col 34 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 27, col 12 to line 27, col 43 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ExitCS line 30, col 1 to line 30, col 12 of module MutualExclusionSpec>: 0:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 31, col 12 to line 31, col 26 of module MutualExclusionSpec: 30
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 31, col 12 to line 31, col 19 of module MutualExclusionSpec: 24
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 32, col 12 to line 32, col 47 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<TypeOK line 11, col 1 to line 11, col 6 of module MutualExclusionSpec>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 11, col 11 to line 11, col 55 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<MutualExclusion line 47, col 1 to line 47, col 15 of module MutualExclusionSpec>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 11, col 1 to line 11, col 8 of module MC: 8:80
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 2 to line 11, col 3 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 6 to line 11, col 7 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(4) at 2022-02-10 12:58:50: 15 states generated (706 s/min), 8 distinct states found (376 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
15 states generated, 8 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 4.
@!@!@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 1285ms at (2022-02-10 12:58:50)
@!@!@ENDMSG 2186 @!@!@
MutualExclusionSpec.toolbox/Model_1/MC_TE.out
deleted
100644 → 0
View file @
fe52d654
@!@!@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 19 and seed -2142680293908231447 with 2 workers on 4 cores with 1161MB heap and 2608MB offheap memory [pid: 90790] (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-10 12:58:49)
@!@!@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: 1 distinct state generated at 2022-02-10 12:58:50.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(4) at 2022-02-10 12:58:50: 15 states generated, 8 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 5 branches of temporal properties for the complete state space with 40 total distinct states at (2022-02-10 12:58:50)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2022-02-10 12:58:50
@!@!@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.0E-18
@!@!@ENDMSG 2193 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2022-02-10 12:58:50
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 16, col 1 to line 16, col 4 of module MutualExclusionSpec>: 1:1
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 16, col 9 to line 16, col 36 of module MutualExclusionSpec: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
|line 16, col 16 to line 16, col 36 of module MutualExclusionSpec: 1:2
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 16, col 17 to line 16, col 21 of module MutualExclusionSpec: 1
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 16, col 26 to line 16, col 35 of module MutualExclusionSpec: 1:5
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<WantCS line 19, col 1 to line 19, col 12 of module MutualExclusionSpec>: 4:10
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 20, col 12 to line 20, col 30 of module MutualExclusionSpec: 34
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 20, col 12 to line 20, col 19 of module MutualExclusionSpec: 24
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 21, col 12 to line 21, col 48 of module MutualExclusionSpec: 10
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<EnterCS line 24, col 1 to line 24, col 13 of module MutualExclusionSpec>: 3:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 25, col 12 to line 25, col 31 of module MutualExclusionSpec: 30
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 25, col 12 to line 25, col 19 of module MutualExclusionSpec: 24
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 26, col 38 to line 26, col 50 of module MutualExclusionSpec: 14
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 26, col 38 to line 26, col 42 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 26, col 21 to line 26, col 34 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 26, col 21 to line 26, col 25 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 11, col 1 to line 11, col 8 of module MC: 8:16
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 2 to line 11, col 3 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 6 to line 11, col 7 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 26, col 29 to line 26, col 34 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 27, col 12 to line 27, col 43 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<ExitCS line 30, col 1 to line 30, col 12 of module MutualExclusionSpec>: 0:6
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 31, col 12 to line 31, col 26 of module MutualExclusionSpec: 30
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 31, col 12 to line 31, col 19 of module MutualExclusionSpec: 24
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 32, col 12 to line 32, col 47 of module MutualExclusionSpec: 6
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<TypeOK line 11, col 1 to line 11, col 6 of module MutualExclusionSpec>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 11, col 11 to line 11, col 55 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<MutualExclusion line 47, col 1 to line 47, col 15 of module MutualExclusionSpec>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
line 47, col 20 to line 47, col 84 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 38 to line 47, col 84 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 39 to line 47, col 44 of module MutualExclusionSpec: 32
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||line 47, col 50 to line 47, col 84 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 47, col 52 to line 47, col 83 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 53 to line 47, col 64 of module MutualExclusionSpec: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
||||line 47, col 71 to line 47, col 82 of module MutualExclusionSpec: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|line 47, col 31 to line 47, col 35 of module MutualExclusionSpec: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2775:0 @!@!@
||line 11, col 1 to line 11, col 8 of module MC: 8:80
@!@!@ENDMSG 2775 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 2 to line 11, col 3 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
|||line 11, col 6 to line 11, col 7 of module MC: 8
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(4) at 2022-02-10 12:58:50: 15 states generated (706 s/min), 8 distinct states found (376 ds/min), 0 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
15 states generated, 8 distinct states found, 0 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 4.
@!@!@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 1285ms at (2022-02-10 12:58:50)
@!@!@ENDMSG 2186 @!@!@
MutualExclusionSpec.toolbox/Model_1/Model_1.pdf
deleted
100644 → 0
View file @
fe52d654
File deleted
MutualExclusionSpec.toolbox/Model_1/Model_1_liveness.dot
deleted
100644 → 0
View file @
fe52d654
digraph
DiskGraph
{
nodesep
=
0.35
;
subgraph
cluster_graph
{
color
=
"white"
;
"7826388974498231005.1"
[
style
=
filled
]
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")
#7826388974498231005.1#"
]
"7826388974498231005.1"
->
"7743948932593470164.1"
[
label
=
"[fffftttt]"
]
;
"7743948932593470164.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")
#7743948932593470164.1#"
]
;
"7826388974498231005.1"
->
"-7091387860856146872.1"
[
label
=
"[fffftttt]"
]
;
"-7091387860856146872.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.1#"
]
;
"7826388974498231005.1"
->
"7826388974498231005.1"
[
label
=
"[fffftttt]"
]
;
"7826388974498231005.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")
#7826388974498231005.1#"
]
;
"7743948932593470164.1"
->
"7743948932593470164.1"
[
label
=
"[fffftttf]"
]
;
"7743948932593470164.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")
#7743948932593470164.1#"
]
;
"7743948932593470164.1"
->
"1520033749518464798.1"
[
label
=
"[tffftttf]"
]
;
"1520033749518464798.1"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\")
#1520033749518464798.1#"
]
;
"7743948932593470164.1"
->
"2891225834013969262.1"
[
label
=
"[fffftttf]"
]
;
"2891225834013969262.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")
#2891225834013969262.1#"
]
;
"-7091387860856146872.1"
->
"-7604993468008606684.0"
[
label
=
"[fftftftt]"
]
;
"-7604993468008606684.0"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")
#-7604993468008606684.0#"
]
;
"-7091387860856146872.1"
->
"-7604993468008606684.1"
[
label
=
"[fftftftt]"
]
;
"-7604993468008606684.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")
#-7604993468008606684.1#"
]
;
"-7091387860856146872.1"
->
"-7091387860856146872.1"
[
label
=
"[fffftftt]"
]
;
"-7091387860856146872.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.1#"
]
;
"-7091387860856146872.1"
->
"2891225834013969262.1"
[
label
=
"[fffftftt]"
]
;
"2891225834013969262.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")
#2891225834013969262.1#"
]
;
"1520033749518464798.1"
->
"8048625394011437004.1"
[
label
=
"[ffffttft]"
]
;
"8048625394011437004.1"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.1#"
]
;
"1520033749518464798.1"
->
"7826388974498231005.1"
[
label
=
"[ftffttft]"
]
;
"7826388974498231005.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")
#7826388974498231005.1#"
]
;
"1520033749518464798.1"
->
"1520033749518464798.1"
[
label
=
"[ffffttft]"
]
;
"1520033749518464798.1"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"non-cs\")
#1520033749518464798.1#"
]
;
"2891225834013969262.1"
->
"6198530037439632960.0"
[
label
=
"[fftftftf]"
]
;
"6198530037439632960.0"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.0#"
]
;
"2891225834013969262.1"
->
"6198530037439632960.1"
[
label
=
"[fftftftf]"
]
;
"6198530037439632960.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.1#"
]
;
"2891225834013969262.1"
->
"8048625394011437004.1"
[
label
=
"[tffftftf]"
]
;
"8048625394011437004.1"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.1#"
]
;
"2891225834013969262.1"
->
"2891225834013969262.1"
[
label
=
"[fffftftf]"
]
;
"2891225834013969262.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"csentry\")
#2891225834013969262.1#"
]
;
"-7604993468008606684.0"
->
"6198530037439632960.2"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.2"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.2#"
]
;
"-7604993468008606684.0"
->
"-7604993468008606684.2"
[
label
=
"[fffffttt]"
]
;
"-7604993468008606684.2"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")
#-7604993468008606684.2#"
]
;
"-7604993468008606684.2"
->
"6198530037439632960.2"
[
style
=
"dotted"
]
[
label
=
"[fffffttt]"
]
;
"-7604993468008606684.1"
->
"6198530037439632960.0"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.0"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.0#"
]
;
"-7604993468008606684.1"
->
"6198530037439632960.1"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.1#"
]
;
"-7604993468008606684.1"
->
"-7604993468008606684.0"
[
label
=
"[fffffttt]"
]
;
"-7604993468008606684.0"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")
#-7604993468008606684.0#"
]
;
"-7604993468008606684.1"
->
"-7604993468008606684.1"
[
label
=
"[fffffttt]"
]
;
"-7604993468008606684.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"cs\")
#-7604993468008606684.1#"
]
;
"-7604993468008606684.1"
->
"7826388974498231005.1"
[
label
=
"[ffftfttt]"
]
;
"7826388974498231005.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"non-cs\")
#7826388974498231005.1#"
]
;
"8048625394011437004.1"
->
"-7091387860856146872.1"
[
label
=
"[ftffttft]"
]
;
"-7091387860856146872.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.1#"
]
;
"8048625394011437004.1"
->
"8048625394011437004.1"
[
label
=
"[ffffttft]"
]
;
"8048625394011437004.1"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.1#"
]
;
"6198530037439632960.0"
->
"6198530037439632960.2"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.2"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.2#"
]
;
"6198530037439632960.1"
->
"6198530037439632960.0"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.0"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.0#"
]
;
"6198530037439632960.1"
->
"6198530037439632960.1"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.1#"
]
;
"6198530037439632960.1"
->
"7743948932593470164.1"
[
label
=
"[ffftfttt]"
]
;
"7743948932593470164.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")
#7743948932593470164.1#"
]
;
"6198530037439632960.2"
->
"6198530037439632960.2"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.2"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.2#"
]
;
}
}
")
#7826388974498231005.1#"
]
;
"8048625394011437004.0"
->
"-7091387860856146872.2"
[
label
=
"[ftffttft]"
]
;
"-7091387860856146872.2"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.2#"
]
;
"8048625394011437004.0"
->
"8048625394011437004.2"
[
label
=
"[ffffttft]"
]
;
"8048625394011437004.2"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.2#"
]
;
"8048625394011437004.1"
->
"-7091387860856146872.0"
[
label
=
"[ftffttft]"
]
;
"-7091387860856146872.0"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.0#"
]
;
"8048625394011437004.1"
->
"-7091387860856146872.1"
[
label
=
"[ftffttft]"
]
;
"-7091387860856146872.1"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.1#"
]
;
"8048625394011437004.1"
->
"8048625394011437004.0"
[
label
=
"[ffffttft]"
]
;
"8048625394011437004.0"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.0#"
]
;
"8048625394011437004.1"
->
"8048625394011437004.1"
[
label
=
"[ffffttft]"
]
;
"8048625394011437004.1"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.1#"
]
;
"8048625394011437004.2"
->
"-7091387860856146872.2"
[
label
=
"[ftffttft]"
]
;
"-7091387860856146872.2"
[
label
=
"pc = (p1 :> \"non-cs\" @@ p2 :> \"csentry\")
#-7091387860856146872.2#"
]
;
"8048625394011437004.2"
->
"8048625394011437004.2"
[
label
=
"[ffffttft]"
]
;
"8048625394011437004.2"
[
label
=
"pc = (p1 :> \"cs\" @@ p2 :> \"csentry\")
#8048625394011437004.2#"
]
;
"6198530037439632960.1"
->
"6198530037439632960.1"
[
label
=
"[fffffttt]"
]
;
"6198530037439632960.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"cs\")
#6198530037439632960.1#"
]
;
"6198530037439632960.1"
->
"7743948932593470164.1"
[
label
=
"[ffftfttt]"
]
;
"7743948932593470164.1"
[
label
=
"pc = (p1 :> \"csentry\" @@ p2 :> \"non-cs\")
#7743948932593470164.1#"
]
;
}
}
\ No newline at end of file
MutualExclusionSpec.toolbox/Model_1/MutualExclusionSpec.tla
deleted
100644 → 0
View file @
fe52d654
------------------------ MODULE MutualExclusionSpec ------------------------
\* Module MutualExclusionSpec provides general specification for mutual-exclusion problem.
\* Procs is set of processes.
\* Every process is assumed to loop and enter into "cs" state on every interation.
\* Non-critical state is represented as "non-cs".
\* When process decides it want to enter into critical-section, it first goes into "csentry" state.
CONSTANT Procs
VARIABLES pc
TypeOK == pc \in [Procs -> {"non-cs", "csentry", "cs"}]
vars == <<pc>>
\* All processes start from non-critical section.
Init == pc \in [Procs -> {"non-cs"}]
\* WantCS(proc) is action when proc decides that it wants to enter into critical section.
WantCS(proc) ==
/\ pc[proc] = "non-cs"
/\ pc' = [pc EXCEPT ![proc] = "csentry"]
\* EnterCS(proc) is action when proc enters critical section.
EnterCS(proc) ==
/\ pc[proc] = "csentry"
/\ \A i \in Procs \ {proc} : pc[i] /= "cs"
/\ pc' = [pc EXCEPT ![proc] = "cs"]
\* ExitCS(proc) is action when proc leaves critical section.
ExitCS(proc) ==
/\ pc[proc] = "cs"
/\ pc' = [pc EXCEPT ![proc] = "non-cs"]
Next == \E i \in Procs: WantCS(i) \/ EnterCS(i) \/ ExitCS(i)
Spec == /\ Init
/\ [][Next]_vars
/\ \A i \in Procs: ( \* fairness
\* not fair for WantCS - it can pause and even hang there
/\ SF_vars(EnterCS(i))
/\ SF_vars(ExitCS(i)))
----------------
\* MutualExclusion is invariant indicating that no two processes can be inside critical section at the same time.
MutualExclusion == \A i,j \in Procs: (i /= j) => ~((pc[i] = "cs") /\ (pc[j] = "cs"))
\* Liveness is temporal property indicating that every process has a chance to enter critical section and leaves it.
\* A process should keep on entering the critical-section unless it is stuck in it non-critical part.
Liveness == \A i \in Procs:
/\
\/ <>[](pc[i] = "non-cs") \* either stuck in non-cs, or
\/ []<>(pc[i] = "csentry") \* keeps on reaching "enter cs"
/\
/\ (pc[i] = "csentry") ~> (pc[i] = "cs") \* if it wants to enter, it enters cs and leaves it
/\ (pc[i] = "cs") ~> (pc[i] = "non-cs")
THEOREM Spec => []TypeOK
THEOREM Spec => []MutualExclusion
THEOREM Spec => Liveness
=============================================================================
\* Modification History
\* Last modified Thu Feb 10 12:58:08 MSK 2022 by kirr
\* Created Wed Feb 09 13:11:29 MSK 2022 by kirr
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment
