PROMELA 如何执行此操作？答案

【问题标题】：How does PROMELA execute this?PROMELA 如何执行此操作？
【发布时间】：2014-01-14 11:52:28
【问题描述】：

byte x;

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

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

【问题讨论】：

【解决方案1】：

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

检查所有可能的变量初始值将使状态空间呈指数增长。

【讨论】：

但是我怎样才能让模型检查器检查所有可能的状态，即在这种情况下同时检查 (x==0) 和 (x>0)？
你能详细说明一下吗？
SPIN 是 (IIRC) explicit-state 模型检查器（也许他们添加了一些符号验证，但我不确定它是否是最近的），因此模型按照定义执行。您可能正在寻找一些参数化并在模型检查器的两个不同启动中验证这两个选项。
阅读本文，spinroot.com/spin/Man/rand.html。据此，如果变量在进程内声明，则其所有值都由模型检查器在验证模式下进行测试。正是，我在寻找什么。

【解决方案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)

【讨论】：