model-checking - Promela 中未达到的错误

Question

对于以下代码，

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;
}

我收到以下错误，

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)

为什么呢？Promela 不应该为 cond1 的每个值执行（cond1 == 0 和 cond1 != 0）。至少这是这里写的。

在验证期间，不会进行此类调用，因为在此模式下将有效地探索所有行为选项，一次一个。

Answer 1

我通过使用 select 语句解决了它，就像这样。

select (cond1 : 0..1);

Answer 2

的初始值为cond10，并且永远不会被 Spin 或您的代码更改。因此，条件cond1 != 0永远不会为真。要执行该选项，您需要设置验证以生成其他/附加值以供cond1使用，例如：

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

  …
}