Unreached error in Promela

Question

For the following code,

proctype A() 
{ 
byte cond1;

time = time + 1;
time = time + 2;
t[0] = 3;
a[0] = 2;
do
:: (a[0] == 0)->break;
:: else -> a[0] = a[0] - 1;
    do
    :: (t[0] <= t[1])->break;
    od;
    if 
        :: (cond1 != 0) ->
           lock(mutex);
           time = time + 1;
           time = time + 2;
           t[0] = t[0] + 3;
           unlock(mutex);
        :: (cond1 == 0) -> time = time + 1;
    fi
od;
t[0] = 1000;
}

I get the following error,

unreached in proctype A
code.pml:15, state 20, "time = (time+1)"
code.pml:14, state 23, "((mutex==0))"
code.pml:14, state 23, "else"
code.pml:18, state 25, "time = (time+1)"
code.pml:12, state 26, "((mutex==0))"
code.pml:12, state 26, "((mutex==1))"
code.pml:12, state 29, "((mutex==0))"
code.pml:12, state 29, "((mutex==1))"
code.pml:45, state 31, "time = (time+2)"
code.pml:46, state 32, "t[0] = (t[0]+3)"
(7 of 43 states)

Why is that so? Shouldn't Promela execute for every value of cond1 (both cond1 == 0 and cond1 != 0). At least this is what is written in here.

During verifications no such calls are made, because effectively all options for behavior will be explored in this mode, one at a time.

Answer 1

I solved it by using the select statement, like this.

select (cond1 : 0..1);

Answer 2

The initial value of cond1 is zero and it is never changed - either by Spin or by your code. Thus the condition cond1 != 0 is never true. To get that option to execute you'll need to setup the verification to generate other/additional values for cond1 using, for example:

proctype A() 
{ 
  byte cond1;
  if
  :: cond1 = 0;
  :: cond1 = 1;
  /* … */
  fi;

  …
}