mirror of
https://github.com/vacp2p/research.git
synced 2025-02-23 19:58:30 +00:00
170 lines
6.3 KiB
Plaintext
170 lines
6.3 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 -7282132633026483868 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-04 12:37:55)
|
|
@!@!@ENDMSG 2185 @!@!@
|
|
@!@!@STARTMSG 2212:0 @!@!@
|
|
Implied-temporal checking--satisfiability problem has 1 branches.
|
|
@!@!@ENDMSG 2212 @!@!@
|
|
@!@!@STARTMSG 2189:0 @!@!@
|
|
Computing initial states...
|
|
@!@!@ENDMSG 2189 @!@!@
|
|
@!@!@STARTMSG 2190:0 @!@!@
|
|
Finished computing initial states: 1 distinct state generated.
|
|
@!@!@ENDMSG 2190 @!@!@
|
|
@!@!@STARTMSG 2200:0 @!@!@
|
|
Progress(3) at 2019-12-04 12:37:56: 4 states generated, 3 distinct states found, 0 states left on queue.
|
|
@!@!@ENDMSG 2200 @!@!@
|
|
@!@!@STARTMSG 2192:0 @!@!@
|
|
Checking temporal properties for the complete state space with 3 total distinct states at (2019-12-04 12:37:56)
|
|
@!@!@ENDMSG 2192 @!@!@
|
|
@!@!@STARTMSG 2116:1 @!@!@
|
|
Temporal properties were violated.
|
|
|
|
@!@!@ENDMSG 2116 @!@!@
|
|
@!@!@STARTMSG 2264:1 @!@!@
|
|
The following behavior constitutes a counter-example:
|
|
|
|
@!@!@ENDMSG 2264 @!@!@
|
|
@!@!@STARTMSG 2217:4 @!@!@
|
|
1: <Initial predicate>
|
|
/\ sender = "alice"
|
|
/\ receiver = "bob"
|
|
/\ inbox = [alice |-> 0, bob |-> 0, charlie |-> 0]
|
|
/\ amount = 4
|
|
/\ pc = "Send"
|
|
/\ peers = [alice |-> "charlie", bob |-> "charlie", charlie |-> "charlie"]
|
|
/\ nodes = {"alice", "bob", "charlie"}
|
|
|
|
@!@!@ENDMSG 2217 @!@!@
|
|
@!@!@STARTMSG 2217:4 @!@!@
|
|
2: <Send line 43, col 9 to line 46, col 65 of module gossip>
|
|
/\ sender = "alice"
|
|
/\ receiver = "bob"
|
|
/\ inbox = [alice |-> 1, bob |-> 0, charlie |-> 0]
|
|
/\ amount = 4
|
|
/\ pc = "Propagate"
|
|
/\ peers = [alice |-> "charlie", bob |-> "charlie", charlie |-> "charlie"]
|
|
/\ nodes = {"alice", "bob", "charlie"}
|
|
|
|
@!@!@ENDMSG 2217 @!@!@
|
|
@!@!@STARTMSG 2217:4 @!@!@
|
|
3: <Propagate line 48, col 14 to line 51, col 70 of module gossip>
|
|
/\ sender = "alice"
|
|
/\ receiver = "bob"
|
|
/\ inbox = [alice |-> 1, bob |-> 0, charlie |-> 1]
|
|
/\ amount = 4
|
|
/\ pc = "Done"
|
|
/\ peers = [alice |-> "charlie", bob |-> "charlie", charlie |-> "charlie"]
|
|
/\ nodes = {"alice", "bob", "charlie"}
|
|
|
|
@!@!@ENDMSG 2217 @!@!@
|
|
@!@!@STARTMSG 2218:4 @!@!@
|
|
4: Stuttering
|
|
@!@!@ENDMSG 2218 @!@!@
|
|
@!@!@STARTMSG 2267:0 @!@!@
|
|
Finished checking temporal properties in 00s at 2019-12-04 12:37:56
|
|
@!@!@ENDMSG 2267 @!@!@
|
|
@!@!@STARTMSG 2201:0 @!@!@
|
|
The coverage statistics at 2019-12-04 12:37:56
|
|
@!@!@ENDMSG 2201 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 12 to line 32, col 16 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 19 to line 32, col 23 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 26 to line 32, col 30 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 33 to line 32, col 38 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 41 to line 32, col 48 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 51 to line 32, col 56 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 32, col 59 to line 32, col 60 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 44, col 12 to line 44, col 64 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 45, col 12 to line 45, col 28 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 46, col 25 to line 46, col 29 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 46, col 32 to line 46, col 36 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 46, col 39 to line 46, col 44 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 46, col 47 to line 46, col 54 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 46, col 57 to line 46, col 62 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 49, col 17 to line 49, col 83 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 50, col 17 to line 50, col 28 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 51, col 30 to line 51, col 34 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 51, col 37 to line 51, col 41 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 51, col 44 to line 51, col 49 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 51, col 52 to line 51, col 59 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2221:0 @!@!@
|
|
line 51, col 62 to line 51, col 67 of module gossip: 1
|
|
@!@!@ENDMSG 2221 @!@!@
|
|
@!@!@STARTMSG 2202:0 @!@!@
|
|
End of statistics.
|
|
@!@!@ENDMSG 2202 @!@!@
|
|
@!@!@STARTMSG 2200:0 @!@!@
|
|
Progress(3) at 2019-12-04 12:37:56: 4 states generated (342 s/min), 3 distinct states found (257 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 2186:0 @!@!@
|
|
Finished in 980ms at (2019-12-04 12:37:56)
|
|
@!@!@ENDMSG 2186 @!@!@
|