odd verification claim

spin_never_verification.txt

/////////////
// Before
syntax check
  the model contains 7 never claims: never_6, never_5, never_4, never_3, never_2, never_1, never_0
spin -a -o3 model.pml
  the model contains 7 never claims: never_6, never_5, never_4, never_3, never_2, never_1, never_0
  only one claim is used in a verification run
  choose which one with ./pan -N name (defaults to -N never_0)
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNOREDUCE -w -o pan pan.c
./pan -m10000  -a -c1 -N never_6
Pid: 3934
pan: error, VECTORSZ too small, recompile pan.c with -DVECTORSZ=N with N>1028
pan:1: aborting (at depth 282)
pan: wrote hdph_scheduler_one_never_claim.pml.trail

(Spin Version 6.2.3 -- 24 October 2012)
Warning: Search not completed

Full statespace search for:
  never claim           + (never_6)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 1028 byte, depth reached 282, errors: 1
      141 states, stored
       18 states, matched
      159 transitions (= stored+matched)
        1 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.142	equivalent memory usage for states (stored*(State-vector + overhead))
    0.365	actual memory usage for states
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
  128.827	total actual memory usage



pan: elapsed time 0 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"
//////////



////////////
// After
syntax check
spin: nothing to report
spin -a -o3 model.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DNOREDUCE -w -o pan pan.c
./pan -m10000  -a -c1
Pid: 3987
pan: reached -DMEMLIM bound
  1.07368e+09 bytes used
	102400 bytes more needed
	1.07374e+09 bytes limit
hint: to reduce memory, recompile with
  -DCOLLAPSE # good, fast compression, or
  -DMA=1020   # better/slower compression, or
  -DHC # hash-compaction, approximation
  -DBITSTATE # supertrace, approximation

(Spin Version 6.2.3 -- 24 October 2012)
Warning: Search not completed

Full statespace search for:
	never claim         	+ (never_0)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 1020 byte, depth reached 2016, errors: 0
   925973 states, stored
  4010379 states, matched
  4936352 transitions (= stored+matched)
   118346 atomic steps
hash conflicts:     61810 (resolved)

Stats on memory usage (in Megabytes):
  925.464	equivalent memory usage for states (stored*(State-vector + overhead))
  900.665	actual memory usage for states (compression: 97.32%)
         	state-vector as stored = 992 byte + 28 byte overhead
  128.000	memory used for hash table (-w24)
    0.534	memory used for DFS stack (-m10000)
    5.256	memory lost to fragmentation
 1023.944	total actual memory usage



pan: elapsed time 9.27 seconds
No errors found -- did you verify all claims?
////////////