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)