verif/nico-md-merge/no_events_lost.log

   1 make[1]: Entering directory `/home/compudj/repository/trunk/verif/nico-md-merge'
   2 rm -f pan* trail.out
   3 cat defines > pan.ltl
   4 spin -f "!(`cat no_events_lost.ltl | grep -v ^//`)" >> pan.ltl
   5 spin -a -X -N pan.ltl model.spin
   6 Exit-Status 0
   7 gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=750 -DXUSAFE -DNOFAIR  pan.c
   8 ./pan -v -X -m100000 -w21  -a -c1
   9 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
  10 (never claims generated from LTL formulae are stutter-invariant)
  11 depth 0: Claim reached state 5 (line 302)
  12
  13 (Spin Version 5.1.6 -- 9 May 2008)
  14         + Partial Order Reduction
  15
  16 Full statespace search for:
  17         never claim             +
  18         assertion violations    + (if within scope of claim)
  19         acceptance   cycles     + (fairness disabled)
  20         invalid end states      - (disabled by never claim)
  21
  22 State-vector 92 byte, depth reached 178, errors: 0
  23    117886 states, stored
  24    210653 states, matched
  25    328539 transitions (= stored+matched)
  26    440774 atomic steps
  27 hash conflicts:      3201 (resolved)
  28
  29 Stats on memory usage (in Megabytes):
  30    12.142       equivalent memory usage for states (stored*(State-vector + overhead))
  31     8.971       actual memory usage for states (compression: 73.88%)
  32                 state-vector as stored = 64 byte + 16 byte overhead
  33     8.000       memory used for hash table (-w21)
  34     3.052       memory used for DFS stack (-m100000)
  35    19.939       total actual memory usage
  36
  37 unreached in proctype switcher
  38         line 81, "pan.___", state 8, "(1)"
  39         line 87, "pan.___", state 15, "write_off = new_off"
  40         line 84, "pan.___", state 18, "((prev_off!=write_off))"
  41         line 84, "pan.___", state 18, "else"
  42         line 97, "pan.___", state 21, "commit_count[((prev_off%4)/(4/2))] = tmp_commit"
  43         line 103, "pan.___", state 25, "(1)"
  44         line 98, "pan.___", state 26, "((((((prev_off/4)*4)/2)+(4/2))-tmp_commit))"
  45         line 98, "pan.___", state 26, "else"
  46         line 91, "pan.___", state 29, "tmp_commit = (commit_count[((prev_off%4)/(4/2))]+size)"
  47         (7 of 31 states)
  48 unreached in proctype tracer
  49         line 177, "pan.___", state 48, "events_lost = (events_lost+1)"
  50         (1 of 51 states)
  51 unreached in proctype reader
  52         (0 of 29 states)
  53 unreached in proctype cleaner
  54         (0 of 9 states)
  55 unreached in proctype :init:
  56         line 284, "pan.___", state 35, "(run switcher())"
  57         (1 of 43 states)
  58 unreached in proctype :never:
  59         line 307, "pan.___", state 8, "-end-"
  60         (1 of 8 states)
  61
  62 pan: elapsed time 0.85 seconds
  63 pan: rate 138689.41 states/second
  64 pan: avg transition delay 2.5872e-06 usec
  65 make[1]: Leaving directory `/home/compudj/repository/trunk/verif/nico-md-merge'