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)