trunk/verif/md/pan.out

   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