mirror of https://github.com/vacp2p/research.git
118 lines
4.8 KiB
Plaintext
118 lines
4.8 KiB
Plaintext
|
@!@!@STARTMSG 2262:0 @!@!@
|
||
|
|
TLC2 Version 2.13 of 18 July 2018
|
||
|
|
@!@!@ENDMSG 2262 @!@!@
|
||
|
|
@!@!@STARTMSG 2187:0 @!@!@
|
||
|
|
Running breadth-first search Model-Checking with seed 6383722702755738499 with 4 workers on 8 cores with 1154MB heap and 2594MB offheap memory (Linux 5.2.18-100.fc29.x86_64 amd64, Oracle Corporation 1.8.0_222 x86_64).
|
||
|
|
@!@!@ENDMSG 2187 @!@!@
|
||
|
|
@!@!@STARTMSG 2220:0 @!@!@
|
||
|
|
Starting SANY...
|
||
|
|
@!@!@ENDMSG 2220 @!@!@
|
||
|
|
Parsing file /home/oskarth/git/vacp2p/research/tlaplus/gossip/gossip.toolbox/Model_1/MC.tla
|
||
|
|
Parsing file /home/oskarth/git/vacp2p/research/tlaplus/gossip/gossip.toolbox/Model_1/gossip.tla
|
||
|
|
Parsing file /home/oskarth/bin/tlaplus/toolbox/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/TLC.tla
|
||
|
|
Parsing file /home/oskarth/bin/tlaplus/toolbox/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/Integers.tla
|
||
|
|
Parsing file /home/oskarth/bin/tlaplus/toolbox/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/Naturals.tla
|
||
|
|
Parsing file /home/oskarth/bin/tlaplus/toolbox/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/Sequences.tla
|
||
|
|
Parsing file /home/oskarth/bin/tlaplus/toolbox/plugins/org.lamport.tlatools_1.0.0.201807180447/tla2sany/StandardModules/FiniteSets.tla
|
||
|
|
Semantic processing of module Naturals
|
||
|
|
Semantic processing of module Integers
|
||
|
|
Semantic processing of module gossip
|
||
|
|
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... (2019-12-03 22:24:23)
|
||
|
|
@!@!@ENDMSG 2185 @!@!@
|
||
|
|
@!@!@STARTMSG 2189:0 @!@!@
|
||
|
|
Computing initial states...
|
||
|
|
@!@!@ENDMSG 2189 @!@!@
|
||
|
|
@!@!@STARTMSG 2190:0 @!@!@
|
||
|
|
Finished computing initial states: 1 distinct state generated.
|
||
|
|
@!@!@ENDMSG 2190 @!@!@
|
||
|
|
@!@!@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 = 1.6E-19
|
||
|
|
based on the actual fingerprints: val = 1.8E308
|
||
|
|
@!@!@ENDMSG 2193 @!@!@
|
||
|
|
@!@!@STARTMSG 2201:0 @!@!@
|
||
|
|
The coverage statistics at 2019-12-03 22:24:26
|
||
|
|
@!@!@ENDMSG 2201 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 30, col 12 to line 30, col 17 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 30, col 20 to line 30, col 22 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 30, col 25 to line 30, col 30 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 30, col 33 to line 30, col 40 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 30, col 43 to line 30, col 48 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 30, col 51 to line 30, col 52 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 41, col 16 to line 41, col 67 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 42, col 16 to line 42, col 30 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 43, col 29 to line 43, col 34 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 43, col 37 to line 43, col 42 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 43, col 45 to line 43, col 52 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 43, col 55 to line 43, col 60 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 46, col 15 to line 46, col 70 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 47, col 15 to line 47, col 26 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 48, col 28 to line 48, col 33 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 48, col 36 to line 48, col 41 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 48, col 44 to line 48, col 51 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
||
|
|
line 48, col 54 to line 48, col 59 of module gossip: 1
|
||
|
|
@!@!@ENDMSG 2221 @!@!@
|
||
|
|
@!@!@STARTMSG 2202:0 @!@!@
|
||
|
|
End of statistics.
|
||
|
|
@!@!@ENDMSG 2202 @!@!@
|
||
|
|
@!@!@STARTMSG 2200:0 @!@!@
|
||
|
|
Progress(3) at 2019-12-03 22:24:26: 4 states generated (78 s/min), 3 distinct states found (58 ds/min), 0 states left on queue.
|
||
|
|
@!@!@ENDMSG 2200 @!@!@
|
||
|
|
@!@!@STARTMSG 2199:0 @!@!@
|
||
|
|
4 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 3.
|
||
|
|
@!@!@ENDMSG 2194 @!@!@
|
||
|
|
@!@!@STARTMSG 2268:0 @!@!@
|
||
|
|
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).
|
||
|
|
@!@!@ENDMSG 2268 @!@!@
|
||
|
|
@!@!@STARTMSG 2186:0 @!@!@
|
||
|
|
Finished in 3336ms at (2019-12-03 22:24:26)
|
||
|
|
@!@!@ENDMSG 2186 @!@!@
|