A forum for Spin users

You are not logged in.

#1 2018-12-03 19:19:35

Registered: 2018-12-02
Posts: 2

Nested if statements inside d_step

Dear all,

I do not understand why the following code fails when verifying:

init {
  int a = 0;

  d_step {
      :: if
        :: a == 1 -> skip;
        :: a == 2 -> skip;

      :: else -> skip;

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


#2 2018-12-03 22:09:05

Registered: 2010-11-18
Posts: 619

Re: Nested if statements inside d_step

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)


#3 2018-12-04 09:36:50

Registered: 2018-12-02
Posts: 2

Re: Nested if statements inside d_step

Great, now I see, thank you very much!


Board footer

Powered by FluxBB