CODEWITHSUNDEEP
formal-verificationmodel-checkingspinformal-methods
Neha
Neha

Reputation: 821

how to resolve max search depth too small in SPIN model checker? What can be the possible reasons?

I am getting this error while doing my model verification, compilation string is

spin -a tesTdma.pml

Max search depth too small, Depth = 9999 states

I do not understand the reason behind this error. Did someone came across this using ISPIN ver 1.1.4 and SPIN 6.4.7

Upvotes: 1

Views: 2271

Answers (1)

0 _
0 _

Reputation: 11484

It appears that the search depth has been bounded, and you need to increase the bound by passing appropriate options to the generated verifier pan:

-b

bounded search mode, makes it an error to exceed the search depth, triggering and error trail

-mN

set max search depth to N steps (default N=10000)

See the man page of pan, and also the man page of spin:

-run

Generate the verifier source code in pan.c (like -a does) and immediately compile and execute the verifier. Options that follow the -run argument are passed through to the compiler (options starting with -[ODUE] or to the verifier as runtime flags (all other options). Options to Spin itself should precede the -run argument.

The -run option is useful if you want to pass the options to pan via the call to spin, instead of separately.

Also, from slide 1 on page 27 in these slides:

SPIN displays “error: max search depth too small” to let you know that the depth bound prevented it from searching the complete statespace.

Upvotes: 3

Related Questions