| dc45444e |
1 | make[1]: Entering directory `/home/compudj/repository/trunk/verif/nico-md-merge' |
| 2 | rm -f pan* trail.out |
| 3 | cat defines > pan.ltl |
| 4 | spin -f "!(`cat commit_sum.ltl | grep -v ^//`)" >> pan.ltl |
| 5 | spin -a -X -N pan.ltl model.spin |
| 6 | Exit-Status 0 |
| 7 | gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=750 -DXUSAFE -DNOFAIR pan.c |
| 8 | ./pan -v -X -m100000 -w21 -a -c1 |
| 9 | warning: for p.o. reduction to be valid the never claim must be stutter-invariant |
| 10 | (never claims generated from LTL formulae are stutter-invariant) |
| 11 | depth 0: Claim reached state 5 (line 302) |
| 12 | |
| 13 | (Spin Version 5.1.6 -- 9 May 2008) |
| 14 | + Partial Order Reduction |
| 15 | |
| 16 | Full statespace search for: |
| 17 | never claim + |
| 18 | assertion violations + (if within scope of claim) |
| 19 | acceptance cycles + (fairness disabled) |
| 20 | invalid end states - (disabled by never claim) |
| 21 | |
| 22 | State-vector 92 byte, depth reached 178, errors: 0 |
| 23 | 117886 states, stored |
| 24 | 210653 states, matched |
| 25 | 328539 transitions (= stored+matched) |
| 26 | 440774 atomic steps |
| 27 | hash conflicts: 3201 (resolved) |
| 28 | |
| 29 | Stats on memory usage (in Megabytes): |
| 30 | 12.142 equivalent memory usage for states (stored*(State-vector + overhead)) |
| 31 | 8.971 actual memory usage for states (compression: 73.88%) |
| 32 | state-vector as stored = 64 byte + 16 byte overhead |
| 33 | 8.000 memory used for hash table (-w21) |
| 34 | 3.052 memory used for DFS stack (-m100000) |
| 35 | 19.939 total actual memory usage |
| 36 | |
| 37 | unreached in proctype switcher |
| 38 | line 81, "pan.___", state 8, "(1)" |
| 39 | line 87, "pan.___", state 15, "write_off = new_off" |
| 40 | line 84, "pan.___", state 18, "((prev_off!=write_off))" |
| 41 | line 84, "pan.___", state 18, "else" |
| 42 | line 97, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit" |
| 43 | line 103, "pan.___", state 25, "(1)" |
| 44 | line 98, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))" |
| 45 | line 98, "pan.___", state 26, "else" |
| 46 | line 91, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)" |
| 47 | (7 of 31 states) |
| 48 | unreached in proctype tracer |
| 49 | line 177, "pan.___", state 48, "events_lost = (events_lost+1)" |
| 50 | (1 of 51 states) |
| 51 | unreached in proctype reader |
| 52 | (0 of 29 states) |
| 53 | unreached in proctype cleaner |
| 54 | (0 of 9 states) |
| 55 | unreached in proctype :init: |
| 56 | line 284, "pan.___", state 35, "(run switcher())" |
| 57 | (1 of 43 states) |
| 58 | unreached in proctype :never: |
| 59 | line 307, "pan.___", state 8, "-end-" |
| 60 | (1 of 8 states) |
| 61 | |
| 62 | pan: elapsed time 0.91 seconds |
| 63 | pan: rate 129545.05 states/second |
| 64 | pan: avg transition delay 2.7698e-06 usec |
| 65 | make[1]: Leaving directory `/home/compudj/repository/trunk/verif/nico-md-merge' |
projects / lttv.git / blame