+++ /dev/null
-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
projects / lttv.git / blobdiff