+++ /dev/null
-make[1]: Entering directory `/home/compudj/repository/trunk/verif/nico-md-merge'
-rm -f pan* trail.out
-cat defines > pan.ltl
-spin -f "!(`cat events_lost.ltl | grep -v ^//`)" >> pan.ltl
-spin -a -X -N pan.ltl model.spin
-Exit-Status 0
-gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=750 -DXUSAFE -DNOFAIR pan.c
-./pan -v -X -m100000 -w21 -a -c1
-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 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 92 byte, depth reached 178, errors: 0
- 117886 states, stored
- 210653 states, matched
- 328539 transitions (= stored+matched)
- 440774 atomic steps
-hash conflicts: 3201 (resolved)
-
-Stats on memory usage (in Megabytes):
- 12.142 equivalent memory usage for states (stored*(State-vector + overhead))
- 8.971 actual memory usage for states (compression: 73.88%)
- state-vector as stored = 64 byte + 16 byte overhead
- 8.000 memory used for hash table (-w21)
- 3.052 memory used for DFS stack (-m100000)
- 19.939 total actual memory usage
-
-unreached in proctype switcher
- line 81, "pan.___", state 8, "(1)"
- line 87, "pan.___", state 15, "write_off = new_off"
- line 84, "pan.___", state 18, "((prev_off!=write_off))"
- line 84, "pan.___", state 18, "else"
- line 97, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit"
- line 103, "pan.___", state 25, "(1)"
- line 98, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))"
- line 98, "pan.___", state 26, "else"
- line 91, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)"
- (7 of 31 states)
-unreached in proctype tracer
- line 177, "pan.___", state 48, "events_lost = (events_lost+1)"
- (1 of 51 states)
-unreached in proctype reader
- (0 of 29 states)
-unreached in proctype cleaner
- (0 of 9 states)
-unreached in proctype :init:
- line 284, "pan.___", state 35, "(run switcher())"
- (1 of 43 states)
-unreached in proctype :never:
- line 307, "pan.___", state 8, "-end-"
- (1 of 8 states)
-
-pan: elapsed time 0.86 seconds
-pan: rate 137076.74 states/second
-pan: avg transition delay 2.6176e-06 usec
-make[1]: Leaving directory `/home/compudj/repository/trunk/verif/nico-md-merge'