Spinroot

A forum for Spin users

You are not logged in.

#1 2016-09-24 15:06:02

mlfv
Member
Registered: 2013-04-29
Posts: 28

unreachable code missed by the safety verification

I have a model with some unreachable code which is not reported by the exhaustive search. Does spin find all unreachable states in a model or it may miss some of them?

Offline

#2 2016-09-25 00:55:26

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

Re: unreachable code missed by the safety verification

it should report all of them.
do you have an example?

Offline

#3 2016-09-26 01:01:45

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: unreachable code missed by the safety verification

Yes, see https://www.dropbox.com/s/h94s2r208vucbz0/forecastingExDstepsImp.pml?dl=0

It has two invalid assertions at lines 357 and 365. The safety verification reports no error but doesn't report the unreachable states.

Offline

#4 2016-09-26 17:27:22

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

Re: unreachable code missed by the safety verification

The two asserts are inside d_step statements -- so that means that those individual statements become part of the entire d_step (deterministic step) as one single statement.
That statement (the guard of the d_step) is indeed reachable: it is reached when the do-statement at the start of proctype ForecastingAgent is reached.

Offline

#5 2016-09-26 21:54:31

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: unreachable code missed by the safety verification

So, if e.g. a process has a single statement if or do with all the options enclosed in d_steps then no unreachable code will be reported for that process.  In order to detect an unreachable option it should be enclosed in atomic and e.g. the unguarded part in d_step.

Offline

#6 2016-09-26 22:08:46

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

Re: unreachable code missed by the safety verification

correct.  think of it in terms of the underlying automaton.
a do-loop with only d_steps as the options corresponds to a single state with lots of self-loops.
There's only one state here: the do-loop itself -- all transitions are indivisible steps, with no intermediate states.
If you want to see if the intermediate steps are reachable, you have to make the visible to the verifier.
You can for instance move the d_step beyond the guard:
do :: d_step { guard -> actions } ... od then becomes
do :: guard -> d_step { actions } ... od

Offline

#7 2016-09-26 22:16:16

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: unreachable code missed by the safety verification

Very nice explanation! Thanks.

Offline

Board footer

Powered by FluxBB