c - PROMELA 如何执行此操作？

Question

byte x;

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

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

Answer 1

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

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