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' |