-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathMC_liveness.out
102 lines (102 loc) · 10.7 KB
/
MC_liveness.out
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
$ tlc MC_liveness.tla -workers 4096 -deadlock
TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99)
Running breadth-first search Model-Checking with fp 29 and seed 3784523914182979876 with 4096 workers on 64 cores with 27305MB heap and 64MB offheap memory [pid: 53071] (Linux 5.3.0-64-generic amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/tla/models/handshaking/blacklist_timeouts/nack_peers/MC_liveness.tla
Parsing file /home/tla/models/handshaking/blacklist_timeouts/nack_peers/Handshaking_nack_peers.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Handshaking_nack_peers
Semantic processing of module TLC
Semantic processing of module MC_liveness
Starting... (2021-04-20 01:56:03)
Implied-temporal checking--satisfiability problem has 27 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2021-04-20 01:56:04.
Checking 27 branches of temporal properties for the current state space with 563867 total distinct states at (2021-04-20 01:56:33)
Finished checking temporal properties in 00s at 2021-04-20 01:56:34
Progress(15) at 2021-04-20 01:56:34: 90,645 states generated (90,645 s/min), 21,456 distinct states found (21,456 ds/min), 15,443 states left on queue.
Checking 27 branches of temporal properties for the current state space with 3167369 total distinct states at (2021-04-20 01:57:35)
Finished checking temporal properties in 01s at 2021-04-20 01:57:36
Progress(17) at 2021-04-20 01:57:36: 1,048,507 states generated (957,862 s/min), 119,363 distinct states found (97,907 ds/min), 55,431 states left on queue.
Checking 27 branches of temporal properties for the current state space with 5350241 total distinct states at (2021-04-20 01:58:39)
Finished checking temporal properties in 08s at 2021-04-20 01:58:47
Progress(18) at 2021-04-20 01:58:47: 2,036,971 states generated (988,464 s/min), 201,110 distinct states found (81,747 ds/min), 79,728 states left on queue.
Checking 27 branches of temporal properties for the current state space with 7474254 total distinct states at (2021-04-20 01:59:50)
Finished checking temporal properties in 04s at 2021-04-20 01:59:54
Progress(19) at 2021-04-20 01:59:54: 3,055,746 states generated (1,018,775 s/min), 280,568 distinct states found (79,458 ds/min), 101,081 states left on queue.
Checking 27 branches of temporal properties for the current state space with 9475990 total distinct states at (2021-04-20 02:00:56)
Finished checking temporal properties in 05s at 2021-04-20 02:01:01
Progress(20) at 2021-04-20 02:01:01: 4,078,597 states generated (1,022,851 s/min), 355,320 distinct states found (74,752 ds/min), 117,649 states left on queue.
Checking 27 branches of temporal properties for the current state space with 11392180 total distinct states at (2021-04-20 02:02:03)
Finished checking temporal properties in 09s at 2021-04-20 02:02:12
Progress(20) at 2021-04-20 02:02:12: 5,120,006 states generated (1,041,409 s/min), 426,809 distinct states found (71,489 ds/min), 131,521 states left on queue.
Checking 27 branches of temporal properties for the current state space with 13312844 total distinct states at (2021-04-20 02:03:14)
Finished checking temporal properties in 07s at 2021-04-20 02:03:22
Progress(21) at 2021-04-20 02:03:22: 6,164,267 states generated (1,044,261 s/min), 498,420 distinct states found (71,611 ds/min), 144,487 states left on queue.
Checking 27 branches of temporal properties for the current state space with 15135531 total distinct states at (2021-04-20 02:04:25)
Finished checking temporal properties in 08s at 2021-04-20 02:04:34
Progress(21) at 2021-04-20 02:04:34: 7,203,138 states generated (1,038,871 s/min), 566,343 distinct states found (67,923 ds/min), 155,729 states left on queue.
Checking 27 branches of temporal properties for the current state space with 16849467 total distinct states at (2021-04-20 02:05:35)
Finished checking temporal properties in 10s at 2021-04-20 02:05:46
Progress(22) at 2021-04-20 02:05:46: 8,241,728 states generated (1,038,590 s/min), 630,044 distinct states found (63,701 ds/min), 161,720 states left on queue.
Checking 27 branches of temporal properties for the current state space with 18684036 total distinct states at (2021-04-20 02:06:48)
Finished checking temporal properties in 11s at 2021-04-20 02:07:00
Progress(22) at 2021-04-20 02:07:00: 9,329,184 states generated (1,087,456 s/min), 698,326 distinct states found (68,282 ds/min), 170,765 states left on queue.
Checking 27 branches of temporal properties for the current state space with 20357770 total distinct states at (2021-04-20 02:08:02)
Finished checking temporal properties in 12s at 2021-04-20 02:08:15
Progress(22) at 2021-04-20 02:08:15: 10,400,211 states generated (1,071,027 s/min), 760,469 distinct states found (62,143 ds/min), 174,892 states left on queue.
Progress(23) at 2021-04-20 02:09:15: 11,472,542 states generated (1,072,331 s/min), 822,685 distinct states found (62,216 ds/min), 178,161 states left on queue.
Checking 27 branches of temporal properties for the current state space with 23663685 total distinct states at (2021-04-20 02:10:17)
Finished checking temporal properties in 17s at 2021-04-20 02:10:34
Progress(23) at 2021-04-20 02:10:34: 12,521,829 states generated (1,049,287 s/min), 883,177 distinct states found (60,492 ds/min), 182,089 states left on queue.
Progress(23) at 2021-04-20 02:11:34: 13,584,373 states generated (1,062,544 s/min), 940,142 distinct states found (56,965 ds/min), 182,061 states left on queue.
Checking 27 branches of temporal properties for the current state space with 26720509 total distinct states at (2021-04-20 02:12:36)
Finished checking temporal properties in 18s at 2021-04-20 02:12:55
Progress(24) at 2021-04-20 02:12:55: 14,630,521 states generated (1,046,148 s/min), 996,375 distinct states found (56,233 ds/min), 181,615 states left on queue.
Progress(24) at 2021-04-20 02:13:55: 15,727,646 states generated (1,097,125 s/min), 1,053,512 distinct states found (57,137 ds/min), 179,701 states left on queue.
Checking 27 branches of temporal properties for the current state space with 29771150 total distinct states at (2021-04-20 02:14:57)
Finished checking temporal properties in 22s at 2021-04-20 02:15:19
Progress(24) at 2021-04-20 02:15:19: 16,788,308 states generated (1,060,662 s/min), 1,109,265 distinct states found (55,753 ds/min), 179,004 states left on queue.
Progress(25) at 2021-04-20 02:16:19: 17,905,801 states generated (1,117,493 s/min), 1,163,281 distinct states found (54,016 ds/min), 172,956 states left on queue.
Checking 27 branches of temporal properties for the current state space with 32622725 total distinct states at (2021-04-20 02:17:21)
Finished checking temporal properties in 24s at 2021-04-20 02:17:45
Progress(25) at 2021-04-20 02:17:45: 18,985,539 states generated (1,079,738 s/min), 1,214,410 distinct states found (51,129 ds/min), 166,344 states left on queue.
Progress(25) at 2021-04-20 02:18:45: 20,104,899 states generated (1,119,360 s/min), 1,269,982 distinct states found (55,572 ds/min), 162,730 states left on queue.
Checking 27 branches of temporal properties for the current state space with 35490556 total distinct states at (2021-04-20 02:19:48)
Finished checking temporal properties in 27s at 2021-04-20 02:20:15
Progress(26) at 2021-04-20 02:20:15: 21,196,009 states generated (1,091,110 s/min), 1,320,197 distinct states found (50,215 ds/min), 154,762 states left on queue.
Progress(26) at 2021-04-20 02:21:15: 22,328,419 states generated (1,132,410 s/min), 1,371,357 distinct states found (51,160 ds/min), 145,867 states left on queue.
Progress(26) at 2021-04-20 02:22:15: 23,431,172 states generated (1,102,753 s/min), 1,417,814 distinct states found (46,457 ds/min), 134,375 states left on queue.
Checking 27 branches of temporal properties for the current state space with 39548776 total distinct states at (2021-04-20 02:23:17)
Finished checking temporal properties in 32s at 2021-04-20 02:23:50
Progress(27) at 2021-04-20 02:23:50: 24,522,420 states generated (1,091,248 s/min), 1,469,515 distinct states found (51,701 ds/min), 128,128 states left on queue.
Progress(27) at 2021-04-20 02:24:50: 25,666,308 states generated (1,143,888 s/min), 1,518,116 distinct states found (48,601 ds/min), 116,536 states left on queue.
Progress(28) at 2021-04-20 02:25:50: 26,776,138 states generated (1,109,830 s/min), 1,565,359 distinct states found (47,243 ds/min), 105,636 states left on queue.
Checking 27 branches of temporal properties for the current state space with 43376934 total distinct states at (2021-04-20 02:26:52)
Finished checking temporal properties in 37s at 2021-04-20 02:27:30
Checkpointing of run states/21-04-20-01-56-03
Checkpointing completed at (2021-04-20 02:27:30)
Progress(28) at 2021-04-20 02:27:30: 27,893,709 states generated (1,117,571 s/min), 1,610,213 distinct states found (44,854 ds/min), 92,084 states left on queue.
Progress(29) at 2021-04-20 02:28:30: 29,019,948 states generated (1,126,239 s/min), 1,655,871 distinct states found (45,658 ds/min), 78,879 states left on queue.
Progress(29) at 2021-04-20 02:29:30: 30,176,107 states generated (1,156,159 s/min), 1,697,374 distinct states found (41,503 ds/min), 60,631 states left on queue.
Checking 27 branches of temporal properties for the current state space with 46806753 total distinct states at (2021-04-20 02:30:32)
Finished checking temporal properties in 39s at 2021-04-20 02:31:11
Progress(30) at 2021-04-20 02:31:11: 31,319,082 states generated (1,142,975 s/min), 1,735,024 distinct states found (37,650 ds/min), 38,894 states left on queue.
Progress(31) at 2021-04-20 02:32:11: 32,545,214 states generated (1,226,132 s/min), 1,767,673 distinct states found (32,649 ds/min), 8,034 states left on queue.
Progress(33) at 2021-04-20 02:32:24: 32,796,933 states generated, 1,771,900 distinct states found, 0 states left on queue.
Checking 27 branches of temporal properties for the complete state space with 47841300 total distinct states at (2021-04-20 02:32:24)
Finished checking temporal properties in 31s at 2021-04-20 02:32:55
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-6
based on the actual fingerprints: val = 2.4E-7
32796933 states generated, 1771900 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 33.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 14 and the 95th percentile is 4).
Finished in 36min 53s at (2021-04-20 02:32:57)