Spinroot

A forum for Spin users

You are not logged in.

#1 2012-06-19 11:30:08

shankar_vm
Member
Registered: 2012-06-19
Posts: 2

Help on Spin Verification

Hi,

I am new to spin, I have modeled a system which I want to verify, when I run the verifiable exe(pan.exe) I see that
depth reached is 0, does this mean that there was no verification done at all, if so what could be the reason for depth 0.

Regards,
Shiv

Offline

#2 2012-06-19 15:54:18

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: Help on Spin Verification

it means that there is not even a single executable action in the model -- it blocks immediately.
best way to try this out and see what is or isn't happening is to do random simulations with spin itself first (before generating a pan.c with spin -a).
for instance: spin -p -v -l -g model.pml
and then try to find out why nothing can happen
or post the model here and we can give advice

Offline

#3 2012-06-20 07:26:25

shankar_vm
Member
Registered: 2012-06-19
Posts: 2

Re: Help on Spin Verification

Thanks you, I checked it fixed the problem

Offline

Board footer

Powered by FluxBB