Promela 中未达到的错误答案

【问题标题】：Unreached error in PromelaPromela 中未达到的错误
【发布时间】：2014-02-02 14:12:17
【问题描述】：

对于以下代码，

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）。至少这是here中写的内容。

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

【问题讨论】：

为什么这个标签是 [c]？

标签： model-checking spin promela

【解决方案1】：

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

select (cond1 : 0..1);

【讨论】：

哎哟。我是“旧时代”的 Spin 用户；不知道最近的select 语法！

【解决方案2】：

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

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

  …
}

【讨论】：