TLCReliableBroadcastFD.out

@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.18 of Day Month 20?? (rev: 2576f2c)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 116 and seed -8753646190424304002 with 16 workers on 20 cores with 45511MB heap and 64MB offheap memory [pid: 1836973] (Linux 6.6.10-76060610-generic amd64, Private Build 17.0.10 x86_64, OffHeapDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/nano/Documents/learner-graphs/TLCReliableBroadcastFD.tla
Parsing file /home/nano/Documents/learner-graphs/ReliableBroadcastFD.tla
Warning: symbols were renamed.
Parsing file /tmp/tlc-11537335082936150615/TLC.tla (jar:file:/home/nano/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.2.2906/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /home/nano/Documents/learner-graphs/LearnerGraph.tla
Parsing file /tmp/tlc-11537335082936150615/FiniteSets.tla (jar:file:/home/nano/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.2.2906/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-11537335082936150615/Naturals.tla (jar:file:/home/nano/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.2.2906/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-11537335082936150615/Sequences.tla (jar:file:/home/nano/.vscode/extensions/alygin.vscode-tlaplus-nightly-2024.2.2906/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module LearnerGraph
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module ReliableBroadcastFD
Semantic processing of module TLC
Semantic processing of module TLCReliableBroadcastFD
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2024-02-29 14:20:38)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2212:0 @!@!@
Implied-temporal checking--satisfiability problem has 3 branches.
@!@!@ENDMSG 2212 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2190:0 @!@!@
Finished computing initial states: 3 distinct states generated at 2024-02-29 14:20:38.
@!@!@ENDMSG 2190 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 109468 total distinct states at (2024-02-29 14:20:41)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 00s at 2024-02-29 14:20:41
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(8) at 2024-02-29 14:20:41: 179,968 states generated (179,968 s/min), 43,159 distinct states found (43,159 ds/min), 33,652 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 1678388 total distinct states at (2024-02-29 14:21:41)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 01s at 2024-02-29 14:21:43
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(10) at 2024-02-29 14:21:43: 5,900,741 states generated (5,720,773 s/min), 666,759 distinct states found (623,600 ds/min), 428,765 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 2900994 total distinct states at (2024-02-29 14:22:43)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 03s at 2024-02-29 14:22:46
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(11) at 2024-02-29 14:22:46: 12,150,710 states generated (6,249,969 s/min), 1,155,786 distinct states found (489,027 ds/min), 696,064 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 3966098 total distinct states at (2024-02-29 14:23:46)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 05s at 2024-02-29 14:23:51
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(11) at 2024-02-29 14:23:51: 17,996,834 states generated (5,846,124 s/min), 1,571,164 distinct states found (415,378 ds/min), 901,582 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 4933067 total distinct states at (2024-02-29 14:24:51)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 07s at 2024-02-29 14:24:58
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(11) at 2024-02-29 14:24:58: 24,891,362 states generated (6,894,528 s/min), 1,943,597 distinct states found (372,433 ds/min), 1,054,688 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 5997465 total distinct states at (2024-02-29 14:25:58)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 08s at 2024-02-29 14:26:07
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(12) at 2024-02-29 14:26:07: 31,064,845 states generated (6,173,483 s/min), 2,366,135 distinct states found (422,538 ds/min), 1,266,216 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 6949994 total distinct states at (2024-02-29 14:27:07)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 10s at 2024-02-29 14:27:18
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(12) at 2024-02-29 14:27:18: 36,997,666 states generated (5,932,821 s/min), 2,735,472 distinct states found (369,337 ds/min), 1,430,500 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 7824380 total distinct states at (2024-02-29 14:28:18)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 12s at 2024-02-29 14:28:30
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(12) at 2024-02-29 14:28:30: 43,344,791 states generated (6,347,125 s/min), 3,068,604 distinct states found (333,132 ds/min), 1,556,723 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 8706318 total distinct states at (2024-02-29 14:29:30)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 13s at 2024-02-29 14:29:44
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(12) at 2024-02-29 14:29:44: 50,379,464 states generated (7,034,673 s/min), 3,398,456 distinct states found (329,852 ds/min), 1,662,268 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 9544454 total distinct states at (2024-02-29 14:30:44)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 16s at 2024-02-29 14:31:00
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(12) at 2024-02-29 14:31:00: 58,143,987 states generated (7,764,523 s/min), 3,704,300 distinct states found (305,844 ds/min), 1,738,532 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 10505993 total distinct states at (2024-02-29 14:32:00)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 17s at 2024-02-29 14:32:17
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:32:17: 64,217,343 states generated (6,073,356 s/min), 4,082,772 distinct states found (378,472 ds/min), 1,915,232 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:33:17: 71,352,888 states generated (7,135,545 s/min), 4,392,813 distinct states found (310,041 ds/min), 2,004,917 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 12154692 total distinct states at (2024-02-29 14:34:17)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 20s at 2024-02-29 14:34:38
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:34:38: 77,585,221 states generated (6,232,333 s/min), 4,695,240 distinct states found (302,427 ds/min), 2,103,266 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:35:38: 83,586,078 states generated (6,000,857 s/min), 4,995,228 distinct states found (299,988 ds/min), 2,214,177 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 13658033 total distinct states at (2024-02-29 14:36:38)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 24s at 2024-02-29 14:37:02
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:37:02: 89,816,571 states generated (6,230,493 s/min), 5,260,564 distinct states found (265,336 ds/min), 2,292,079 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:38:02: 97,142,207 states generated (7,325,636 s/min), 5,521,491 distinct states found (260,927 ds/min), 2,322,606 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 15127075 total distinct states at (2024-02-29 14:39:02)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 28s at 2024-02-29 14:39:31
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:39:31: 104,225,836 states generated (7,083,629 s/min), 5,782,269 distinct states found (260,778 ds/min), 2,375,825 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(13) at 2024-02-29 14:40:31: 112,629,696 states generated (8,403,860 s/min), 6,039,090 distinct states found (256,821 ds/min), 2,400,343 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 16639889 total distinct states at (2024-02-29 14:41:31)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 31s at 2024-02-29 14:42:02
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:42:02: 118,983,625 states generated (6,353,929 s/min), 6,326,946 distinct states found (287,856 ds/min), 2,492,707 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:43:02: 125,052,430 states generated (6,068,805 s/min), 6,616,260 distinct states found (289,314 ds/min), 2,594,033 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 18219938 total distinct states at (2024-02-29 14:44:02)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 36s at 2024-02-29 14:44:39
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:44:39: 132,661,794 states generated (7,609,364 s/min), 6,912,356 distinct states found (296,096 ds/min), 2,666,045 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:45:39: 140,082,373 states generated (7,420,579 s/min), 7,155,715 distinct states found (243,359 ds/min), 2,684,421 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:46:39: 146,815,639 states generated (6,733,266 s/min), 7,404,940 distinct states found (249,225 ds/min), 2,728,607 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 20293612 total distinct states at (2024-02-29 14:47:39)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 43s at 2024-02-29 14:48:22
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:48:22: 152,597,339 states generated (5,781,700 s/min), 7,651,183 distinct states found (246,243 ds/min), 2,799,756 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:49:22: 159,070,683 states generated (6,473,344 s/min), 7,879,773 distinct states found (228,590 ds/min), 2,842,652 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:50:22: 165,515,610 states generated (6,444,927 s/min), 8,086,177 distinct states found (206,404 ds/min), 2,867,772 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 22162680 total distinct states at (2024-02-29 14:51:22)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 45s at 2024-02-29 14:52:07
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2195:0 @!@!@
Checkpointing of run states/24-02-29-14-20-37.805
@!@!@ENDMSG 2195 @!@!@
@!@!@STARTMSG 2196:0 @!@!@
Checkpointing completed at (2024-02-29 14:52:07)
@!@!@ENDMSG 2196 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:52:07: 173,047,366 states generated (7,531,756 s/min), 8,295,098 distinct states found (208,921 ds/min), 2,845,183 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:53:07: 180,145,781 states generated (7,098,415 s/min), 8,518,516 distinct states found (223,418 ds/min), 2,871,690 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:54:07: 187,752,794 states generated (7,607,013 s/min), 8,725,415 distinct states found (206,899 ds/min), 2,864,643 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 24103541 total distinct states at (2024-02-29 14:55:07)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 55s at 2024-02-29 14:56:02
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(14) at 2024-02-29 14:56:02: 196,922,233 states generated (9,169,439 s/min), 8,944,625 distinct states found (219,210 ds/min), 2,843,136 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 14:57:02: 202,972,575 states generated (6,050,342 s/min), 9,196,941 distinct states found (252,316 ds/min), 2,914,113 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 14:58:02: 209,323,937 states generated (6,351,362 s/min), 9,439,181 distinct states found (242,240 ds/min), 2,968,223 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 14:59:02: 216,461,121 states generated (7,137,184 s/min), 9,682,246 distinct states found (243,065 ds/min), 3,006,421 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 26807362 total distinct states at (2024-02-29 15:00:02)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 59s at 2024-02-29 15:01:02
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:01:02: 223,973,034 states generated (7,511,913 s/min), 9,909,557 distinct states found (227,311 ds/min), 3,026,887 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:02:02: 231,887,968 states generated (7,914,934 s/min), 10,110,313 distinct states found (200,756 ds/min), 3,005,718 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:03:02: 238,560,252 states generated (6,672,284 s/min), 10,302,176 distinct states found (191,863 ds/min), 2,998,453 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:04:02: 244,412,663 states generated (5,852,411 s/min), 10,490,753 distinct states found (188,577 ds/min), 3,023,183 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 29087567 total distinct states at (2024-02-29 15:05:02)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 01min 13s at 2024-02-29 15:06:15
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:06:15: 250,069,835 states generated (5,657,172 s/min), 10,680,817 distinct states found (190,064 ds/min), 3,048,547 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:07:15: 256,400,235 states generated (6,330,400 s/min), 10,861,339 distinct states found (180,522 ds/min), 3,054,304 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:08:15: 263,159,126 states generated (6,758,891 s/min), 11,032,829 distinct states found (171,490 ds/min), 3,053,128 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:09:15: 269,896,344 states generated (6,737,218 s/min), 11,199,865 distinct states found (167,036 ds/min), 3,023,677 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:10:15: 277,607,993 states generated (7,711,649 s/min), 11,378,630 distinct states found (178,765 ds/min), 2,988,087 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 31745575 total distinct states at (2024-02-29 15:11:15)
@!@!@ENDMSG 2192 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 01min 20s at 2024-02-29 15:12:36
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:12:36: 284,697,979 states generated (7,089,986 s/min), 11,547,485 distinct states found (168,855 ds/min), 2,972,247 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(15) at 2024-02-29 15:13:36: 293,296,234 states generated (8,598,255 s/min), 11,723,410 distinct states found (175,925 ds/min), 2,924,424 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(16) at 2024-02-29 15:14:36: 301,239,128 states generated (7,942,894 s/min), 11,906,994 distinct states found (183,584 ds/min), 2,893,387 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(16) at 2024-02-29 15:15:36: 307,453,419 states generated (6,214,291 s/min), 12,109,953 distinct states found (202,959 ds/min), 2,920,871 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(16) at 2024-02-29 15:16:36: 313,908,110 states generated (6,454,691 s/min), 12,297,815 distinct states found (187,862 ds/min), 2,927,928 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2192:0 @!@!@
Checking 3 branches of temporal properties for the current state space with 34587838 total distinct states at (2024-02-29 15:17:36)
@!@!@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>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {} @@ a2 :> {} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <l0_("failure-detector") line 139, col 14 to line 148, col 58 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {} @@ a2 :> {} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <l0(a1) line 191, col 13 to line 200, col 48 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <l0(a1) line 191, col 13 to line 200, col 48 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <l0_a(a2) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <l0_a(a3) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
7: <l0_a(a2) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
8: <l0_("failure-detector") line 139, col 14 to line 148, col 58 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
9: <l0_a(a3) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
10: <l0_a(a3) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {v1} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
11: <l0_a(a3) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {v1} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {v2})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
12: <l0_a(a2) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {v2} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {v1} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {v2})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
13: <l0_a(a2) line 162, col 15 to line 187, col 50 of module ReliableBroadcastFD>
/\ output = (la :> <<>> @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {v1, v2} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {v1} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {v2})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "l0_l" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
14: <l0_l(la) line 152, col 15 to line 158, col 55 of module ReliableBroadcastFD>
/\ output = (la :> v1 @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {v1, v2} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {v1} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {v2})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "Done" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "l0_" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
15: <l0_("failure-detector") line 139, col 14 to line 148, col 58 of module ReliableBroadcastFD>
/\ output = (la :> v1 @@ lb :> <<>> @@ lc :> <<>>)
/\ ready = ( a1 :> (la :> {v1} @@ lb :> {} @@ lc :> {}) @@
  a2 :> (la :> {v1, v2} @@ lb :> {} @@ lc :> {v1}) @@
  a3 :> (la :> {v1} @@ lb :> {v1} @@ lc :> {v1}) )
/\ bcast = {v1, v2}
/\ echo = (a1 :> {v2} @@ a2 :> {v2} @@ a3 :> {v2})
/\ pc = ( a1 :> "l0" @@
  a2 :> "l0_a" @@
  a3 :> "l0_a" @@
  la :> "Done" @@
  lb :> "l0_l" @@
  lc :> "l0_l" @@
  "failure-detector" :> "Done" )
/\ fd = (a1 :> {} @@ a2 :> {a1} @@ a3 :> {a1})

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2218:4 @!@!@
16: Stuttering
@!@!@ENDMSG 2218 @!@!@
@!@!@STARTMSG 2267:0 @!@!@
Finished checking temporal properties in 01min 28s at 2024-02-29 15:19:04
@!@!@ENDMSG 2267 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(16) at 2024-02-29 15:19:04: 319,956,580 states generated (5,474,649 s/min), 12,488,558 distinct states found (213,686 ds/min), 2,947,980 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
319956580 states generated, 12488558 distinct states found, 2947980 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 16.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 3506598ms at (2024-02-29 15:19:04)
@!@!@ENDMSG 2186 @!@!@