[mcracetrack] Explicit McRaceTrack Model Checker Version 4.2
[mcracetrack] Copyright (C) 2015 Armin Biere JKU Linz
[mcracetrack] gcc -Wall -O3 -DNDEBUG -DNLOG -DBACKWARD
[mcracetrack] maximum acceleration 10 increment 1
[mcracetrack] using euclidean norm to limit acceleration
[mcracetrack] moves which can not be handled will force abort
[mcracetrack] garbage collection enabled
[mcracetrack] both forward and backward reachability analysis
[mcracetrack] will sort generations
[mcracetrack] measuring process time
[mcracetrack] using default parcours of c't 2015 issue 23
[mcracetrack] found and sorted 4 horizontal segments
[mcracetrack] found and sorted 3 vertical segments
[mcracetrack] maximum number of states 4294967296
[mcracetrack] velocity range [0..127] 7 bits
[mcracetrack] coordinate range [0..511] 9 bits
[mcracetrack] sizeof (long) = 8 bytes
[mcracetrack] sizeof (State) = 8 bytes
[mcracetrack] visited table needs 512.0 MB
[mcracetrack] maximum states stack of 32.0 GB
[mcracetrack] prepared acceleration table with 317 pairs 72%
[mcracetrack] 0.00: search initialized
[mcracetrack] 0.00: sorted forward 0 of 1 states in 0.001 sec
[mcracetrack] 0.00: sorted backward 0 of 1 states in 0.001 sec
[mcracetrack] 0.01: expand forward 0 of 1 states in 0.006 sec
[mcracetrack] 0.01: sorted forward 1 of 316 states in 0.004 sec
[mcracetrack] 0.01: expand backward 0 of 1 states in 0.001 sec
[mcracetrack] 0.01: sorted backward 1 of 316 states in 0.000 sec
[mcracetrack] 0.03: expand forward 1 of 316 states in 0.011 sec
[mcracetrack] 0.03: sorted forward 2 of 92696 states in 0.001 sec
[mcracetrack] 0.04: expand backward 1 of 316 states in 0.011 sec
[mcracetrack] 0.04: sorted backward 2 of 92696 states in 0.001 sec
[mcracetrack] 0.19: expand forward 2 of 92696 states in 0.156 sec
[mcracetrack] 0.20: sorted forward 3 of 774370 states in 0.007 sec
[mcracetrack] 0.20: marked forward 3 collected 244.5 KB 4% in 0.003 sec
[mcracetrack] 0.36: expand backward 2 of 92696 states in 0.157 sec
[mcracetrack] 0.37: sorted backward 3 of 774370 states in 0.007 sec
[mcracetrack] 0.37: marked backward 3 collected 261.0 KB 4% in 0.003 sec
[mcracetrack] 1.44: expand forward 3 of 774370 states in 1.074 sec
[mcracetrack] 1.47: sorted forward 4 of 2927418 states in 0.026 sec
[mcracetrack] 1.49: marked forward 4 collected 2.3 MB 8% in 0.019 sec
[mcracetrack] 2.57: expand backward 3 of 774370 states in 1.078 sec
[mcracetrack] 2.60: sorted backward 4 of 3012268 states in 0.027 sec
[mcracetrack] 2.61: marked backward 4 collected 2.4 MB 8% in 0.019 sec
[mcracetrack] 6.56: expand forward 4 of 2927418 states in 3.943 sec
[mcracetrack] 6.62: sorted forward 5 of 6616183 states in 0.060 sec
[mcracetrack] 6.68: marked forward 5 collected 10.4 MB 14% in 0.063 sec
[mcracetrack] 10.75: expand backward 4 of 3012268 states in 4.070 sec
[mcracetrack] 10.82: sorted backward 5 of 7736674 states in 0.070 sec
[mcracetrack] 10.89: marked backward 5 collected 7.6 MB 9% in 0.072 sec
[mcracetrack] 19.81: expand forward 5 of 6616183 states in 8.916 sec
[mcracetrack] 19.93: sorted forward 6 of 12875980 states in 0.119 sec
[mcracetrack] 20.08: marked forward 6 collected 22.5 MB 14% in 0.148 sec
[mcracetrack] 30.42: expand backward 5 of 7736674 states in 10.345 sec
[mcracetrack] 30.54: sorted backward 6 of 13215854 states in 0.118 sec
[mcracetrack] 30.71: marked backward 6 collected 21.6 MB 12% in 0.171 sec
[mcracetrack] 47.91: expand forward 6 of 12875980 states in 17.202 sec
[mcracetrack] 48.07: sorted forward 7 of 17019036 states in 0.156 sec
[mcracetrack] 48.33: marked forward 7 collected 49.8 MB 18% in 0.261 sec
[mcracetrack] 65.99: expand backward 6 of 13215854 states in 17.659 sec
[mcracetrack] 66.16: sorted backward 7 of 19259877 states in 0.173 sec
[mcracetrack] 66.47: marked backward 7 collected 49.6 MB 16% in 0.308 sec
[mcracetrack] 89.17: expand forward 7 of 17019036 states in 22.699 sec
[mcracetrack] 89.35: sorted forward 8 of 20874496 states in 0.186 sec
[mcracetrack] 89.73: marked forward 8 collected 77.7 MB 20% in 0.379 sec
[mcracetrack] 115.37: expand backward 7 of 19259877 states in 25.637 sec
[mcracetrack] 115.62: sorted backward 8 of 27724656 states in 0.248 sec
[mcracetrack] 116.10: marked backward 8 collected 80.8 MB 17% in 0.480 sec
[mcracetrack] 126.83: forward found matching middle 227 290 -17 -16
s REACHED
1: 120 180 0 0 --[9,-3]-> 129 177 9 -3 (9,-3)
2: 129 177 9 -3 --[19,-3]-> 148 174 19 -3 (10,0)
3: 148 174 19 -3 --[25,4]-> 173 178 25 4 (6,7)
4: 173 178 25 4 --[21,13]-> 194 191 21 13 (-4,9)
5: 194 191 21 13 --[13,19]-> 207 210 13 19 (-8,6)
6: 207 210 13 19 --[5,25]-> 212 235 5 25 (-8,6)
7: 212 235 5 25 --[4,31]-> 216 266 4 31 (-1,6)
8: 216 266 4 31 --[11,24]-> 227 290 11 24 (7,-7)
9: 227 290 11 24 --[17,16]-> 244 306 17 16 (6,-8)
10: 244 306 17 16 --[21,7]-> 265 313 21 7 (4,-9)
11: 265 313 21 7 --[21,-3]-> 286 310 21 -3 (0,-10)
12: 286 310 21 -3 --[17,-12]-> 303 298 17 -12 (-4,-9)
13: 303 298 17 -12 --[11,-20]-> 314 278 11 -20 (-6,-8)
14: 314 278 11 -20 --[6,-28]-> 320 250 6 -28 (-5,-8)
15: 320 250 6 -28 --[0,-20]-> 320 230 0 -20 (-6,8)
16: 320 230 0 -20 --[0,-10]-> 320 220 0 -10 (0,10)
17: 320 220 0 -10 --[0,0]-> 320 220 0 0 (0,10)
[mcracetrack] worked on 18 generations
[mcracetrack] found 145004107 states 3% at 1.143 millions/sec
[mcracetrack] active 102367535 states 71%, 61146640 max 42%
[mcracetrack] collected 325.3 MB of 42636572 states 29%
[mcracetrack] moves range from [-52,-45] to [58,47]
[mcracetrack] checked 221631016 moves, valid 65%, invalid 35%
[mcracetrack] intersection checks 78% with on average 0.36 segments
[mcracetrack] invalid 3355976 moves out-of-box 4%
[mcracetrack] invalid 27137500 moves intersecting segment 35%
[mcracetrack] invalid 46133435 moves hitting border 60%
[mcracetrack] fixed static memory of 1.0 MB 0%
[mcracetrack] maximum allocated heap memory of 3.2 GB 100%
[mcracetrack] total maximum allocated memory of 3.2 GB
[mcracetrack] sorting time 1.20 sec 1%
[mcracetrack] garbage collection time 1.93 sec 2%
[mcracetrack] expansion time 112.97 sec 89%
[mcracetrack] finished after 126.86 seconds