Exit-Status 0 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) depth 0: Claim reached state 5 (line 301) Depth= 198 States= 1e+06 Transitions= 2.9e+06 Memory= 79.649 t= 7.71 R= 1e+05 (Spin Version 5.1.6 -- 9 May 2008) + Partial Order Reduction Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 100 byte, depth reached 200, errors: 0 1295413 states, stored 2540827 states, matched 3836240 transitions (= stored+matched) 4818193 atomic steps hash conflicts: 1991528 (resolved) Stats on memory usage (in Megabytes): 143.307 equivalent memory usage for states (stored*(State-vector + overhead)) 100.700 actual memory usage for states (compression: 70.27%) state-vector as stored = 66 byte + 16 byte overhead 2.000 memory used for hash table (-w19) 0.305 memory used for DFS stack (-m10000) 102.891 total actual memory usage unreached in proctype switcher (0 of 31 states) unreached in proctype tracer (0 of 51 states) unreached in proctype reader (0 of 29 states) unreached in proctype cleaner (0 of 9 states) unreached in proctype :init: (0 of 43 states) unreached in proctype :never: line 306, "pan.___", state 8, "-end-" (1 of 8 states) pan: elapsed time 10.3 seconds pan: rate 125768.25 states/second pan: avg transition delay 2.6849e-06 usec Exit-Status 0 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) depth 0: Claim reached state 5 (line 301) Depth= 198 States= 1e+06 Transitions= 2.9e+06 Memory= 79.649 t= 7.7 R= 1e+05 (Spin Version 5.1.6 -- 9 May 2008) + Partial Order Reduction Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 100 byte, depth reached 200, errors: 0 1295413 states, stored 2540827 states, matched 3836240 transitions (= stored+matched) 4818193 atomic steps hash conflicts: 1991528 (resolved) Stats on memory usage (in Megabytes): 143.307 equivalent memory usage for states (stored*(State-vector + overhead)) 100.700 actual memory usage for states (compression: 70.27%) state-vector as stored = 66 byte + 16 byte overhead 2.000 memory used for hash table (-w19) 0.305 memory used for DFS stack (-m10000) 102.891 total actual memory usage unreached in proctype switcher (0 of 31 states) unreached in proctype tracer (0 of 51 states) unreached in proctype reader (0 of 29 states) unreached in proctype cleaner (0 of 9 states) unreached in proctype :init: (0 of 43 states) unreached in proctype :never: line 306, "pan.___", state 8, "-end-" (1 of 8 states) pan: elapsed time 10.3 seconds pan: rate 125890.48 states/second pan: avg transition delay 2.6823e-06 usec Exit-Status 0 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) depth 0: Claim reached state 3 (line 302) depth 25: Claim reached state 7 (line 307) pan: acceptance cycle (at depth 167) pan: wrote model.spin.trail (Spin Version 5.1.6 -- 9 May 2008) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 100 byte, depth reached 168, errors: 1 43 states, stored 0 states, matched 43 transitions (= stored+matched) 83 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.005 equivalent memory usage for states (stored*(State-vector + overhead)) 0.277 actual memory usage for states (unsuccessful compression: 5822.98%) state-vector as stored = 6739 byte + 16 byte overhead 2.000 memory used for hash table (-w19) 0.305 memory used for DFS stack (-m10000) 2.501 total actual memory usage unreached in proctype switcher line 80, "pan.___", state 8, "(1)" line 75, "pan.___", state 9, "(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))" line 75, "pan.___", state 9, "else" line 86, "pan.___", state 15, "write_off = new_off" line 83, "pan.___", state 18, "((prev_off!=write_off))" line 83, "pan.___", state 18, "else" line 96, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit" line 102, "pan.___", state 25, "(1)" line 97, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))" line 97, "pan.___", state 26, "else" line 90, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)" (8 of 31 states) unreached in proctype tracer line 153, "pan.___", state 34, "((i=size))" line 151, "pan.___", state 46, "i = 0" line 176, "pan.___", state 48, "events_lost = (events_lost+1)" (3 of 51 states) unreached in proctype reader line 201, "pan.___", state 12, "i = 0" line 215, "pan.___", state 23, "i = 0" (2 of 29 states) unreached in proctype cleaner (0 of 9 states) unreached in proctype :init: line 253, "pan.___", state 7, "((i<2))" line 253, "pan.___", state 7, "((i>=2))" line 272, "pan.___", state 29, "((i<4))" line 272, "pan.___", state 29, "((i>=4))" (2 of 43 states) unreached in proctype :never: line 306, "pan.___", state 7, "(!((events_lost!=0)))" line 309, "pan.___", state 9, "-end-" (2 of 9 states) pan: elapsed time 0 seconds Exit-Status 0 warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) depth 0: Claim reached state 5 (line 301) depth 0: Claim reached state 5 (line 302) (Spin Version 5.1.6 -- 9 May 2008) + Partial Order Reduction Full statespace search for: never claim + assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 32 byte, depth reached 0, errors: 0 1 states, stored 0 states, matched 1 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 0.277 actual memory usage for states (unsuccessful compression: 604850.00%) state-vector as stored = 290312 byte + 16 byte overhead 2.000 memory used for hash table (-w19) 0.305 memory used for DFS stack (-m10000) 2.501 total actual memory usage unreached in proctype switcher line 74, "pan.___", state 3, "new_off = (prev_off+size)" line 80, "pan.___", state 8, "(1)" line 75, "pan.___", state 9, "(((((new_off-read_off)>4)&&((new_off-read_off)<(255/2)))||(size==(4/2))))" line 75, "pan.___", state 9, "else" line 71, "pan.___", state 11, "prev_off = write_off" line 86, "pan.___", state 15, "write_off = new_off" line 83, "pan.___", state 18, "((prev_off!=write_off))" line 83, "pan.___", state 18, "else" line 96, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit" line 102, "pan.___", state 25, "(1)" line 97, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))" line 97, "pan.___", state 26, "else" line 90, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)" line 108, "pan.___", state 31, "-end-" (11 of 31 states) unreached in proctype tracer line 122, "pan.___", state 3, "prev_off = write_off" line 130, "pan.___", state 7, "(1)" line 126, "pan.___", state 10, "((((new_off-read_off)>4)&&((new_off-read_off)<(255/2))))" line 126, "pan.___", state 10, "else" line 136, "pan.___", state 14, "write_off = new_off" line 142, "pan.___", state 20, "buffer_use[((prev_off+i)%4)] = 1" line 143, "pan.___", state 21, "i = (i+1)" line 133, "pan.___", state 27, "((prev_off!=write_off))" line 133, "pan.___", state 27, "else" line 156, "pan.___", state 31, "i = (i+1)" line 153, "pan.___", state 34, "((i=size))" line 164, "pan.___", state 39, "commit_count[((prev_off%4)/(4/2))] = tmp_commit" line 170, "pan.___", state 43, "(1)" line 165, "pan.___", state 44, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))" line 165, "pan.___", state 44, "else" line 151, "pan.___", state 46, "i = 0" line 176, "pan.___", state 48, "events_lost = (events_lost+1)" line 178, "pan.___", state 49, "refcount = (refcount-1)" line 173, "pan.___", state 50, "goto end" line 180, "pan.___", state 51, "-end-" (17 of 51 states) unreached in proctype reader line 206, "pan.___", state 5, "buffer_use[((read_off+i)%4)] = 1" line 207, "pan.___", state 6, "i = (i+1)" line 201, "pan.___", state 12, "i = 0" line 220, "pan.___", state 16, "i = (i+1)" line 223, "pan.___", state 22, "read_off = (read_off+(4/2))" line 215, "pan.___", state 23, "i = 0" line 195, "pan.___", state 26, "((((((write_off/(4/2))-(read_off/(4/2)))>0)&&(((write_off/(4/2))-(read_off/(4/2)))<(255/2)))&&(((commit_count[((read_off%4)/(4/2))]-(4/2))-(((read_off/4)*4)/2))==0)))" line 195, "pan.___", state 26, "((read_off>=(4-events_lost)))" line 227, "pan.___", state 29, "-end-" (8 of 29 states) unreached in proctype cleaner line 239, "pan.___", state 3, "(run switcher())" line 236, "pan.___", state 5, "((refcount==0))" line 235, "pan.___", state 8, "((refcount==0))" line 243, "pan.___", state 9, "-end-" (4 of 9 states) unreached in proctype :init: line 256, "pan.___", state 4, "i = (i+1)" line 253, "pan.___", state 7, "((i<2))" line 253, "pan.___", state 7, "((i>=2))" line 266, "pan.___", state 14, "i = (i+1)" line 263, "pan.___", state 17, "((i<4))" line 263, "pan.___", state 17, "((i>=4))" line 269, "pan.___", state 20, "(run reader())" line 270, "pan.___", state 21, "(run cleaner())" line 275, "pan.___", state 25, "(run tracer())" line 272, "pan.___", state 29, "((i<4))" line 272, "pan.___", state 29, "((i>=4))" line 283, "pan.___", state 35, "(run switcher())" line 288, "pan.___", state 43, "-end-" (10 of 43 states) unreached in proctype :never: line 305, "pan.___", state 11, "((events_lost!=0))" line 305, "pan.___", state 11, "(1)" line 311, "pan.___", state 14, "-end-" (2 of 14 states) pan: elapsed time 0 seconds