[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 disabled
[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.000 sec
[mcracetrack] 0.01: expand backward 0 of 1 states in 0.005 sec
[mcracetrack] 0.01: sorted backward 1 of 316 states in 0.000 sec
[mcracetrack] 0.02: expand forward 1 of 316 states in 0.011 sec
[mcracetrack] 0.03: sorted forward 2 of 92696 states in 0.004 sec
[mcracetrack] 0.04: expand backward 1 of 316 states in 0.009 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.157 sec
[mcracetrack] 0.20: sorted forward 3 of 774370 states in 0.007 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] 1.45: expand forward 3 of 774370 states in 1.080 sec
[mcracetrack] 1.47: sorted forward 4 of 2927418 states in 0.027 sec
[mcracetrack] 2.55: expand backward 3 of 774370 states in 1.082 sec
[mcracetrack] 2.58: sorted backward 4 of 3012268 states in 0.027 sec
[mcracetrack] 6.55: expand forward 4 of 2927418 states in 3.966 sec
[mcracetrack] 6.61: sorted forward 5 of 6616183 states in 0.061 sec
[mcracetrack] 10.70: expand backward 4 of 3012268 states in 4.087 sec
[mcracetrack] 10.77: sorted backward 5 of 7736674 states in 0.070 sec
[mcracetrack] 19.74: expand forward 5 of 6616183 states in 8.978 sec
[mcracetrack] 19.86: sorted forward 6 of 12875980 states in 0.120 sec
[mcracetrack] 30.28: expand backward 5 of 7736674 states in 10.416 sec
[mcracetrack] 30.40: sorted backward 6 of 13215854 states in 0.120 sec
[mcracetrack] 47.73: expand forward 6 of 12875980 states in 17.329 sec
[mcracetrack] 47.89: sorted forward 7 of 17019036 states in 0.159 sec
[mcracetrack] 65.67: expand backward 6 of 13215854 states in 17.785 sec
[mcracetrack] 65.85: sorted backward 7 of 19259877 states in 0.175 sec
[mcracetrack] 88.75: expand forward 7 of 17019036 states in 22.905 sec
[mcracetrack] 88.94: sorted forward 8 of 20874496 states in 0.190 sec
[mcracetrack] 110.47: enlarged backward stack to hold 134217728 states 1 GB
[mcracetrack] 114.81: expand backward 7 of 19259877 states in 25.864 sec
[mcracetrack] 115.06: sorted backward 8 of 27724656 states in 0.253 sec
[mcracetrack] 120.69: enlarged forward stack to hold 134217728 states 1 GB
[mcracetrack] 125.92: 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.151 millions/sec
[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 4.0 GB 100%
[mcracetrack] total maximum allocated memory of 4.0 GB
[mcracetrack] sorting time 1.22 sec 1%
[mcracetrack] expansion time 113.84 sec 90%
[mcracetrack] finished after 125.94 seconds