Component based Model Checking 3.14omega
Preparing components
Allocating memory management
Loading bytecode from test/lunar.pr.b
Initialized Bloom filter, k=1, 1.073.741.824 bits
Allocated lossy hashing with 1.048.576 entries, 400.000.000 max size, 4.194.304 consumed
Initialized hash partition disk storage, 128 partitions, page size 65536, lookup buffer 65536, working file prefix /local/tmp/diskstore
At 2s downrange: visited 100.000 states, sets: open: 1.690, candidate: 4
At 3s downrange: visited 200.000 states, sets: open: 3.486, candidate: 20
At 5s downrange: visited 300.000 states, sets: open: 5.223, candidate: 43
At 6s downrange: visited 400.000 states, sets: open: 7.110, candidate: 82
At 8s downrange: visited 500.000 states, sets: open: 9.626, candidate: 122
At 9s downrange: visited 600.000 states, sets: open: 11.816, candidate: 162
At 9s downrange, 636.688 elements: reclaiming 104857 states
Done at 10s downrange
At 11s downrange: visited 700.000 states, sets: open: 13.966, candidate: 229
At 11s downrange, 735.071 elements: reclaiming 104857 states
Done at 12s downrange
At 13s downrange: visited 800.000 states, sets: open: 16.224, candidate: 308
At 13s downrange, 833.925 elements: reclaiming 104857 states
Done at 13s downrange
At 15s downrange: visited 900.000 states, sets: open: 18.383, candidate: 413
At 15s downrange, 931.238 elements: reclaiming 104857 states
Done at 15s downrange
At 16s downrange: visited 1.000.000 states, sets: open: 19.266, candidate: 508
At 17s downrange, 1.031.265 elements: reclaiming 104857 states
Done at 17s downrange
At 18s downrange: visited 1.100.000 states, sets: open: 22.677, candidate: 607
At 19s downrange, 1.129.007 elements: reclaiming 104857 states
Done at 19s downrange
At 20s downrange: visited 1.200.000 states, sets: open: 26.033, candidate: 714
At 21s downrange, 1.230.202 elements: reclaiming 104857 states
Done at 21s downrange
At 22s downrange: visited 1.300.000 states, sets: open: 27.103, candidate: 874
At 23s downrange, 1.330.478 elements: reclaiming 104857 states
Done at 23s downrange
At 24s downrange: visited 1.400.000 states, sets: open: 30.853, candidate: 1.061
At 24s downrange, 1.425.591 elements: reclaiming 104857 states
Done at 25s downrange
At 26s downrange: visited 1.500.000 states, sets: open: 32.039, candidate: 1.203
At 27s downrange, 1.527.144 elements: reclaiming 104857 states
Done at 27s downrange
At 28s downrange: visited 1.600.000 states, sets: open: 33.050, candidate: 1.343
At 29s downrange, 1.627.835 elements: reclaiming 104857 states
Done at 29s downrange
At 30s downrange: visited 1.700.000 states, sets: open: 35.321, candidate: 1.510
At 31s downrange, 1.724.112 elements: reclaiming 104857 states
Done at 31s downrange
At 32s downrange: visited 1.800.000 states, sets: open: 37.799, candidate: 1.675
At 33s downrange, 1.821.582 elements: reclaiming 104857 states
Done at 33s downrange
At 34s downrange: visited 1.900.000 states, sets: open: 40.661, candidate: 1.869
At 35s downrange, 1.923.065 elements: reclaiming 104857 states
Done at 35s downrange
At 36s downrange: visited 2.000.000 states, sets: open: 38.793, candidate: 2.074
At 37s downrange, 2.028.279 elements: reclaiming 104857 states
Done at 37s downrange
At 38s downrange: visited 2.100.000 states, sets: open: 41.262, candidate: 2.273
At 39s downrange, 2.122.975 elements: reclaiming 104857 states
Done at 39s downrange
At 40s downrange: visited 2.200.000 states, sets: open: 43.034, candidate: 2.492
At 41s downrange, 2.220.767 elements: reclaiming 104857 states
Done at 41s downrange
At 42s downrange: visited 2.300.000 states, sets: open: 46.659, candidate: 2.711
At 43s downrange, 2.321.173 elements: reclaiming 104857 states
Done at 43s downrange
At 44s downrange: visited 2.400.000 states, sets: open: 48.209, candidate: 2.947
At 45s downrange, 2.422.157 elements: reclaiming 104857 states
Done at 56s downrange
At 57s downrange: visited 2.500.000 states, sets: open: 48.619, candidate: 3.234
At 58s downrange, 2.522.910 elements: reclaiming 104857 states
Done at 58s downrange
At 59s downrange: visited 2.600.000 states, sets: open: 51.661, candidate: 3.508
At 60s downrange, 2.623.500 elements: reclaiming 104857 states
Done at 60s downrange
At 62s downrange: visited 2.700.000 states, sets: open: 53.786, candidate: 3.798
At 62s downrange, 2.721.269 elements: reclaiming 104857 states
Done at 62s downrange
At 64s downrange: visited 2.800.000 states, sets: open: 53.791, candidate: 4.089
At 64s downrange, 2.822.037 elements: reclaiming 104857 states
Done at 64s downrange
At 66s downrange: visited 2.900.000 states, sets: open: 55.670, candidate: 4.406
At 66s downrange, 2.921.446 elements: reclaiming 104857 states
Done at 67s downrange
At 68s downrange: visited 3.000.000 states, sets: open: 54.360, candidate: 4.730
At 68s downrange, 3.021.526 elements: reclaiming 104857 states
Done at 69s downrange
At 70s downrange: visited 3.100.000 states, sets: open: 55.194, candidate: 5.067
At 70s downrange, 3.122.210 elements: reclaiming 104857 states
Done at 71s downrange
At 73s downrange: visited 3.200.000 states, sets: open: 52.273, candidate: 5.373
At 73s downrange, 3.224.927 elements: reclaiming 104857 states
Done at 73s downrange
At 75s downrange: visited 3.300.000 states, sets: open: 55.657, candidate: 5.729
At 75s downrange, 3.324.735 elements: reclaiming 104857 states
Done at 76s downrange
At 77s downrange: visited 3.400.000 states, sets: open: 58.128, candidate: 6.118
At 77s downrange, 3.425.721 elements: reclaiming 104857 states
Done at 78s downrange
At 79s downrange: visited 3.500.000 states, sets: open: 59.825, candidate: 6.470
At 79s downrange, 3.528.474 elements: reclaiming 104857 states
Done at 80s downrange
At 81s downrange: visited 3.600.000 states, sets: open: 62.133, candidate: 6.811
At 82s downrange, 3.627.018 elements: reclaiming 104857 states
Done at 82s downrange
At 83s downrange: visited 3.700.000 states, sets: open: 61.968, candidate: 7.235
At 84s downrange, 3.726.993 elements: reclaiming 104857 states
Done at 85s downrange
At 87s downrange: visited 3.800.000 states, sets: open: 57.773, candidate: 7.636
At 87s downrange, 3.827.619 elements: reclaiming 104857 states
Done at 91s downrange
At 92s downrange: visited 3.900.000 states, sets: open: 57.695, candidate: 8.040
At 93s downrange, 3.929.296 elements: reclaiming 104857 states
Done at 93s downrange
At 95s downrange: visited 4.000.000 states, sets: open: 60.740, candidate: 8.469
At 95s downrange, 4.031.584 elements: reclaiming 104857 states
Done at 96s downrange
At 97s downrange: visited 4.100.000 states, sets: open: 62.659, candidate: 8.898
At 97s downrange, 4.135.002 elements: reclaiming 104857 states
Done at 98s downrange
At 99s downrange: visited 4.200.000 states, sets: open: 65.269, candidate: 9.362
At 99s downrange, 4.233.169 elements: reclaiming 104857 states
Done at 100s downrange
At 101s downrange: visited 4.300.000 states, sets: open: 62.898, candidate: 9.831
At 101s downrange, 4.332.881 elements: reclaiming 104857 states
Done at 107s downrange
At 108s downrange: visited 4.400.000 states, sets: open: 57.674, candidate: 10.261
At 109s downrange, 4.435.501 elements: reclaiming 104857 states
Done at 110s downrange
At 111s downrange: visited 4.500.000 states, sets: open: 57.656, candidate: 10.729
At 111s downrange, 4.539.256 elements: reclaiming 104857 states
Done at 112s downrange
At 113s downrange: visited 4.600.000 states, sets: open: 62.113, candidate: 11.236
At 114s downrange, 4.641.382 elements: reclaiming 104857 states
Done at 122s downrange
At 123s downrange: visited 4.700.000 states, sets: open: 62.329, candidate: 11.708
At 123s downrange, 4.745.113 elements: reclaiming 104857 states
Done at 124s downrange
At 125s downrange: visited 4.800.000 states, sets: open: 62.897, candidate: 12.215
At 125s downrange, 4.842.755 elements: reclaiming 104857 states
Done at 126s downrange
At 127s downrange: visited 4.900.000 states, sets: open: 61.133, candidate: 12.749
At 128s downrange, 4.941.521 elements: reclaiming 104857 states
Done at 128s downrange
At 129s downrange: visited 5.000.000 states, sets: open: 56.017, candidate: 13.252
At 130s downrange, 5.044.819 elements: reclaiming 104857 states
Done at 130s downrange
At 132s downrange: visited 5.100.000 states, sets: open: 57.104, candidate: 13.752
At 132s downrange, 5.149.764 elements: reclaiming 104857 states
Done at 133s downrange
At 134s downrange: visited 5.200.000 states, sets: open: 60.837, candidate: 14.305
At 135s downrange, 5.251.432 elements: reclaiming 104857 states
Done at 135s downrange
At 136s downrange: visited 5.300.000 states, sets: open: 59.469, candidate: 14.836
At 137s downrange, 5.358.669 elements: reclaiming 104857 states
Done at 137s downrange
At 138s downrange: visited 5.400.000 states, sets: open: 61.089, candidate: 15.465
At 139s downrange, 5.457.126 elements: reclaiming 104857 states
Done at 144s downrange
At 144s downrange: visited 5.500.000 states, sets: open: 60.292, candidate: 16.104
At 145s downrange, 5.554.532 elements: reclaiming 104857 states
Done at 146s downrange
At 147s downrange: visited 5.600.000 states, sets: open: 56.971, candidate: 16.720
At 148s downrange, 5.655.677 elements: reclaiming 104857 states
Done at 148s downrange
At 149s downrange: visited 5.700.000 states, sets: open: 54.753, candidate: 17.346
At 150s downrange, 5.757.577 elements: reclaiming 104857 states
Done at 151s downrange
At 152s downrange: visited 5.800.000 states, sets: open: 57.204, candidate: 17.942
At 152s downrange, 5.860.822 elements: reclaiming 104857 states
Done at 156s downrange
At 157s downrange: visited 5.900.000 states, sets: open: 52.737, candidate: 18.495
At 158s downrange, 5.964.260 elements: reclaiming 104857 states
Done at 158s downrange
At 159s downrange: visited 6.000.000 states, sets: open: 55.345, candidate: 19.155
At 160s downrange, 6.065.823 elements: reclaiming 104857 states
Done at 161s downrange
At 161s downrange: visited 6.100.000 states, sets: open: 58.271, candidate: 19.747
At 163s downrange, 6.167.817 elements: reclaiming 104857 states
Done at 168s downrange
At 168s downrange: visited 6.200.000 states, sets: open: 58.105, candidate: 20.372
At 170s downrange, 6.271.027 elements: reclaiming 104857 states
Done at 170s downrange
At 171s downrange: visited 6.300.000 states, sets: open: 54.746, candidate: 21.130
At 172s downrange, 6.373.780 elements: reclaiming 104857 states
Done at 172s downrange
At 173s downrange: visited 6.400.000 states, sets: open: 54.149, candidate: 21.730
At 174s downrange, 6.482.791 elements: reclaiming 104857 states
Done at 175s downrange
At 175s downrange: visited 6.500.000 states, sets: open: 49.002, candidate: 22.406
At 176s downrange, 6.583.021 elements: reclaiming 104857 states
Done at 179s downrange
At 179s downrange: visited 6.600.000 states, sets: open: 49.024, candidate: 23.128
At 181s downrange, 6.682.504 elements: reclaiming 104857 states
Done at 182s downrange
At 182s downrange: visited 6.700.000 states, sets: open: 48.538, candidate: 23.846
At 183s downrange, 6.784.247 elements: reclaiming 104857 states
Done at 184s downrange
At 184s downrange: visited 6.800.000 states, sets: open: 47.878, candidate: 24.566
At 185s downrange, 6.886.567 elements: reclaiming 104857 states
Done at 186s downrange
At 187s downrange: visited 6.900.000 states, sets: open: 46.456, candidate: 25.221
At 188s downrange, 6.994.064 elements: reclaiming 104857 states
Done at 196s downrange
At 196s downrange: visited 7.000.000 states, sets: open: 39.165, candidate: 25.944
At 198s downrange, 7.098.503 elements: reclaiming 104857 states
Done at 199s downrange
At 199s downrange: visited 7.100.000 states, sets: open: 37.353, candidate: 26.607
At 202s downrange: visited 7.200.000 states, sets: open: 36.709, candidate: 27.321
At 202s downrange, 7.200.572 elements: reclaiming 104857 states
Done at 202s downrange
At 204s downrange: visited 7.300.000 states, sets: open: 28.165, candidate: 28.068
At 205s downrange, 7.312.483 elements: reclaiming 104857 states
Done at 205s downrange
At 207s downrange: visited 7.400.000 states, sets: open: 25.772, candidate: 28.858
At 208s downrange, 7.414.919 elements: reclaiming 104857 states
Done at 209s downrange
At 210s downrange: visited 7.500.000 states, sets: open: 20.132, candidate: 29.666
At 210s downrange, 7.522.266 elements: reclaiming 104857 states
Done at 213s downrange
At 214s downrange: visited 7.600.000 states, sets: open: 15.318, candidate: 30.477
At 215s downrange, 7.629.938 elements: reclaiming 104857 states
Done at 218s downrange
At 219s downrange: visited 7.700.000 states, sets: open: 7.316, candidate: 31.312
At 220s downrange, 7.741.920 elements: reclaiming 104857 states
Done at 228s downrange
At 228s downrange, 7.760.950 elements: Complete partitions lookup, 31869 elements... 128 partitions, 68832 pages read, 28396 elements reopened, 568 seconds elapsed...
At 804s downrange: visited 7.800.000 states, sets: open: 25.148, candidate: 3.219
At 806s downrange, 7.823.449 elements: reclaiming 104857 states
Done at 814s downrange
At 823s downrange: visited 7.900.000 states, sets: open: 11.464, candidate: 12.003
At 827s downrange, 7.943.567 elements: reclaiming 104857 states
Done at 833s downrange
At 837s downrange: visited 8.000.000 states, sets: open: 1.416, candidate: 22.419
At 838s downrange, 8.047.861 elements: reclaiming 104857 states
Done at 842s downrange
At 845s downrange, 8.086.301 elements: Complete partitions lookup, 27353 elements... 128 partitions, 71745 pages read, 2171 elements reopened, 401 seconds elapsed...
At 1.248s downrange: visited 8.100.000 states, sets: open: 619, candidate: 1.237
At 1.248s downrange, 8.117.450 elements: Complete partitions lookup, 2323 elements... 128 partitions, 71745 pages read, 200 elements reopened, 382 seconds elapsed...
At 1.630s downrange, 8.119.203 elements: Complete partitions lookup, 142 elements... 84 partitions, 47084 pages read, 11 elements reopened, 258 seconds elapsed...
At 1.888s downrange, 8.119.307 elements: Complete partitions lookup, 10 elements... 9 partitions, 5034 pages read, 1 elements reopened, 27 seconds elapsed...
At 1.915s downrange, 8.119.319 elements: Complete partitions lookup, 1 elements... 1 partitions, 559 pages read, 0 elements reopened, 2 seconds elapsed...

Search complete: visited 8.119.319 states, created 8.723.018 states, search time elapsed: 1.917s, maximum state size 603
                   7.828.962 single successor states, 0 dead ends, 53.431 DFS problems (53 real)
Double caching: 6 explicit lookups
  Bloom filter, k=1, size 1073741824: 0 partial collisions
                8088540 bits set, 8119319 entries, collision rate: 1.00, fill rate:0.01
    8723019 queries, 8088540 resolved
  Lossy hashing with 8119319 elements; reclaimed 7727374 elements with 306.257.134 bytes in 74 runs
    634479 queries, 572781 resolved
  Cache failures: 61698
  Diskstore: 61.698 lookups, 290 maximum lookup size, 27.575 revisits detected
             71.745 pages written, 264.999 pages read, 65.536 pagesize, 128 partitions, 65.536 lookupbuf
State size histogram: 220:23, 262:3, 304:3, 346:3, 380:1, 387:1, 388:5, 434:157, 441:50, 488:3.445, 495:672, 542:77.329, 549:3.124, 596:8.633.222, 603:4.980