spin - Promela 中的 Select 语句比等效的 if 语句慢得多？

Question

所以我在我的 Promela 代码中使用了以下行。

select( cycles: 26..31 );

但是，它正在引起状态爆炸。我用以下if语句替换它，突然状态爆炸问题消失了。我上面显示的语句不select应该等同于if下面的语句吗？这里发生了什么？

if 
:: cycles = 26;
:: cycles = 27;
:: cycles = 28;
:: cycles = 29;
:: cycles = 30;
:: cycles = 31;
fi;

Answer 1

您的 select 语句由 Spin 转换为

cycles = 26;
do
  :: cycles < 31 -> cycles++
  :: break
od

这意味着，在每个循环执行中，有两种选择的可能性，即转换系统中的两种不同的后继状态。如果没有break选择，则必须进行比较和赋值（两种状态），然后继续。如果你想达到 31 的值，你之前已经进行了 5 次比较和 5 次赋值，而在 if 版本中，赋值只有一个不确定的选择。

我用 spinspider 可视化了两个不同的版本，这应该使问题更容易理解。

下图描述了从带有“if”版本的程序生成的状态空间，其中显然只有 6 种可能性可供选择：

int cycles;

active proctype testWithIf() {
  if 
    :: cycles = 26;
    :: cycles = 27;
    :: cycles = 28;
    :: cycles = 29;
    :: cycles = 30;
    :: cycles = 31;
  fi;

  assert(cycles >= 26 && cycles <= 31);
}

与此相比，从程序生成的图像将您的 select 语句转换为 do-loop：

int cycles;
active proctype test1() {
  cycles = 26;
  do
    :: cycles < 31 -> cycles++
    :: break
  od;

  assert(cycles >= 26 && cycles <= 31);
}

你看到差异了吗？正如我所说，我认为主要问题是，虽然在 if-version 中您只需选择一个分配，但您必须在 do-version 在每个不选择 break 的状态下做多件事：您必须进行比较，增加计数器，然后继续。这显然会产生更大的状态空间。