make[1]: Entering directory `/home/compudj/repository/trunk/verif/nico-md-merge'
rm -f pan* trail.out
cat defines > pan.ltl
spin -f "!(`cat no_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.85 seconds
pan: rate 138689.41 states/second
pan: avg transition delay 2.5872e-06 usec
make[1]: Leaving directory `/home/compudj/repository/trunk/verif/nico-md-merge'