(Spin Version 5.1.3 -- 11 December 2007) + Partial Order Reduction + Compression Full statespace search for: never claim - (not selected) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 96 byte, depth reached 1295, errors: 0 9486804 states, stored 6241956 states, matched 15728760 transitions (= stored+matched) 1 atomic steps hash conflicts: 8767391 (resolved) Stats on memory usage (in Megabytes): 1121.868 equivalent memory usage for states (stored*(State-vector + overhead)) 412.481 actual memory usage for states (compression: 36.77%) state-vector as stored = 18 byte + 28 byte overhead 64.000 memory used for hash table (-w23) 0.458 memory used for DFS stack (-m10000) 476.743 total actual memory usage nr of templates: [ globals chans procs ] collapse counts: [ 542065 4481 6650 2 ] unreached in proctype UAC line 96, "pan_in", state 11, "assert(0)" line 105, "pan_in", state 23, "assert(0)" line 107, "pan_in", state 28, "assert(0)" line 137, "pan_in", state 78, "assert(0)" line 169, "pan_in", state 123, "assert(0)" line 187, "pan_in", state 157, "assert(0)" line 191, "pan_in", state 166, "assert(0)" line 192, "pan_in", state 168, "assert(0)" line 193, "pan_in", state 170, "assert(0)" line 198, "pan_in", state 176, "assert(0)" line 220, "pan_in", state 214, "assert(0)" line 237, "pan_in", state 249, "assert(0)" line 240, "pan_in", state 255, "assert(0)" line 249, "pan_in", state 277, "assert(0)" line 251, "pan_in", state 282, "assert(0)" line 271, "pan_in", state 325, "assert(0)" line 272, "pan_in", state 327, "assert(0)" line 273, "pan_in", state 329, "assert(0)" line 274, "pan_in", state 331, "assert(0)" line 275, "pan_in", state 333, "assert(0)" line 276, "pan_in", state 335, "assert(0)" line 277, "pan_in", state 337, "assert(0)" line 278, "pan_in", state 339, "assert(0)" line 279, "pan_in", state 341, "assert(0)" line 280, "pan_in", state 343, "assert(0)" line 281, "pan_in", state 345, "assert(0)" line 282, "pan_in", state 347, "assert(0)" line 283, "pan_in", state 349, "assert(0)" line 284, "pan_in", state 351, "assert(0)" line 285, "pan_in", state 353, "assert(0)" line 287, "pan_in", state 357, "-end-" (31 of 357 states) unreached in proctype UAS line 315, "pan_in", state 10, "assert(0)" line 346, "pan_in", state 61, "assert(0)" line 347, "pan_in", state 63, "assert(0)" line 348, "pan_in", state 65, "assert(0)" line 350, "pan_in", state 70, "assert(0)" line 397, "pan_in", state 161, "assert(0)" line 398, "pan_in", state 163, "assert(0)" line 419, "pan_in", state 206, "assert(0)" line 437, "pan_in", state 244, "assert(0)" line 438, "pan_in", state 246, "assert(0)" line 441, "pan_in", state 252, "assert(0)" line 442, "pan_in", state 254, "assert(0)" line 443, "pan_in", state 256, "assert(0)" line 451, "pan_in", state 273, "assert(0)" line 459, "pan_in", state 291, "assert(0)" line 460, "pan_in", state 293, "assert(0)" line 461, "pan_in", state 295, "assert(0)" line 463, "pan_in", state 300, "assert(0)" line 465, "pan_in", state 304, "-end-" (19 of 304 states) unreached in proctype :init: (0 of 4 states) pan: elapsed time 61.6 seconds pan: rate 154081.6 states/second pan: avg transition delay 3.9145e-06 usec