Error: VECTORSZ is too small

Question

I am new to working with Promela and in particular SPIN. I have a model which I am trying verify and can't understand SPIN's output to resolve the problem.

Here is what I did:

spin -a untitled.pml
gcc -o pan pan.c
./pan

The output was as follows:

pan:1: VECTORSZ is too small, edit pan.h (at depth 0)
pan: wrote untitled.pml.trail

(Spin Version 6.4.5 -- 1 January 2016)
Warning: Search not completed
+ Partial Order Reduction

Full statespace search for:
  never claim           - (none specified)
  assertion violations  +
  acceptance   cycles   - (not selected)
  invalid end states    +

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

I then ran SPIN again to try to determine the cause of the problem by examining the trail file. I used this command:

spin -t -v -p untitled.pml

This was the result:

using statement merging
spin: trail ends after -4 steps
#processes: 1
( global variable dump omitted )
-4: proc  0 (:init::1) untitled.pml:173 (state 1)
1 process created

According to this output (as I understand it), the verification is failing during the "init" procedure. The relevant code from within untitled.pml is this:

init {
  int count = 0;
  int ordinal = N;

  do  // This is line 173
    :: (count < 2 * N + 1) ->

At this point I have no idea what is causing the problem since to me, the "do" statement should execute just fine.

Can anyone please help me in understanding SPINs output so I can remove this error during the verification process? The model does produce the correct output for reference.

Patrick Trentin Patrick Trentin · Accepted Answer · 2017-11-23T13:23:47

You can simply ignore the trail file in this case, it is not relevant at all.

The error message

pan:1: VECTORSZ is too small, edit pan.h (at depth 0)

tells you that the size of directive VECTORSZ is too small to successfully verify your model.

By default, VECTORSZ has size 1024.

To fix this issue, try compiling your verifier with a larger VECTORSZ size:

spin -a untitled.pml
gcc -DVECTORSZ=2048 -o run pan.c
./run

If 2048 doesn't work too, try some more (increasingly larger) values.

Error: VECTORSZ is too small

1 Answers