Spinroot

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