1 make[1]: Entering directory `/home/compudj/repository/trunk/verif/nico-md-merge'
4 spin -f "!(`cat no_events_lost.ltl | grep -v ^//`)" >> pan.ltl
5 spin -a -X -N pan.ltl model.spin
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)
13 (Spin Version 5.1.6 -- 9 May 2008)
14 + Partial Order Reduction
16 Full statespace search for:
18 assertion violations + (if within scope of claim)
19 acceptance cycles + (fairness disabled)
20 invalid end states - (disabled by never claim)
22 State-vector 92 byte, depth reached 178, errors: 0
24 210653 states, matched
25 328539 transitions (= stored+matched)
27 hash conflicts: 3201 (resolved)
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
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)"
48 unreached in proctype tracer
49 line 177, "pan.___", state 48, "events_lost = (events_lost+1)"
51 unreached in proctype reader
53 unreached in proctype cleaner
55 unreached in proctype :init:
56 line 284, "pan.___", state 35, "(run switcher())"
58 unreached in proctype :never:
59 line 307, "pan.___", state 8, "-end-"
62 pan: elapsed time 0.85 seconds
63 pan: rate 138689.41 states/second
64 pan: avg transition delay 2.5872e-06 usec
65 make[1]: Leaving directory `/home/compudj/repository/trunk/verif/nico-md-merge'