A forum for Spin users
You are not logged in.
Pages: 1
Dear all,
I do not understand why the following code fails when verifying:
init {
int a = 0;
d_step {
if
:: if
:: a == 1 -> skip;
:: a == 2 -> skip;
fi
:: else -> skip;
fi
}
}
I checked "The Book" and also online description, but I have not found an explanation. The verification output is:
pan:1: blocking sel in d_step (nr.0, near line 8) (at depth 0)
pan: wrote dstep.pml.trail
Why this? The inner if statement should be blocked as whole, right? Then, I assume, the else branch is the only enabled option and should be taken. When using atomic instead of d_step, the verification succeeds as expected (no deadlock, in particular). What am I missing?
I use Spin Version 6.4.8 -- 2 March 2018, but I am sure a similar issue manifested itself in 6.4.7.
Thanks a lot for your time!
Jan Kofron
Offline
It's the way that the first if-selection is encoded in the d_step.
If you omit the nested if-fi and lift the two tests to the top-level if,
then things work as they should.
d_steps are a little tricky in that they expect purely deterministic code,
so when it encounters an if-fi statement that blocks for any reason,
the verifier will complain. The selection in this case has to be available
within the if-fi itself. It's a little more rigid than in general Promela,
so this can indeed be confusing.
Things to do to figure out what's happening can include:
$ spin -run -d spec.pml
to look at the automata structure that is generated (not too helpful
in this case).
And in some cases, look at how the d_step is encoded in C in the
file pan.t that is generated (this file holds the transition tables)
Offline
Great, now I see, thank you very much!
Jan
Offline
Pages: 1