Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ java -version
- java version "9"
- Java(TM) SE Runtime Environment (build 9+181)
- Java HotSpot(TM) 64-Bit Server VM (build 9+181, mixed mode)
- markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ java --add-modules=java.activation -jar tla2tools.jar -workers 32
- TLC2 Version 2.10 of 28 September 2017 (rev: ${git.shortRevision})
- Running breadth-first search Model-Checking with 32 workers on 32 cores with 15096MB heap and 64MB offheap memory (Linux 4.4.0-1035-aws amd64, Oracle Corporation 9 x86_64).
- Starting SANY...
- Parsing file /tmp/MC.tla
- Parsing file /tmp/PaxosCommit.tla
- Parsing file /tmp/TLC.tla
- Parsing file /tmp/Integers.tla
- Parsing file /tmp/Naturals.tla
- Parsing file /tmp/TCommit.tla
- Parsing file /tmp/Sequences.tla
- Semantic processing of module Naturals
- Semantic processing of module Integers
- Semantic processing of module TCommit
- Semantic processing of module PaxosCommit
- Semantic processing of module Sequences
- Semantic processing of module TLC
- Semantic processing of module MC
- SANY finished.
- Starting... (2017-10-09 20:51:28)
- Computing initial states...
- Finished computing initial states: 1 distinct state generated.
- Progress(12) at 2017-10-09 20:51:32: 222924 states generated (222,924 s/min), 38262 distinct states found (38,262 ds/min), 22481 states left on queue.
- Progress(19) at 2017-10-09 20:52:32: 32499482 states generated (32,276,558 s/min), 3882765 distinct states found (3,844,503 ds/min), 1674798 states left on queue.
- Progress(20) at 2017-10-09 20:53:32: 64081112 states generated (31,581,630 s/min), 7183636 distinct states found (3,300,871 ds/min), 2875674 states left on queue.
- Progress(20) at 2017-10-09 20:54:32: 94576609 states generated (30,495,497 s/min), 10292383 distinct states found (3,108,747 ds/min), 3961873 states left on queue.
- Progress(20) at 2017-10-09 20:55:32: 125032114 states generated (30,455,505 s/min), 13334703 distinct states found (3,042,320 ds/min), 4993419 states left on queue.
- Progress(21) at 2017-10-09 20:56:32: 154754170 states generated (29,722,056 s/min), 16106323 distinct states found (2,771,620 ds/min), 5817747 states left on queue.
- Progress(22) at 2017-10-09 20:57:32: 184647843 states generated (29,893,673 s/min), 18987831 distinct states found (2,881,508 ds/min), 6726031 states left on queue.
- Progress(22) at 2017-10-09 20:58:32: 215230850 states generated (30,583,007 s/min), 21674189 distinct states found (2,686,358 ds/min), 7455894 states left on queue.
- Progress(22) at 2017-10-09 20:59:32: 244655646 states generated (29,424,796 s/min), 24357527 distinct states found (2,683,338 ds/min), 8197207 states left on queue.
- Progress(23) at 2017-10-09 21:00:32: 275301989 states generated (30,646,343 s/min), 27071616 distinct states found (2,714,089 ds/min), 8913940 states left on queue.
- Progress(23) at 2017-10-09 21:01:32: 305350519 states generated (30,048,530 s/min), 29880771 distinct states found (2,809,155 ds/min), 9766772 states left on queue.
- Progress(23) at 2017-10-09 21:02:32: 336679339 states generated (31,328,820 s/min), 32336138 distinct states found (2,455,367 ds/min), 10247608 states left on queue.
- Progress(23) at 2017-10-09 21:03:32: 366230948 states generated (29,551,609 s/min), 35012747 distinct states found (2,676,609 ds/min), 10982262 states left on queue.
- Progress(24) at 2017-10-09 21:04:32: 397780219 states generated (31,549,271 s/min), 37532080 distinct states found (2,519,333 ds/min), 11489726 states left on queue.
- Progress(24) at 2017-10-09 21:05:32: 428060428 states generated (30,280,209 s/min), 40288211 distinct states found (2,756,131 ds/min), 12218532 states left on queue.
- Progress(24) at 2017-10-09 21:06:32: 458744106 states generated (30,683,678 s/min), 42875544 distinct states found (2,587,333 ds/min), 12839475 states left on queue.
- Progress(24) at 2017-10-09 21:07:32: 490462258 states generated (31,718,152 s/min), 45206891 distinct states found (2,331,347 ds/min), 13213931 states left on queue.
- Progress(24) at 2017-10-09 21:08:32: 520153501 states generated (29,691,243 s/min), 47755579 distinct states found (2,548,688 ds/min), 13811267 states left on queue.
- Progress(25) at 2017-10-09 21:09:32: 550261280 states generated (30,107,779 s/min), 50194810 distinct states found (2,439,231 ds/min), 14300520 states left on queue.
- Progress(25) at 2017-10-09 21:10:32: 581958988 states generated (31,697,708 s/min), 52447745 distinct states found (2,252,935 ds/min), 14609436 states left on queue.
- Progress(25) at 2017-10-09 21:11:32: 611634798 states generated (29,675,810 s/min), 55107030 distinct states found (2,659,285 ds/min), 15249767 states left on queue.
- Progress(25) at 2017-10-09 21:12:32: 641601438 states generated (29,966,640 s/min), 57647469 distinct states found (2,540,439 ds/min), 15849309 states left on queue.
- Progress(25) at 2017-10-09 21:13:32: 672554824 states generated (30,953,386 s/min), 59836931 distinct states found (2,189,462 ds/min), 16141839 states left on queue.
- Progress(25) at 2017-10-09 21:14:32: 703387423 states generated (30,832,599 s/min), 61962410 distinct states found (2,125,479 ds/min), 16372566 states left on queue.
- Progress(25) at 2017-10-09 21:15:32: 732533575 states generated (29,146,152 s/min), 64442516 distinct states found (2,480,106 ds/min), 16913062 states left on queue.
- Progress(25) at 2017-10-09 21:16:32: 761770440 states generated (29,236,865 s/min), 66739227 distinct states found (2,296,711 ds/min), 17372045 states left on queue.
- Progress(26) at 2017-10-09 21:17:32: 792629800 states generated (30,859,360 s/min), 68900974 distinct states found (2,161,747 ds/min), 17576964 states left on queue.
- Progress(26) at 2017-10-09 21:18:32: 823051225 states generated (30,421,425 s/min), 71054591 distinct states found (2,153,617 ds/min), 17823001 states left on queue.
- Progress(26) at 2017-10-09 21:19:32: 851808370 states generated (28,757,145 s/min), 73452176 distinct states found (2,397,585 ds/min), 18288863 states left on queue.
- Progress(26) at 2017-10-09 21:20:32: 881243318 states generated (29,434,948 s/min), 75790835 distinct states found (2,338,659 ds/min), 18707133 states left on queue.
- Progress(26) at 2017-10-09 21:21:32: 910823636 states generated (29,580,318 s/min), 77943829 distinct states found (2,152,994 ds/min), 19041534 states left on queue.
- Progress(26) at 2017-10-09 21:22:32: 941548492 states generated (30,724,856 s/min), 79789749 distinct states found (1,845,920 ds/min), 19057069 states left on queue.
- Progress(26) at 2017-10-09 21:23:32: 971228926 states generated (29,680,434 s/min), 81757903 distinct states found (1,968,154 ds/min), 19196588 states left on queue.
- Progress(26) at 2017-10-09 21:24:32: 998966394 states generated (27,737,468 s/min), 84215051 distinct states found (2,457,148 ds/min), 19765832 states left on queue.
- Progress(26) at 2017-10-09 21:25:32: 1027173189 states generated (28,206,795 s/min), 86469361 distinct states found (2,254,310 ds/min), 20266349 states left on queue.
- Progress(27) at 2017-10-09 21:26:32: 1056346003 states generated (29,172,814 s/min), 88282497 distinct states found (1,813,136 ds/min), 20263830 states left on queue.
- Progress(27) at 2017-10-09 21:27:32: 1086459000 states generated (30,112,997 s/min), 90196170 distinct states found (1,913,673 ds/min), 20389087 states left on queue.
- Progress(27) at 2017-10-09 21:28:32: 1115088307 states generated (28,629,307 s/min), 92228767 distinct states found (2,032,597 ds/min), 20519374 states left on queue.
- Progress(27) at 2017-10-09 21:29:32: 1142987972 states generated (27,899,665 s/min), 94362853 distinct states found (2,134,086 ds/min), 20803883 states left on queue.
- Progress(27) at 2017-10-09 21:30:32: 1171389427 states generated (28,401,455 s/min), 96486433 distinct states found (2,123,580 ds/min), 21081557 states left on queue.
- Progress(27) at 2017-10-09 21:31:32: 1199574528 states generated (28,185,101 s/min), 98487520 distinct states found (2,001,087 ds/min), 21362465 states left on queue.
- Progress(27) at 2017-10-09 21:32:32: 1228783458 states generated (29,208,930 s/min), 100241124 distinct states found (1,753,604 ds/min), 21359475 states left on queue.
- Progress(27) at 2017-10-09 21:33:32: 1258203261 states generated (29,419,803 s/min), 101988321 distinct states found (1,747,197 ds/min), 21349833 states left on queue.
- Progress(27) at 2017-10-09 21:34:32: 1286252632 states generated (28,049,371 s/min), 103895552 distinct states found (1,907,231 ds/min), 21462495 states left on queue.
- Progress(27) at 2017-10-09 21:35:32: 1312736841 states generated (26,484,209 s/min), 106091881 distinct states found (2,196,329 ds/min), 21881860 states left on queue.
- Progress(27) at 2017-10-09 21:36:32: 1339610564 states generated (26,873,723 s/min), 108135115 distinct states found (2,043,234 ds/min), 22237703 states left on queue.
- Progress(28) at 2017-10-09 21:37:32: 1367247092 states generated (27,636,528 s/min), 109716892 distinct states found (1,581,777 ds/min), 22226504 states left on queue.
- Progress(28) at 2017-10-09 21:38:32: 1397215080 states generated (29,967,988 s/min), 111473447 distinct states found (1,756,555 ds/min), 22150016 states left on queue.
- Progress(28) at 2017-10-09 21:39:32: 1426157512 states generated (28,942,432 s/min), 113283317 distinct states found (1,809,870 ds/min), 22198170 states left on queue.
- Progress(28) at 2017-10-09 21:40:32: 1454064068 states generated (27,906,556 s/min), 115206524 distinct states found (1,923,207 ds/min), 22243421 states left on queue.
- Progress(28) at 2017-10-09 21:41:32: 1481635101 states generated (27,571,033 s/min), 117127602 distinct states found (1,921,078 ds/min), 22370034 states left on queue.
- Progress(28) at 2017-10-09 21:42:32: 1509032485 states generated (27,397,384 s/min), 119053395 distinct states found (1,925,793 ds/min), 22529056 states left on queue.
- Progress(28) at 2017-10-09 21:43:32: 1536939107 states generated (27,906,622 s/min), 120897247 distinct states found (1,843,852 ds/min), 22684397 states left on queue.
- Progress(28) at 2017-10-09 21:44:32: 1565365634 states generated (28,426,527 s/min), 122579844 distinct states found (1,682,597 ds/min), 22651502 states left on queue.
- Progress(28) at 2017-10-09 21:45:32: 1594878213 states generated (29,512,579 s/min), 124140371 distinct states found (1,560,527 ds/min), 22495333 states left on queue.
- Progress(28) at 2017-10-09 21:46:32: 1622445308 states generated (27,567,095 s/min), 125827793 distinct states found (1,687,422 ds/min), 22461598 states left on queue.
- Progress(28) at 2017-10-09 21:47:32: 1649332970 states generated (26,887,662 s/min), 127861908 distinct states found (2,034,115 ds/min), 22690661 states left on queue.
- Progress(28) at 2017-10-09 21:48:32: 1675949793 states generated (26,616,823 s/min), 129811687 distinct states found (1,949,779 ds/min), 22945399 states left on queue.
- Progress(28) at 2017-10-09 21:49:32: 1702636088 states generated (26,686,295 s/min), 131649046 distinct states found (1,837,359 ds/min), 23169689 states left on queue.
- Progress(29) at 2017-10-09 21:50:32: 1730426645 states generated (27,790,557 s/min), 133052372 distinct states found (1,403,326 ds/min), 23008155 states left on queue.
- Progress(29) at 2017-10-09 21:51:32: 1754062280 states generated (23,635,635 s/min), 134283826 distinct states found (1,231,454 ds/min), 22837570 states left on queue.
- Progress(29) at 2017-10-09 21:52:32: 1782548810 states generated (28,486,530 s/min), 135909040 distinct states found (1,625,214 ds/min), 22769444 states left on queue.
- Progress(29) at 2017-10-09 21:53:32: 1810288488 states generated (27,739,678 s/min), 137648169 distinct states found (1,739,129 ds/min), 22645163 states left on queue.
- Progress(29) at 2017-10-09 21:54:32: 1837544497 states generated (27,256,009 s/min), 139399984 distinct states found (1,751,815 ds/min), 22624355 states left on queue.
- Progress(29) at 2017-10-09 21:55:32: 1865025419 states generated (27,480,922 s/min), 141113604 distinct states found (1,713,620 ds/min), 22585811 states left on queue.
- Progress(29) at 2017-10-09 21:56:32: 1892272261 states generated (27,246,842 s/min), 142862671 distinct states found (1,749,067 ds/min), 22643924 states left on queue.
- Progress(29) at 2017-10-09 21:57:32: 1919652067 states generated (27,379,806 s/min), 144526140 distinct states found (1,663,469 ds/min), 22659363 states left on queue.
- Progress(29) at 2017-10-09 21:58:32: 1948562216 states generated (28,910,149 s/min), 145881108 distinct states found (1,354,968 ds/min), 22376138 states left on queue.
- Progress(29) at 2017-10-09 21:59:32: 1976617189 states generated (28,054,973 s/min), 147403227 distinct states found (1,522,119 ds/min), 22217641 states left on queue.
- Progress(29) at 2017-10-09 22:00:32: 2003444115 states generated (26,826,926 s/min), 149147324 distinct states found (1,744,097 ds/min), 22181788 states left on queue.
- Progress(29) at 2017-10-09 22:01:32: 2030039199 states generated (26,595,084 s/min), 151061646 distinct states found (1,914,322 ds/min), 22345697 states left on queue.
- Progress(29) at 2017-10-09 22:02:32: 2056885129 states generated (26,845,930 s/min), 152806993 distinct states found (1,745,347 ds/min), 22444983 states left on queue.
- Progress(29) at 2017-10-09 22:03:32: 2084079791 states generated (27,194,662 s/min), 154485135 distinct states found (1,678,142 ds/min), 22585012 states left on queue.
- Progress(30) at 2017-10-09 22:04:32: 2112352854 states generated (28,273,063 s/min), 155734873 distinct states found (1,249,738 ds/min), 22273772 states left on queue.
- Progress(30) at 2017-10-09 22:05:32: 2141283048 states generated (28,930,194 s/min), 157147215 distinct states found (1,412,342 ds/min), 22038736 states left on queue.
- Progress(30) at 2017-10-09 22:06:32: 2169187429 states generated (27,904,381 s/min), 158601329 distinct states found (1,454,114 ds/min), 21720676 states left on queue.
- Progress(30) at 2017-10-09 22:07:32: 2196794742 states generated (27,607,313 s/min), 160198158 distinct states found (1,596,829 ds/min), 21486377 states left on queue.
- Progress(30) at 2017-10-09 22:08:32: 2223691555 states generated (26,896,813 s/min), 161730262 distinct states found (1,532,104 ds/min), 21326700 states left on queue.
- Progress(30) at 2017-10-09 22:09:32: 2250451384 states generated (26,759,829 s/min), 163345418 distinct states found (1,615,156 ds/min), 21228580 states left on queue.
- Progress(30) at 2017-10-09 22:10:32: 2277812977 states generated (27,361,593 s/min), 164874742 distinct states found (1,529,324 ds/min), 21160179 states left on queue.
- Progress(30) at 2017-10-09 22:11:32: 2305329774 states generated (27,516,797 s/min), 166251104 distinct states found (1,376,362 ds/min), 20914737 states left on queue.
- Progress(30) at 2017-10-09 22:12:32: 2333543725 states generated (28,213,951 s/min), 167558497 distinct states found (1,307,393 ds/min), 20581921 states left on queue.
- Progress(30) at 2017-10-09 22:13:32: 2360280133 states generated (26,736,408 s/min), 169069045 distinct states found (1,510,548 ds/min), 20367729 states left on queue.
- Progress(30) at 2017-10-09 22:14:32: 2386541946 states generated (26,261,813 s/min), 170745566 distinct states found (1,676,521 ds/min), 20329181 states left on queue.
- Progress(30) at 2017-10-09 22:15:32: 2412448742 states generated (25,906,796 s/min), 172323289 distinct states found (1,577,723 ds/min), 20324634 states left on queue.
- Progress(30) at 2017-10-09 22:16:32: 2438515253 states generated (26,066,511 s/min), 173901305 distinct states found (1,578,016 ds/min), 20352624 states left on queue.
- Progress(30) at 2017-10-09 22:17:32: 2465835025 states generated (27,319,772 s/min), 175289689 distinct states found (1,388,384 ds/min), 20382152 states left on queue.
- Progress(31) at 2017-10-09 22:18:32: 2493534438 states generated (27,699,413 s/min), 176303743 distinct states found (1,014,054 ds/min), 19834369 states left on queue.
- Progress(31) at 2017-10-09 22:19:32: 2520679645 states generated (27,145,207 s/min), 177534679 distinct states found (1,230,936 ds/min), 19491884 states left on queue.
- Progress(31) at 2017-10-09 22:20:32: 2547628771 states generated (26,949,126 s/min), 178886087 distinct states found (1,351,408 ds/min), 19060472 states left on queue.
- Progress(31) at 2017-10-09 22:21:32: 2573994595 states generated (26,365,824 s/min), 180202942 distinct states found (1,316,855 ds/min), 18711791 states left on queue.
- Progress(31) at 2017-10-09 22:22:32: 2599967305 states generated (25,972,710 s/min), 181608964 distinct states found (1,406,022 ds/min), 18486335 states left on queue.
- Progress(31) at 2017-10-09 22:23:32: 2626496156 states generated (26,528,851 s/min), 182927110 distinct states found (1,318,146 ds/min), 18249873 states left on queue.
- Progress(31) at 2017-10-09 22:24:32: 2653106641 states generated (26,610,485 s/min), 184207111 distinct states found (1,280,001 ds/min), 17973324 states left on queue.
- Progress(31) at 2017-10-09 22:25:32: 2680178391 states generated (27,071,750 s/min), 185348798 distinct states found (1,141,687 ds/min), 17537560 states left on queue.
- Progress(31) at 2017-10-09 22:26:32: 2706248961 states generated (26,070,570 s/min), 186657048 distinct states found (1,308,250 ds/min), 17170600 states left on queue.
- Progress(31) at 2017-10-09 22:27:32: 2732008717 states generated (25,759,756 s/min), 188140203 distinct states found (1,483,155 ds/min), 17007902 states left on queue.
- Progress(31) at 2017-10-09 22:28:32: 2758045160 states generated (26,036,443 s/min), 189511274 distinct states found (1,371,071 ds/min), 16850699 states left on queue.
- Progress(31) at 2017-10-09 22:29:32: 2783766889 states generated (25,721,729 s/min), 190890977 distinct states found (1,379,703 ds/min), 16769445 states left on queue.
- Progress(32) at 2017-10-09 22:30:32: 2810679212 states generated (26,912,323 s/min), 192080822 distinct states found (1,189,845 ds/min), 16708872 states left on queue.
- Progress(32) at 2017-10-09 22:31:32: 2837761707 states generated (27,082,495 s/min), 193025367 distinct states found (944,545 ds/min), 16159697 states left on queue.
- Progress(32) at 2017-10-09 22:32:32: 2864437117 states generated (26,675,410 s/min), 194113780 distinct states found (1,088,413 ds/min), 15572780 states left on queue.
- Progress(32) at 2017-10-09 22:33:32: 2890971780 states generated (26,534,663 s/min), 195260476 distinct states found (1,146,696 ds/min), 15045382 states left on queue.
- Progress(32) at 2017-10-09 22:34:32: 2917338456 states generated (26,366,676 s/min), 196506474 distinct states found (1,245,998 ds/min), 14653331 states left on queue.
- Progress(32) at 2017-10-09 22:35:32: 2944215720 states generated (26,877,264 s/min), 197700671 distinct states found (1,194,197 ds/min), 14295411 states left on queue.
- Progress(32) at 2017-10-09 22:36:32: 2971079502 states generated (26,863,782 s/min), 198728006 distinct states found (1,027,335 ds/min), 13783924 states left on queue.
- Progress(32) at 2017-10-09 22:37:32: 2997283497 states generated (26,203,995 s/min), 199842252 distinct states found (1,114,246 ds/min), 13255799 states left on queue.
- Progress(32) at 2017-10-09 22:38:32: 3023644295 states generated (26,360,798 s/min), 201133679 distinct states found (1,291,427 ds/min), 12908056 states left on queue.
- Progress(32) at 2017-10-09 22:39:32: 3050221913 states generated (26,577,618 s/min), 202355418 distinct states found (1,221,739 ds/min), 12625206 states left on queue.
- Progress(32) at 2017-10-09 22:40:32: 3076186712 states generated (25,964,799 s/min), 203530735 distinct states found (1,175,317 ds/min), 12408289 states left on queue.
- Progress(33) at 2017-10-09 22:41:32: 3102220131 states generated (26,033,419 s/min), 204522912 distinct states found (992,177 ds/min), 12215810 states left on queue.
- Progress(33) at 2017-10-09 22:42:32: 3128312462 states generated (26,092,331 s/min), 205340688 distinct states found (817,776 ds/min), 11579241 states left on queue.
- Progress(33) at 2017-10-09 22:43:32: 3154321991 states generated (26,009,529 s/min), 206284425 distinct states found (943,737 ds/min), 10893835 states left on queue.
- Progress(33) at 2017-10-09 22:44:32: 3180572074 states generated (26,250,083 s/min), 207315976 distinct states found (1,031,551 ds/min), 10341036 states left on queue.
- Progress(33) at 2017-10-09 22:45:32: 3206974416 states generated (26,402,342 s/min), 208317572 distinct states found (1,001,596 ds/min), 9852413 states left on queue.
- Progress(33) at 2017-10-09 22:46:32: 3232257298 states generated (25,282,882 s/min), 209199151 distinct states found (881,579 ds/min), 9168757 states left on queue.
- Progress(33) at 2017-10-09 22:47:32: 3258235396 states generated (25,978,098 s/min), 210256345 distinct states found (1,057,194 ds/min), 8685955 states left on queue.
- Progress(33) at 2017-10-09 22:48:32: 3284212888 states generated (25,977,492 s/min), 211299041 distinct states found (1,042,696 ds/min), 8300206 states left on queue.
- Progress(33) at 2017-10-09 22:49:32: 3310498157 states generated (26,285,269 s/min), 212237024 distinct states found (937,983 ds/min), 8065475 states left on queue.
- Progress(34) at 2017-10-09 22:50:32: 3335750632 states generated (25,252,475 s/min), 212914440 distinct states found (677,416 ds/min), 7490801 states left on queue.
- Progress(34) at 2017-10-09 22:51:32: 3360689381 states generated (24,938,749 s/min), 213720248 distinct states found (805,808 ds/min), 6763203 states left on queue.
- Progress(34) at 2017-10-09 22:52:32: 3385986414 states generated (25,297,033 s/min), 214522694 distinct states found (802,446 ds/min), 6143439 states left on queue.
- Progress(34) at 2017-10-09 22:53:32: 3410648071 states generated (24,661,657 s/min), 215288045 distinct states found (765,351 ds/min), 5425476 states left on queue.
- Progress(34) at 2017-10-09 22:54:32: 3435898186 states generated (25,250,115 s/min), 216105238 distinct states found (817,193 ds/min), 4897657 states left on queue.
- Progress(34) at 2017-10-09 22:55:32: 3461932720 states generated (26,034,534 s/min), 216872384 distinct states found (767,146 ds/min), 4578047 states left on queue.
- Progress(35) at 2017-10-09 22:56:32: 3485951990 states generated (24,019,270 s/min), 217429814 distinct states found (557,430 ds/min), 3881754 states left on queue.
- Progress(35) at 2017-10-09 22:57:32: 3510081316 states generated (24,129,326 s/min), 218065952 distinct states found (636,138 ds/min), 3138978 states left on queue.
- Progress(35) at 2017-10-09 22:58:32: 3534534555 states generated (24,453,239 s/min), 218692812 distinct states found (626,860 ds/min), 2505916 states left on queue.
- Progress(36) at 2017-10-09 22:59:32: 3558971347 states generated (24,436,792 s/min), 219222486 distinct states found (529,674 ds/min), 2122019 states left on queue.
- Progress(36) at 2017-10-09 23:00:32: 3581319581 states generated (22,348,234 s/min), 219683240 distinct states found (460,754 ds/min), 1338361 states left on queue.
- Progress(37) at 2017-10-09 23:01:32: 3605399279 states generated (24,079,698 s/min), 220106287 distinct states found (423,047 ds/min), 857134 states left on queue.
- Progress(38) at 2017-10-09 23:02:32: 3626964273 states generated (21,564,994 s/min), 220413298 distinct states found (307,011 ds/min), 269470 states left on queue.
- 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 = .041
- based on the actual fingerprints: val = .0083
- Progress(44) at 2017-10-09 23:03:28: 3638478200 states generated (27,565,043 s/min), 220515772 distinct states found (1,670,623 ds/min), 0 states left on queue.
- 3638478200 states generated, 220515772 distinct states found, 0 states left on queue.
- The depth of the complete state graph search is 44.
- The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 15 and the 95th percentile is 3).
- Finished in 7920823ms at (2017-10-09 23:03:29)
- markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ /mnt/markus/ibm-java-x86_64-80/bin/java -version
- java version "1.8.0"
- Java(TM) SE Runtime Environment (build pxa6480sr3fp12-20160919_01(SR3 FP12))
- IBM J9 VM (build 2.8, JRE 1.8.0 Linux amd64-64 Compressed References 20160915_318796 (JIT enabled, AOT enabled)
- J9VM - R28_Java8_SR3_20160915_0912_B318796
- JIT - tr.r14.java.green_20160818_122998
- GC - R28_Java8_SR3_20160915_0912_B318796_CMPRSS
- J9CL - 20160915_318796)
- JCL - 20160914_01 based on Oracle jdk8u101-b13
- markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ /mnt/markus/ibm-java-x86_64-80/bin/java -jar tla2tools.jar -workers 32
- TLC2 Version 2.10 of 28 September 2017 (rev: ${git.shortRevision})
- Running breadth-first search Model-Checking with 32 workers on 32 cores with 512MB heap and 64MB offheap memory (Linux 4.4.0-1035-aws amd64, IBM Corporation 1.8.0 x86_64).
- Starting SANY...
- Parsing file /tmp/MC.tla
- Parsing file /tmp/PaxosCommit.tla
- Parsing file /tmp/TLC.tla
- Parsing file /tmp/Integers.tla
- Parsing file /tmp/Naturals.tla
- Parsing file /tmp/TCommit.tla
- Parsing file /tmp/Sequences.tla
- Semantic processing of module Naturals
- Semantic processing of module Integers
- Semantic processing of module TCommit
- Semantic processing of module PaxosCommit
- Semantic processing of module Sequences
- Semantic processing of module TLC
- Semantic processing of module MC
- SANY finished.
- Starting... (2017-10-10 06:07:52)
- Computing initial states...
- Finished computing initial states: 1 distinct state generated.
- Progress(11) at 2017-10-10 06:07:55: 537257 states generated (537,257 s/min), 87751 distinct states found (87,751 ds/min), 49997 states left on queue.
- Progress(18) at 2017-10-10 06:08:55: 17634119 states generated (17,096,862 s/min), 2205328 distinct states found (2,117,577 ds/min), 997102 states left on queue.
- Progress(19) at 2017-10-10 06:09:55: 36460614 states generated (18,826,495 s/min), 4395374 distinct states found (2,190,046 ds/min), 1910551 states left on queue.
- Progress(19) at 2017-10-10 06:10:55: 53426649 states generated (16,966,035 s/min), 6153129 distinct states found (1,757,755 ds/min), 2541831 states left on queue.
- Progress(20) at 2017-10-10 06:11:55: 69439773 states generated (16,013,124 s/min), 7972030 distinct states found (1,818,901 ds/min), 3274999 states left on queue.
- Progress(20) at 2017-10-10 06:12:55: 86740132 states generated (17,300,359 s/min), 9588907 distinct states found (1,616,877 ds/min), 3768091 states left on queue.
- Progress(21) at 2017-10-10 06:13:55: 103069021 states generated (16,328,889 s/min), 11262509 distinct states found (1,673,602 ds/min), 4341610 states left on queue.
- Progress(21) at 2017-10-10 06:14:55: 118417672 states generated (15,348,651 s/min), 12951442 distinct states found (1,688,933 ds/min), 4994297 states left on queue.
- Progress(21) at 2017-10-10 06:15:55: 135919141 states generated (17,501,469 s/min), 14473302 distinct states found (1,521,860 ds/min), 5390821 states left on queue.
- Progress(21) at 2017-10-10 06:16:55: 152510608 states generated (16,591,467 s/min), 15961419 distinct states found (1,488,117 ds/min), 5805858 states left on queue.
- Progress(22) at 2017-10-10 06:17:55: 168129341 states generated (15,618,733 s/min), 17521302 distinct states found (1,559,883 ds/min), 6312179 states left on queue.
- Progress(22) at 2017-10-10 06:18:55: 183174877 states generated (15,045,536 s/min), 19154997 distinct states found (1,633,695 ds/min), 6929618 states left on queue.
- Progress(22) at 2017-10-10 06:19:55: 199549150 states generated (16,374,273 s/min), 20707920 distinct states found (1,552,923 ds/min), 7410920 states left on queue.
- Progress(22) at 2017-10-10 06:20:55: 216140055 states generated (16,590,905 s/min), 22028408 distinct states found (1,320,488 ds/min), 7684208 states left on queue.
- Progress(22) at 2017-10-10 06:21:55: 232755559 states generated (16,615,504 s/min), 23375511 distinct states found (1,347,103 ds/min), 7966961 states left on queue.
- Progress(23) at 2017-10-10 06:22:55: 248835390 states generated (16,079,831 s/min), 24779530 distinct states found (1,404,019 ds/min), 8335225 states left on queue.
- Progress(23) at 2017-10-10 06:23:55: 264069444 states generated (15,234,054 s/min), 26304115 distinct states found (1,524,585 ds/min), 8817874 states left on queue.
- Progress(23) at 2017-10-10 06:24:55: 279030033 states generated (14,960,589 s/min), 27902425 distinct states found (1,598,310 ds/min), 9399781 states left on queue.
- Progress(23) at 2017-10-10 06:25:55: 294840588 states generated (15,810,555 s/min), 29344340 distinct states found (1,441,915 ds/min), 9800636 states left on queue.
- Progress(23) at 2017-10-10 06:26:55: 310833817 states generated (15,993,229 s/min), 30807922 distinct states found (1,463,582 ds/min), 10227991 states left on queue.
- Progress(23) at 2017-10-10 06:27:55: 327824946 states generated (16,991,129 s/min), 32133647 distinct states found (1,325,725 ds/min), 10499241 states left on queue.
- Progress(23) at 2017-10-10 06:28:55: 344520828 states generated (16,695,882 s/min), 33370428 distinct states found (1,236,781 ds/min), 10671302 states left on queue.
- Progress(23) at 2017-10-10 06:29:55: 360557958 states generated (16,037,130 s/min), 34593793 distinct states found (1,223,365 ds/min), 10888935 states left on queue.
- Progress(24) at 2017-10-10 06:30:55: 376837367 states generated (16,279,409 s/min), 35924945 distinct states found (1,331,152 ds/min), 11187119 states left on queue.
- Progress(24) at 2017-10-10 06:31:55: 392426691 states generated (15,589,324 s/min), 37428442 distinct states found (1,503,497 ds/min), 11615014 states left on queue.
- Progress(24) at 2017-10-10 06:32:55: 407275827 states generated (14,849,136 s/min), 38870712 distinct states found (1,442,270 ds/min), 12052288 states left on queue.
- Progress(24) at 2017-10-10 06:33:55: 422442880 states generated (15,167,053 s/min), 40359429 distinct states found (1,488,717 ds/min), 12531554 states left on queue.
- Progress(24) at 2017-10-10 06:34:55: 438051903 states generated (15,609,023 s/min), 41751868 distinct states found (1,392,439 ds/min), 12910050 states left on queue.
- Progress(24) at 2017-10-10 06:35:55: 453672424 states generated (15,620,521 s/min), 43078047 distinct states found (1,326,179 ds/min), 13193330 states left on queue.
- Progress(24) at 2017-10-10 06:36:55: 470726956 states generated (17,054,532 s/min), 44465012 distinct states found (1,386,965 ds/min), 13513933 states left on queue.
- Progress(24) at 2017-10-10 06:37:55: 487431834 states generated (16,704,878 s/min), 45738922 distinct states found (1,273,910 ds/min), 13780186 states left on queue.
- Progress(24) at 2017-10-10 06:38:55: 503705048 states generated (16,273,214 s/min), 46769609 distinct states found (1,030,687 ds/min), 13771309 states left on queue.
- Progress(24) at 2017-10-10 06:39:55: 520669431 states generated (16,964,383 s/min), 47953239 distinct states found (1,183,630 ds/min), 13941799 states left on queue.
- Progress(24) at 2017-10-10 06:40:55: 537009885 states generated (16,340,454 s/min), 49215896 distinct states found (1,262,657 ds/min), 14169409 states left on queue.
- Progress(25) at 2017-10-10 06:41:55: 552536301 states generated (15,526,416 s/min), 50413751 distinct states found (1,197,855 ds/min), 14368684 states left on queue.
- Progress(25) at 2017-10-10 06:42:55: 568304042 states generated (15,767,741 s/min), 51841516 distinct states found (1,427,765 ds/min), 14700623 states left on queue.
- Progress(25) at 2017-10-10 06:43:55: 584380713 states generated (16,076,671 s/min), 53224350 distinct states found (1,382,834 ds/min), 15020196 states left on queue.
- Progress(25) at 2017-10-10 06:44:55: 598517815 states generated (14,137,102 s/min), 54598850 distinct states found (1,374,500 ds/min), 15440554 states left on queue.
- Progress(25) at 2017-10-10 06:45:55: 613930905 states generated (15,413,090 s/min), 56004570 distinct states found (1,405,720 ds/min), 15837834 states left on queue.
- Progress(25) at 2017-10-10 06:46:55: 629435825 states generated (15,504,920 s/min), 57363102 distinct states found (1,358,532 ds/min), 16175219 states left on queue.
- Progress(25) at 2017-10-10 06:47:55: 645742928 states generated (16,307,103 s/min), 58610974 distinct states found (1,247,872 ds/min), 16385357 states left on queue.
- Progress(25) at 2017-10-10 06:48:55: 661260521 states generated (15,517,593 s/min), 59892382 distinct states found (1,281,408 ds/min), 16632773 states left on queue.
- Progress(25) at 2017-10-10 06:49:55: 678585597 states generated (17,325,076 s/min), 61193657 distinct states found (1,301,275 ds/min), 16869588 states left on queue.
- Progress(25) at 2017-10-10 06:50:55: 695381967 states generated (16,796,370 s/min), 62447803 distinct states found (1,254,146 ds/min), 17125325 states left on queue.
- Progress(25) at 2017-10-10 06:51:55: 711637036 states generated (16,255,069 s/min), 63400845 distinct states found (953,042 ds/min), 17089392 states left on queue.
- Progress(25) at 2017-10-10 06:52:55: 728502596 states generated (16,865,560 s/min), 64497017 distinct states found (1,096,172 ds/min), 17144420 states left on queue.
- Progress(25) at 2017-10-10 06:53:55: 745543773 states generated (17,041,177 s/min), 65596822 distinct states found (1,099,805 ds/min), 17217974 states left on queue.
- Progress(25) at 2017-10-10 06:54:55: 761779749 states generated (16,235,976 s/min), 66776481 distinct states found (1,179,659 ds/min), 17395911 states left on queue.
- Progress(26) at 2017-10-10 06:55:55: 777366263 states generated (15,586,514 s/min), 67900208 distinct states found (1,123,727 ds/min), 17512049 states left on queue.
- Progress(26) at 2017-10-10 06:56:55: 793256872 states generated (15,890,609 s/min), 69250928 distinct states found (1,350,720 ds/min), 17752716 states left on queue.
- Progress(26) at 2017-10-10 06:57:55: 809440184 states generated (16,183,312 s/min), 70557686 distinct states found (1,306,758 ds/min), 17993920 states left on queue.
- Progress(26) at 2017-10-10 06:58:55: 824012401 states generated (14,572,217 s/min), 71804582 distinct states found (1,246,896 ds/min), 18260364 states left on queue.
- Progress(26) at 2017-10-10 06:59:55: 839367573 states generated (15,355,172 s/min), 73167091 distinct states found (1,362,509 ds/min), 18612211 states left on queue.
- Progress(26) at 2017-10-10 07:00:55: 854984740 states generated (15,617,167 s/min), 74492469 distinct states found (1,325,378 ds/min), 18911978 states left on queue.
- Progress(26) at 2017-10-10 07:01:55: 869349847 states generated (14,365,107 s/min), 75679497 distinct states found (1,187,028 ds/min), 19190928 states left on queue.
- Progress(26) at 2017-10-10 07:02:55: 885160294 states generated (15,810,447 s/min), 76968639 distinct states found (1,289,142 ds/min), 19447292 states left on queue.
- Progress(26) at 2017-10-10 07:03:55: 901675787 states generated (16,515,493 s/min), 78127757 distinct states found (1,159,118 ds/min), 19574370 states left on queue.
- Progress(26) at 2017-10-10 07:04:55: 918396257 states generated (16,720,470 s/min), 79384787 distinct states found (1,257,030 ds/min), 19720547 states left on queue.
- Progress(26) at 2017-10-10 07:05:55: 934278060 states generated (15,881,803 s/min), 80516830 distinct states found (1,132,043 ds/min), 19873446 states left on queue.
- Progress(26) at 2017-10-10 07:06:55: 951501037 states generated (17,222,977 s/min), 81747756 distinct states found (1,230,926 ds/min), 20074569 states left on queue.
- Progress(26) at 2017-10-10 07:07:55: 968200053 states generated (16,699,016 s/min), 82917628 distinct states found (1,169,872 ds/min), 20259653 states left on queue.
- Progress(26) at 2017-10-10 07:08:55: 985699296 states generated (17,499,243 s/min), 83771682 distinct states found (854,054 ds/min), 20053447 states left on queue.
- Progress(26) at 2017-10-10 07:09:55: 1001501222 states generated (15,801,926 s/min), 84752279 distinct states found (980,597 ds/min), 20104945 states left on queue.
- Progress(26) at 2017-10-10 07:10:55: 1018660910 states generated (17,159,688 s/min), 85778977 distinct states found (1,026,698 ds/min), 20110788 states left on queue.
- Progress(26) at 2017-10-10 07:11:55: 1035065492 states generated (16,404,582 s/min), 86913087 distinct states found (1,134,110 ds/min), 20236932 states left on queue.
- Progress(27) at 2017-10-10 07:12:55: 1051982036 states generated (16,916,544 s/min), 88013815 distinct states found (1,100,728 ds/min), 20265230 states left on queue.
- Progress(27) at 2017-10-10 07:13:55: 1066768191 states generated (14,786,155 s/min), 89161894 distinct states found (1,148,079 ds/min), 20382817 states left on queue.
- Progress(27) at 2017-10-10 07:14:55: 1083056140 states generated (16,287,949 s/min), 90417171 distinct states found (1,255,277 ds/min), 20543168 states left on queue.
- Progress(27) at 2017-10-10 07:15:55: 1099488278 states generated (16,432,138 s/min), 91607303 distinct states found (1,190,132 ds/min), 20667996 states left on queue.
- Progress(27) at 2017-10-10 07:16:55: 1113523104 states generated (14,034,826 s/min), 92794810 distinct states found (1,187,507 ds/min), 20904124 states left on queue.
- Progress(27) at 2017-10-10 07:17:55: 1128996264 states generated (15,473,160 s/min), 94061084 distinct states found (1,266,274 ds/min), 21169078 states left on queue.
- Progress(27) at 2017-10-10 07:18:55: 1145079002 states generated (16,082,738 s/min), 95284591 distinct states found (1,223,507 ds/min), 21353196 states left on queue.
- Progress(27) at 2017-10-10 07:19:55: 1159801801 states generated (14,722,799 s/min), 96468461 distinct states found (1,183,870 ds/min), 21619975 states left on queue.
- Progress(27) at 2017-10-10 07:20:55: 1174723161 states generated (14,921,360 s/min), 97648998 distinct states found (1,180,537 ds/min), 21840247 states left on queue.
- Progress(27) at 2017-10-10 07:21:55: 1190806713 states generated (16,083,552 s/min), 98840446 distinct states found (1,191,448 ds/min), 21997282 states left on queue.
- Progress(27) at 2017-10-10 07:22:55: 1207357622 states generated (16,550,909 s/min), 99956465 distinct states found (1,116,019 ds/min), 22098147 states left on queue.
- Progress(27) at 2017-10-10 07:23:55: 1222533312 states generated (15,175,690 s/min), 100954540 distinct states found (998,075 ds/min), 22100242 states left on queue.
- Progress(27) at 2017-10-10 07:24:55: 1239814694 states generated (17,281,382 s/min), 102129242 distinct states found (1,174,702 ds/min), 22186183 states left on queue.
- Progress(27) at 2017-10-10 07:25:55: 1257254640 states generated (17,439,946 s/min), 103281163 distinct states found (1,151,921 ds/min), 22297033 states left on queue.
- Progress(27) at 2017-10-10 07:26:55: 1274114398 states generated (16,859,758 s/min), 104417494 distinct states found (1,136,331 ds/min), 22445410 states left on queue.
- Progress(27) at 2017-10-10 07:27:55: 1289366780 states generated (15,252,382 s/min), 105410366 distinct states found (992,872 ds/min), 22536884 states left on queue.
- Progress(27) at 2017-10-10 07:28:55: 1306973740 states generated (17,606,960 s/min), 106187266 distinct states found (776,900 ds/min), 22281612 states left on queue.
- Progress(27) at 2017-10-10 07:29:55: 1324371475 states generated (17,397,735 s/min), 107165581 distinct states found (978,315 ds/min), 22255856 states left on queue.
- Progress(27) at 2017-10-10 07:30:55: 1341476155 states generated (17,104,680 s/min), 108152817 distinct states found (987,236 ds/min), 22239132 states left on queue.
- Progress(27) at 2017-10-10 07:31:55: 1356274568 states generated (14,798,413 s/min), 109090870 distinct states found (938,053 ds/min), 22272208 states left on queue.
- Progress(28) at 2017-10-10 07:32:55: 1373233421 states generated (16,958,853 s/min), 110123468 distinct states found (1,032,598 ds/min), 22246189 states left on queue.
- Progress(28) at 2017-10-10 07:33:55: 1389617390 states generated (16,383,969 s/min), 111268114 distinct states found (1,144,646 ds/min), 22258417 states left on queue.
- Progress(28) at 2017-10-10 07:34:55: 1405993770 states generated (16,376,380 s/min), 112408175 distinct states found (1,140,061 ds/min), 22292614 states left on queue.
- Progress(28) at 2017-10-10 07:35:55: 1420632770 states generated (14,639,000 s/min), 113434496 distinct states found (1,026,321 ds/min), 22373176 states left on queue.
- Progress(28) at 2017-10-10 07:36:55: 1436876022 states generated (16,243,252 s/min), 114571895 distinct states found (1,137,399 ds/min), 22449380 states left on queue.
- Progress(28) at 2017-10-10 07:37:55: 1452382837 states generated (15,506,815 s/min), 115809411 distinct states found (1,237,516 ds/min), 22644775 states left on queue.
- Progress(28) at 2017-10-10 07:38:55: 1468233018 states generated (15,850,181 s/min), 116982294 distinct states found (1,172,883 ds/min), 22821287 states left on queue.
- Progress(28) at 2017-10-10 07:39:55: 1482529795 states generated (14,296,777 s/min), 117990976 distinct states found (1,008,682 ds/min), 22920224 states left on queue.
- Progress(28) at 2017-10-10 07:40:55: 1498345319 states generated (15,815,524 s/min), 119157363 distinct states found (1,166,387 ds/min), 23084280 states left on queue.
- Progress(28) at 2017-10-10 07:41:55: 1514193343 states generated (15,848,024 s/min), 120296826 distinct states found (1,139,463 ds/min), 23253365 states left on queue.
- Progress(28) at 2017-10-10 07:42:55: 1530096380 states generated (15,903,037 s/min), 121433028 distinct states found (1,136,202 ds/min), 23395869 states left on queue.
- Progress(28) at 2017-10-10 07:43:55: 1544643689 states generated (14,547,309 s/min), 122396859 distinct states found (963,831 ds/min), 23434991 states left on queue.
- Progress(28) at 2017-10-10 07:44:55: 1561336854 states generated (16,693,165 s/min), 123433563 distinct states found (1,036,704 ds/min), 23469510 states left on queue.
- Progress(28) at 2017-10-10 07:45:55: 1578384676 states generated (17,047,822 s/min), 124468970 distinct states found (1,035,407 ds/min), 23394049 states left on queue.
- Progress(28) at 2017-10-10 07:46:55: 1595817606 states generated (17,432,930 s/min), 125529285 distinct states found (1,060,315 ds/min), 23378544 states left on queue.
- Progress(28) at 2017-10-10 07:47:55: 1611023409 states generated (15,205,803 s/min), 126474598 distinct states found (945,313 ds/min), 23420887 states left on queue.
- Progress(28) at 2017-10-10 07:48:55: 1628344341 states generated (17,320,932 s/min), 127518119 distinct states found (1,043,521 ds/min), 23461616 states left on queue.
- Progress(28) at 2017-10-10 07:49:55: 1645269352 states generated (16,925,011 s/min), 128596017 distinct states found (1,077,898 ds/min), 23556547 states left on queue.
- Progress(28) at 2017-10-10 07:50:55: 1662499988 states generated (17,230,636 s/min), 129414659 distinct states found (818,642 ds/min), 23392976 states left on queue.
- Progress(28) at 2017-10-10 07:51:55: 1677752874 states generated (15,252,886 s/min), 130166243 distinct states found (751,584 ds/min), 23265796 states left on queue.
- Progress(28) at 2017-10-10 07:52:55: 1695124610 states generated (17,371,736 s/min), 131045495 distinct states found (879,252 ds/min), 23160422 states left on queue.
- Progress(28) at 2017-10-10 07:53:55: 1711781331 states generated (16,656,721 s/min), 132037517 distinct states found (992,022 ds/min), 23148738 states left on queue.
- Progress(29) at 2017-10-10 07:54:55: 1728759921 states generated (16,978,590 s/min), 132989652 distinct states found (952,135 ds/min), 23054712 states left on queue.
- Progress(29) at 2017-10-10 07:55:55: 1745260870 states generated (16,500,949 s/min), 133998781 distinct states found (1,009,129 ds/min), 22937299 states left on queue.
- Progress(29) at 2017-10-10 07:56:55: 1759604977 states generated (14,344,107 s/min), 134943551 distinct states found (944,770 ds/min), 22908136 states left on queue.
- Progress(29) at 2017-10-10 07:57:55: 1776171365 states generated (16,566,388 s/min), 135990077 distinct states found (1,046,526 ds/min), 22879011 states left on queue.
- Progress(29) at 2017-10-10 07:58:55: 1792716478 states generated (16,545,113 s/min), 136996457 distinct states found (1,006,380 ds/min), 22829018 states left on queue.
- Progress(29) at 2017-10-10 07:59:55: 1808385834 states generated (15,669,356 s/min), 138131198 distinct states found (1,134,741 ds/min), 22918119 states left on queue.
- Progress(29) at 2017-10-10 08:00:55: 1821998778 states generated (13,612,944 s/min), 139082001 distinct states found (950,803 ds/min), 22986025 states left on queue.
- Progress(29) at 2017-10-10 08:01:55: 1838090287 states generated (16,091,509 s/min), 140165706 distinct states found (1,083,705 ds/min), 23084788 states left on queue.
- Progress(29) at 2017-10-10 08:02:55: 1854388781 states generated (16,298,494 s/min), 141214288 distinct states found (1,048,582 ds/min), 23105692 states left on queue.
- Progress(29) at 2017-10-10 08:03:55: 1870177476 states generated (15,788,695 s/min), 142303207 distinct states found (1,088,919 ds/min), 23207796 states left on queue.
- Progress(29) at 2017-10-10 08:04:55: 1884339488 states generated (14,162,012 s/min), 143175786 distinct states found (872,579 ds/min), 23279442 states left on queue.
- Progress(29) at 2017-10-10 08:05:55: 1900196290 states generated (15,856,802 s/min), 144235494 distinct states found (1,059,708 ds/min), 23342446 states left on queue.
- Progress(29) at 2017-10-10 08:06:55: 1916386856 states generated (16,190,566 s/min), 145287714 distinct states found (1,052,220 ds/min), 23384456 states left on queue.
- Progress(29) at 2017-10-10 08:07:55: 1933005540 states generated (16,618,684 s/min), 146270763 distinct states found (983,049 ds/min), 23354388 states left on queue.
- Progress(29) at 2017-10-10 08:08:55: 1947252336 states generated (14,246,796 s/min), 147063240 distinct states found (792,477 ds/min), 23306474 states left on queue.
- Progress(29) at 2017-10-10 08:09:55: 1964598065 states generated (17,345,729 s/min), 148015524 distinct states found (952,284 ds/min), 23138574 states left on queue.
- Progress(29) at 2017-10-10 08:10:55: 1982138730 states generated (17,540,665 s/min), 148966999 distinct states found (951,475 ds/min), 23051235 states left on queue.
- Progress(29) at 2017-10-10 08:11:55: 1999853969 states generated (17,715,239 s/min), 149958385 distinct states found (991,386 ds/min), 23018565 states left on queue.
- Progress(29) at 2017-10-10 08:12:55: 2016772612 states generated (16,918,643 s/min), 150979266 distinct states found (1,020,881 ds/min), 23067765 states left on queue.
- Progress(29) at 2017-10-10 08:13:55: 2031304182 states generated (14,531,570 s/min), 151812167 distinct states found (832,901 ds/min), 23056766 states left on queue.
- Progress(29) at 2017-10-10 08:14:55: 2048640657 states generated (17,336,475 s/min), 152587921 distinct states found (775,754 ds/min), 22863601 states left on queue.
- Progress(29) at 2017-10-10 08:15:55: 2066178725 states generated (17,538,068 s/min), 153360880 distinct states found (772,959 ds/min), 22685894 states left on queue.
- Progress(29) at 2017-10-10 08:16:55: 2083082199 states generated (16,903,474 s/min), 154243113 distinct states found (882,233 ds/min), 22561630 states left on queue.
- Progress(30) at 2017-10-10 08:17:55: 2099473970 states generated (16,391,771 s/min), 155137212 distinct states found (894,099 ds/min), 22458664 states left on queue.
- Progress(30) at 2017-10-10 08:18:55: 2114138534 states generated (14,664,564 s/min), 155870384 distinct states found (733,172 ds/min), 22239334 states left on queue.
- Progress(30) at 2017-10-10 08:19:55: 2130579080 states generated (16,440,546 s/min), 156864727 distinct states found (994,343 ds/min), 22101108 states left on queue.
- Progress(30) at 2017-10-10 08:20:55: 2147293695 states generated (16,714,615 s/min), 157809072 distinct states found (944,345 ds/min), 21960052 states left on queue.
- Progress(30) at 2017-10-10 08:21:55: 2164030387 states generated (16,736,692 s/min), 158729776 distinct states found (920,704 ds/min), 21824869 states left on queue.
- Progress(30) at 2017-10-10 08:22:55: 2177620523 states generated (13,590,136 s/min), 159596576 distinct states found (866,800 ds/min), 21798861 states left on queue.
- Progress(30) at 2017-10-10 08:23:55: 2193646068 states generated (16,025,545 s/min), 160612217 distinct states found (1,015,641 ds/min), 21779104 states left on queue.
- Progress(30) at 2017-10-10 08:24:55: 2209887662 states generated (16,241,594 s/min), 161575276 distinct states found (963,059 ds/min), 21782448 states left on queue.
- Progress(30) at 2017-10-10 08:25:55: 2226102534 states generated (16,214,872 s/min), 162579435 distinct states found (1,004,159 ds/min), 21748069 states left on queue.
- Progress(30) at 2017-10-10 08:26:55: 2242395885 states generated (16,293,351 s/min), 163502737 distinct states found (923,302 ds/min), 21680920 states left on queue.
- Progress(30) at 2017-10-10 08:27:55: 2256237160 states generated (13,841,275 s/min), 164363530 distinct states found (860,793 ds/min), 21747340 states left on queue.
- Progress(30) at 2017-10-10 08:28:55: 2272515775 states generated (16,278,615 s/min), 165314953 distinct states found (951,423 ds/min), 21747231 states left on queue.
- Progress(30) at 2017-10-10 08:29:55: 2288588105 states generated (16,072,330 s/min), 166298104 distinct states found (983,151 ds/min), 21748951 states left on queue.
- Progress(30) at 2017-10-10 08:30:55: 2305035992 states generated (16,447,887 s/min), 167218679 distinct states found (920,575 ds/min), 21661734 states left on queue.
- Progress(30) at 2017-10-10 08:31:55: 2319093680 states generated (14,057,688 s/min), 167987075 distinct states found (768,396 ds/min), 21614142 states left on queue.
- Progress(30) at 2017-10-10 08:32:55: 2335843771 states generated (16,750,091 s/min), 168853476 distinct states found (866,401 ds/min), 21471173 states left on queue.
- Progress(30) at 2017-10-10 08:33:55: 2353681128 states generated (17,837,357 s/min), 169685438 distinct states found (831,962 ds/min), 21215693 states left on queue.
- Progress(30) at 2017-10-10 08:34:55: 2371251059 states generated (17,569,931 s/min), 170565598 distinct states found (880,160 ds/min), 21087837 states left on queue.
- Progress(30) at 2017-10-10 08:35:55: 2388501036 states generated (17,249,977 s/min), 171447204 distinct states found (881,606 ds/min), 20996650 states left on queue.
- Progress(30) at 2017-10-10 08:36:55: 2402594035 states generated (14,092,999 s/min), 172258768 distinct states found (811,564 ds/min), 21006530 states left on queue.
- Progress(30) at 2017-10-10 08:37:55: 2419486038 states generated (16,892,003 s/min), 173191486 distinct states found (932,718 ds/min), 20961099 states left on queue.
- Progress(30) at 2017-10-10 08:38:55: 2437219684 states generated (17,733,646 s/min), 173824342 distinct states found (632,856 ds/min), 20640464 states left on queue.
- Progress(30) at 2017-10-10 08:39:55: 2454606692 states generated (17,387,008 s/min), 174581771 distinct states found (757,429 ds/min), 20409922 states left on queue.
- Progress(31) at 2017-10-10 08:40:55: 2471149036 states generated (16,542,344 s/min), 175426889 distinct states found (845,118 ds/min), 20246442 states left on queue.
- Progress(31) at 2017-10-10 08:41:55: 2486814568 states generated (15,665,532 s/min), 176149720 distinct states found (722,831 ds/min), 19936227 states left on queue.
- Progress(31) at 2017-10-10 08:42:55: 2502089283 states generated (15,274,715 s/min), 176932756 distinct states found (783,036 ds/min), 19696793 states left on queue.
- Progress(31) at 2017-10-10 08:43:55: 2519059064 states generated (16,969,781 s/min), 177754542 distinct states found (821,786 ds/min), 19444218 states left on queue.
- Progress(31) at 2017-10-10 08:44:55: 2535583986 states generated (16,524,922 s/min), 178636777 distinct states found (882,235 ds/min), 19272839 states left on queue.
- Progress(31) at 2017-10-10 08:45:55: 2551787900 states generated (16,203,914 s/min), 179540940 distinct states found (904,163 ds/min), 19143552 states left on queue.
- Progress(31) at 2017-10-10 08:46:55: 2567113316 states generated (15,325,416 s/min), 180344846 distinct states found (803,906 ds/min), 19050102 states left on queue.
- Progress(31) at 2017-10-10 08:47:55: 2581858258 states generated (14,744,942 s/min), 181121766 distinct states found (776,920 ds/min), 18923057 states left on queue.
- Progress(31) at 2017-10-10 08:48:55: 2598367281 states generated (16,509,023 s/min), 181998583 distinct states found (876,817 ds/min), 18781934 states left on queue.
- Progress(31) at 2017-10-10 08:49:55: 2614997734 states generated (16,630,453 s/min), 182907629 distinct states found (909,046 ds/min), 18747285 states left on queue.
- Progress(31) at 2017-10-10 08:50:55: 2631751421 states generated (16,753,687 s/min), 183746051 distinct states found (838,422 ds/min), 18688362 states left on queue.
- Progress(31) at 2017-10-10 08:51:55: 2646558930 states generated (14,807,509 s/min), 184546061 distinct states found (800,010 ds/min), 18597609 states left on queue.
- Progress(31) at 2017-10-10 08:52:55: 2661407325 states generated (14,848,395 s/min), 185365894 distinct states found (819,833 ds/min), 18526287 states left on queue.
- Progress(31) at 2017-10-10 08:53:55: 2678353590 states generated (16,946,265 s/min), 186173098 distinct states found (807,204 ds/min), 18333937 states left on queue.
- Progress(31) at 2017-10-10 08:54:55: 2695109608 states generated (16,756,018 s/min), 186993124 distinct states found (820,026 ds/min), 18199478 states left on queue.
- Progress(31) at 2017-10-10 08:55:55: 2712779594 states generated (17,669,986 s/min), 187697325 distinct states found (704,201 ds/min), 17855768 states left on queue.
- Progress(31) at 2017-10-10 08:56:55: 2730382074 states generated (17,602,480 s/min), 188481396 distinct states found (784,071 ds/min), 17663241 states left on queue.
- Progress(31) at 2017-10-10 08:57:55: 2744742195 states generated (14,360,121 s/min), 189151037 distinct states found (669,641 ds/min), 17520020 states left on queue.
- Progress(31) at 2017-10-10 08:58:55: 2761660178 states generated (16,917,983 s/min), 190023911 distinct states found (872,874 ds/min), 17429350 states left on queue.
- Progress(31) at 2017-10-10 08:59:55: 2778856960 states generated (17,196,782 s/min), 190766840 distinct states found (742,929 ds/min), 17224461 states left on queue.
- Progress(31) at 2017-10-10 09:00:55: 2796570724 states generated (17,713,764 s/min), 191421410 distinct states found (654,570 ds/min), 16900855 states left on queue.
- Progress(32) at 2017-10-10 09:01:55: 2813326122 states generated (16,755,398 s/min), 192166741 distinct states found (745,331 ds/min), 16634192 states left on queue.
- Progress(32) at 2017-10-10 09:02:55: 2830156700 states generated (16,830,578 s/min), 192878345 distinct states found (711,604 ds/min), 16219526 states left on queue.
- Progress(32) at 2017-10-10 09:03:55: 2844143250 states generated (13,986,550 s/min), 193470365 distinct states found (592,020 ds/min), 15921082 states left on queue.
- Progress(32) at 2017-10-10 09:04:55: 2860849354 states generated (16,706,104 s/min), 194208096 distinct states found (737,731 ds/min), 15607208 states left on queue.
- Progress(32) at 2017-10-10 09:05:55: 2877303573 states generated (16,454,219 s/min), 194995473 distinct states found (787,377 ds/min), 15370581 states left on queue.
- Progress(32) at 2017-10-10 09:06:55: 2893891672 states generated (16,588,099 s/min), 195739770 distinct states found (744,297 ds/min), 15194409 states left on queue.
- Progress(32) at 2017-10-10 09:07:55: 2910429952 states generated (16,538,280 s/min), 196538141 distinct states found (798,371 ds/min), 14960908 states left on queue.
- Progress(32) at 2017-10-10 09:08:55: 2924385555 states generated (13,955,603 s/min), 197140959 distinct states found (602,818 ds/min), 14765477 states left on queue.
- Progress(32) at 2017-10-10 09:09:55: 2940899492 states generated (16,513,937 s/min), 197906364 distinct states found (765,405 ds/min), 14663636 states left on queue.
- Progress(32) at 2017-10-10 09:10:55: 2957645947 states generated (16,746,455 s/min), 198647736 distinct states found (741,372 ds/min), 14485278 states left on queue.
- Progress(32) at 2017-10-10 09:11:55: 2974156873 states generated (16,510,926 s/min), 199450018 distinct states found (802,282 ds/min), 14336507 states left on queue.
- Progress(32) at 2017-10-10 09:12:55: 2991036985 states generated (16,880,112 s/min), 200159534 distinct states found (709,516 ds/min), 14063580 states left on queue.
- Progress(32) at 2017-10-10 09:13:55: 3007795475 states generated (16,758,490 s/min), 200904730 distinct states found (745,196 ds/min), 13892129 states left on queue.
- Progress(32) at 2017-10-10 09:14:55: 3021946758 states generated (14,151,283 s/min), 201373851 distinct states found (469,121 ds/min), 13554638 states left on queue.
- Progress(32) at 2017-10-10 09:15:55: 3039683116 states generated (17,736,358 s/min), 202048831 distinct states found (674,980 ds/min), 13272212 states left on queue.
- Progress(32) at 2017-10-10 09:16:55: 3056818693 states generated (17,135,577 s/min), 202818542 distinct states found (769,711 ds/min), 13082665 states left on queue.
- Progress(32) at 2017-10-10 09:17:55: 3073835698 states generated (17,017,005 s/min), 203569913 distinct states found (751,371 ds/min), 12874753 states left on queue.
- Progress(32) at 2017-10-10 09:18:55: 3091183828 states generated (17,348,130 s/min), 204137695 distinct states found (567,782 ds/min), 12477498 states left on queue.
- Progress(33) at 2017-10-10 09:19:55: 3107887398 states generated (16,703,570 s/min), 204748049 distinct states found (610,354 ds/min), 12030992 states left on queue.
- Progress(33) at 2017-10-10 09:20:55: 3124712315 states generated (16,824,917 s/min), 205355275 distinct states found (607,226 ds/min), 11574533 states left on queue.
- Progress(33) at 2017-10-10 09:21:55: 3138000646 states generated (13,288,331 s/min), 205871439 distinct states found (516,164 ds/min), 11256114 states left on queue.
- Progress(33) at 2017-10-10 09:22:55: 3154730391 states generated (16,729,745 s/min), 206517247 distinct states found (645,808 ds/min), 10969206 states left on queue.
- Progress(33) at 2017-10-10 09:23:55: 3171623181 states generated (16,892,790 s/min), 207194928 distinct states found (677,681 ds/min), 10650387 states left on queue.
- Progress(33) at 2017-10-10 09:24:55: 3188491969 states generated (16,868,788 s/min), 207838491 distinct states found (643,563 ds/min), 10374410 states left on queue.
- Progress(33) at 2017-10-10 09:25:55: 3205858145 states generated (17,366,176 s/min), 208458360 distinct states found (619,869 ds/min), 10174465 states left on queue.
- Progress(33) at 2017-10-10 09:26:55: 3222619210 states generated (16,761,065 s/min), 209139231 distinct states found (680,871 ds/min), 9895555 states left on queue.
- Progress(33) at 2017-10-10 09:27:55: 3238054376 states generated (15,435,166 s/min), 209704987 distinct states found (565,756 ds/min), 9610887 states left on queue.
- Progress(33) at 2017-10-10 09:28:55: 3252999992 states generated (14,945,616 s/min), 210278532 distinct states found (573,545 ds/min), 9415402 states left on queue.
- Progress(33) at 2017-10-10 09:29:55: 3270455079 states generated (17,455,087 s/min), 210794343 distinct states found (515,811 ds/min), 8986271 states left on queue.
- Progress(33) at 2017-10-10 09:30:55: 3287869341 states generated (17,414,262 s/min), 211421914 distinct states found (627,571 ds/min), 8666306 states left on queue.
- Progress(33) at 2017-10-10 09:31:55: 3305022258 states generated (17,152,917 s/min), 212069479 distinct states found (647,565 ds/min), 8365342 states left on queue.
- Progress(34) at 2017-10-10 09:32:55: 3321979975 states generated (16,957,717 s/min), 212578811 distinct states found (509,332 ds/min), 7858520 states left on queue.
- Progress(34) at 2017-10-10 09:33:55: 3338794792 states generated (16,814,817 s/min), 213091973 distinct states found (513,162 ds/min), 7317330 states left on queue.
- Progress(34) at 2017-10-10 09:34:55: 3355831365 states generated (17,036,573 s/min), 213621292 distinct states found (529,319 ds/min), 6949996 states left on queue.
- Progress(34) at 2017-10-10 09:35:55: 3369221549 states generated (13,390,184 s/min), 214053210 distinct states found (431,918 ds/min), 6604198 states left on queue.
- Progress(34) at 2017-10-10 09:36:55: 3386627951 states generated (17,406,402 s/min), 214584642 distinct states found (531,432 ds/min), 6339802 states left on queue.
- Progress(34) at 2017-10-10 09:37:55: 3403663753 states generated (17,035,802 s/min), 215127248 distinct states found (542,606 ds/min), 5987702 states left on queue.
- Progress(34) at 2017-10-10 09:38:55: 3421111642 states generated (17,447,889 s/min), 215655008 distinct states found (527,760 ds/min), 5659734 states left on queue.
- Progress(34) at 2017-10-10 09:39:55: 3438238401 states generated (17,126,759 s/min), 216111400 distinct states found (456,392 ds/min), 5231641 states left on queue.
- Progress(34) at 2017-10-10 09:40:55: 3455627147 states generated (17,388,746 s/min), 216689728 distinct states found (578,328 ds/min), 4843114 states left on queue.
- Progress(35) at 2017-10-10 09:41:55: 3472284937 states generated (16,657,790 s/min), 217122213 distinct states found (432,485 ds/min), 4313415 states left on queue.
- Progress(35) at 2017-10-10 09:42:55: 3488820111 states generated (16,535,174 s/min), 217528736 distinct states found (406,523 ds/min), 3839159 states left on queue.
- Progress(35) at 2017-10-10 09:43:55: 3506189866 states generated (17,369,755 s/min), 217959686 distinct states found (430,950 ds/min), 3436835 states left on queue.
- Progress(35) at 2017-10-10 09:44:55: 3520017214 states generated (13,827,348 s/min), 218299667 distinct states found (339,981 ds/min), 3136247 states left on queue.
- Progress(35) at 2017-10-10 09:45:55: 3537210871 states generated (17,193,657 s/min), 218699238 distinct states found (399,571 ds/min), 2746407 states left on queue.
- Progress(35) at 2017-10-10 09:46:55: 3554228356 states generated (17,017,485 s/min), 219135328 distinct states found (436,090 ds/min), 2287767 states left on queue.
- Progress(36) at 2017-10-10 09:47:55: 3570427648 states generated (16,199,292 s/min), 219450785 distinct states found (315,457 ds/min), 1738714 states left on queue.
- Progress(36) at 2017-10-10 09:48:55: 3587321793 states generated (16,894,145 s/min), 219760298 distinct states found (309,513 ds/min), 1353662 states left on queue.
- Progress(36) at 2017-10-10 09:49:55: 3603964649 states generated (16,642,856 s/min), 220087273 distinct states found (326,975 ds/min), 909214 states left on queue.
- Progress(37) at 2017-10-10 09:50:55: 3619809539 states generated (15,844,890 s/min), 220304829 distinct states found (217,556 ds/min), 490783 states left on queue.
- Progress(39) at 2017-10-10 09:51:55: 3634988915 states generated (15,179,376 s/min), 220493344 distinct states found (188,515 ds/min), 75385 states left on queue.
- 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 = .041
- based on the actual fingerprints: val = .0083
- Progress(44) at 2017-10-10 09:52:29: 3638478200 states generated (16,198,345 s/min), 220515772 distinct states found (981,726 ds/min), 0 states left on queue.
- 3638478200 states generated, 220515772 distinct states found, 0 states left on queue.
- The depth of the complete state graph search is 44.
- The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 15 and the 95th percentile is 3).
- Finished in 13478458ms at (2017-10-10 09:52:30)
- markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ /home/markus/Downloads/jdk-9+181/bin/java --add-modules=java.activation -jar tla2tools.jar -workers 32
- TLC2 Version 2.10 of 28 September 2017 (rev: ${git.shortRevision})
- Running breadth-first search Model-Checking with 32 workers on 32 cores with 15095MB heap and 64MB offheap memory (Linux 4.4.0-1035-aws amd64, Eclipse OpenJ9 9-internal x86_64).
- Starting SANY...
- Parsing file /tmp/MC.tla
- Parsing file /tmp/PaxosCommit.tla
- Parsing file /tmp/TLC.tla
- Parsing file /tmp/Integers.tla
- Parsing file /tmp/Naturals.tla
- Parsing file /tmp/TCommit.tla
- Parsing file /tmp/Sequences.tla
- Semantic processing of module Naturals
- Semantic processing of module Integers
- Semantic processing of module TCommit
- Semantic processing of module PaxosCommit
- Semantic processing of module Sequences
- Semantic processing of module TLC
- Semantic processing of module MC
- SANY finished.
- Starting... (2017-10-10 19:03:48)
- unsuccessfully trying to load custom FPSet class: tlc2.tool.fp.MSBDiskFPSet
- java.lang.reflect.InvocationTargetException
- at jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(java.base@9-internal/Native Method)
- at jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(java.base@9-internal/NativeConstructorAccessorImpl.java:62)
- at jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(java.base@9-internal/DelegatingConstructorAccessorImpl.java:45)
- at java.lang.reflect.Constructor.newInstance(java.base@9-internal/Constructor.java:488)
- at tlc2.tool.fp.FPSetFactory.loadImplementation(FPSetFactory.java:180)
- at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:104)
- at tlc2.tool.fp.MultiFPSet.getNestedFPSets(MultiFPSet.java:66)
- at tlc2.tool.fp.MultiFPSet.<init>(MultiFPSet.java:58)
- at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:100)
- at tlc2.tool.ModelChecker.<init>(ModelChecker.java:86)
- at tlc2.TLC.process(TLC.java:825)
- at tlc2.TLC.main(TLC.java:213)
- Caused by: java.lang.ExceptionInInitializerError
- at java.lang.J9VMInternals.ensureError(java.base@9-internal/J9VMInternals.java:191)
- at java.lang.J9VMInternals.recordInitializationFailure(java.base@9-internal/J9VMInternals.java:180)
- at tlc2.tool.fp.DiskFPSet.<init>(DiskFPSet.java:128)
- at tlc2.tool.fp.HeapBasedDiskFPSet.<init>(HeapBasedDiskFPSet.java:65)
- at tlc2.tool.fp.MSBDiskFPSet.<init>(MSBDiskFPSet.java:35)
- ... 12 more
- Caused by: java.lang.UnsupportedOperationException: The method has not yet been implemented for now
- at java.lang.invoke.MethodHandles.privateLookupIn(java.base@9-internal/MethodHandles.java:1538)
- at java.util.concurrent.atomic.Striped64$1.run(java.base@9-internal/Striped64.java:390)
- at java.util.concurrent.atomic.Striped64$1.run(java.base@9-internal/Striped64.java:387)
- at java.security.AccessController.doPrivileged(java.base@9-internal/AccessController.java:638)
- at java.util.concurrent.atomic.Striped64.<clinit>(java.base@9-internal/Striped64.java:386)
- ... 15 more
- java.lang.reflect.InvocationTargetException
- at jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(java.base@9-internal/Native Method)
- at jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(java.base@9-internal/NativeConstructorAccessorImpl.java:62)
- at jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(java.base@9-internal/DelegatingConstructorAccessorImpl.java:45)
- at java.lang.reflect.Constructor.newInstance(java.base@9-internal/Constructor.java:488)
- at tlc2.tool.fp.FPSetFactory.loadImplementation(FPSetFactory.java:180)
- at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:104)
- at tlc2.tool.fp.MultiFPSet.getNestedFPSets(MultiFPSet.java:66)
- at tlc2.tool.fp.MultiFPSet.<init>(MultiFPSet.java:58)
- at tlc2.tool.fp.FPSetFactory.getFPSet(FPSetFactory.java:100)
- at tlc2.tool.ModelChecker.<init>(ModelChecker.java:86)
- at tlc2.TLC.process(TLC.java:825)
- at tlc2.TLC.main(TLC.java:213)
- Caused by: java.lang.NoClassDefFoundError: java.util.concurrent.atomic.LongAdder (initialization failure)
- at java.lang.J9VMInternals.initializationAlreadyFailed(java.base@9-internal/J9VMInternals.java:141)
- at tlc2.tool.fp.DiskFPSet.<init>(DiskFPSet.java:128)
- at tlc2.tool.fp.HeapBasedDiskFPSet.<init>(HeapBasedDiskFPSet.java:65)
- at tlc2.tool.fp.MSBDiskFPSet.<init>(MSBDiskFPSet.java:35)
- ... 12 more
- Caused by: java.lang.UnsupportedOperationException: The method has not yet been implemented for now
- at java.lang.invoke.MethodHandles.privateLookupIn(java.base@9-internal/MethodHandles.java:1538)
- at java.util.concurrent.atomic.Striped64$1.run(java.base@9-internal/Striped64.java:390)
- at java.util.concurrent.atomic.Striped64$1.run(java.base@9-internal/Striped64.java:387)
- at java.security.AccessController.doPrivileged(java.base@9-internal/AccessController.java:638)
- at java.util.concurrent.atomic.Striped64.<clinit>(java.base@9-internal/Striped64.java:386)
- ... 15 more
- TLC threw an unexpected exception.
- This was probably caused by an error in the spec or model.
- See the User Output or TLC Console for clues to what happened.
- The exception was a java.lang.NullPointerException
- java.lang.NullPointerException
- at tlc2.tool.fp.MultiFPSet.init(MultiFPSet.java:76)
- at tlc2.tool.ModelChecker.<init>(ModelChecker.java:89)
- at tlc2.TLC.process(TLC.java:825)
- at tlc2.TLC.main(TLC.java:213)
- Finished in 617ms at (2017-10-10 19:03:49)
- markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ /home/markus/Downloads/jdk-9+181/bin/java -version
- openjdk version "9-internal"
- OpenJDK Runtime Environment (build 9-internal+0-adhoc.jenkins.openjdk)
- Eclipse OpenJ9 VM (build 2.9, JRE 9 Linux amd64-64 Compressed References 20170915_6 (JIT enabled, AOT enabled)
- J9VM - cea1ed7
- JIT - cea1ed7
- OMR - 617de12
- OpenJDK - 83f5cd0 based on )
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement