A forum for Spin users
You are not logged in.
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
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
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
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
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
Very nice explanation! Thanks.
Offline