A forum for Spin users
You are not logged in.
Pages: 1
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
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
Thanks you, I checked it fixed the problem
Offline
Pages: 1