Spinroot

A forum for Spin users

You are not logged in.

#1 2013-01-04 19:54:42

robstewartuk
Member
Registered: 2013-01-04
Posts: 8

unreached states when verifying never claims

Hi,

I'm having difficulty understanding a problem I am having when verifying never claims generating from linear temporal logic formula's. I also do not fully understand the effects of selecting safety/non-progress/acceptance cycles in ispin's "verification" tab, in combination with "use never claim" - and I cannot find documentation in the book to describe the behaviours of these combinations.

I have a few never claims generated with:
$ spin -f ...

I'm uneasy with the amount of "unreached in" statements:
(23 of 83 states)
(32 of 65 states)
(6 of 27 states)
...

On inspection of the states that are not being reached, I can see that these states are reached when I simulate with a given seed. So I'm not sure why spin is not reaching them when trying to validate my never claims. I should perhaps add that it is not finding errors in LTL-generated never claims that I would expect violations to be found in, which gives me reason to be suspicious.

--
Rob

Offline

#2 2013-01-04 23:58:26

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

Re: unreached states when verifying never claims

1. when you use a never claim, spin will search only that part of the statespace that can in principle contain violating executions for the specific claim specified. so it is expected that not all system states are reached in this mode. (it would actually be bad if all states were reached anyway, because we'd probably be doing too much work then)
2. remember to use the -a flag to search for cyclic executions when verifying ltl formula that formalize liveness properties -- if you forget the option and there are violating cyclic executions, they would not be reported

Offline

Board footer

Powered by FluxBB