Oracle vs. J9 VM

gistfile1.txt

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 )