[lttv.git] / trunk / verif / md / pan.out

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 321)
Depth=     201 States=    1e+06 Transitions= 3.11e+06 Memory=    79.063	t=   25.4 R=   4e+04
Depth=     201 States=    2e+06 Transitions= 6.44e+06 Memory=   156.895	t=   46.1 R=   4e+04
pan: resizing hashtable to -w21..  done

(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 100 byte, depth reached 203, errors: 0
  2590821 states, stored
  5924281 states, matched
  8515102 transitions (= stored+matched)
  9636364 atomic steps
hash conflicts:   6260639 (resolved)

Stats on memory usage (in Megabytes):
  286.613	equivalent memory usage for states (stored*(State-vector + overhead))
  202.768	actual memory usage for states (compression: 70.75%)
         	state-vector as stored = 66 byte + 16 byte overhead
    8.000	memory used for hash table (-w21)
    0.305	memory used for DFS stack (-m10000)
  210.891	total actual memory usage

unreached in proctype switcher
	(0 of 31 states)
unreached in proctype tracer
	(0 of 51 states)
unreached in proctype reader
	(0 of 29 states)
unreached in proctype cleaner
	(0 of 9 states)
unreached in proctype :init:
	(0 of 47 states)
unreached in proctype :never:
	line 326, "pan.___", state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 56.4 seconds
pan: rate  45960.99 states/second
pan: avg transition delay 6.62e-06 usec
23.05user 0.18system 0:56.38elapsed 41%CPU (0avgtext+0avgdata 0maxresident)k
0inputs+0outputs (0major+54128minor)pagefaults 0swaps
Commit	Line	Data
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