c - PROMELA 如何执行此操作？

Question

byte x;

if
::(x == 0) -> ...
::(x > 0) -> ...
fi

是否有全局变量的默认值？或者模型检查器检查所有可能的交错，也就是说，在这种情况下，将所有可能的状态与(x==0)和一起使用(x>0)。

Answer 1

根据Promela doc，变量默认初始化为零。

检查所有可能的变量初始值将成倍增加状态空间。

Answer 2

像这样做;

if
:: x = 0
:: x = 1
:: x = 2
// if you need more, add more
fi

或者如果你真的想要所有值，0 到 255

byte x = 0;

do
:: x <= 254 -> x++
:: break
od

这将在每次迭代时中断或增加，从而生成所有可能的值。或者，正如您（和我）现在所知道的，使用：

select (i : 0 .. 255)