dc45444e |
1 | warning: for p.o. reduction to be valid the never claim must be stutter-invariant |
2 | (never claims generated from LTL formulae are stutter-invariant) |
3 | depth 0: Claim reached state 5 (line 321) |
4 | Depth= 201 States= 1e+06 Transitions= 3.11e+06 Memory= 79.063 t= 25.4 R= 4e+04 |
5 | Depth= 201 States= 2e+06 Transitions= 6.44e+06 Memory= 156.895 t= 46.1 R= 4e+04 |
6 | pan: resizing hashtable to -w21.. done |
7 | |
8 | (Spin Version 5.1.6 -- 9 May 2008) |
9 | + Partial Order Reduction |
10 | |
11 | Full statespace search for: |
12 | never claim + |
13 | assertion violations + (if within scope of claim) |
14 | acceptance cycles + (fairness disabled) |
15 | invalid end states - (disabled by never claim) |
16 | |
17 | State-vector 100 byte, depth reached 203, errors: 0 |
18 | 2590821 states, stored |
19 | 5924281 states, matched |
20 | 8515102 transitions (= stored+matched) |
21 | 9636364 atomic steps |
22 | hash conflicts: 6260639 (resolved) |
23 | |
24 | Stats on memory usage (in Megabytes): |
25 | 286.613 equivalent memory usage for states (stored*(State-vector + overhead)) |
26 | 202.768 actual memory usage for states (compression: 70.75%) |
27 | state-vector as stored = 66 byte + 16 byte overhead |
28 | 8.000 memory used for hash table (-w21) |
29 | 0.305 memory used for DFS stack (-m10000) |
30 | 210.891 total actual memory usage |
31 | |
32 | unreached in proctype switcher |
33 | (0 of 31 states) |
34 | unreached in proctype tracer |
35 | (0 of 51 states) |
36 | unreached in proctype reader |
37 | (0 of 29 states) |
38 | unreached in proctype cleaner |
39 | (0 of 9 states) |
40 | unreached in proctype :init: |
41 | (0 of 47 states) |
42 | unreached in proctype :never: |
43 | line 326, "pan.___", state 8, "-end-" |
44 | (1 of 8 states) |
45 | |
46 | pan: elapsed time 56.4 seconds |
47 | pan: rate 45960.99 states/second |
48 | pan: avg transition delay 6.62e-06 usec |
49 | 23.05user 0.18system 0:56.38elapsed 41%CPU (0avgtext+0avgdata 0maxresident)k |
50 | 0inputs+0outputs (0major+54128minor)pagefaults 0swaps |