@!@!@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 @!@!@