c - PROMELA はこれをどのように実行しますか?

Question

byte x;

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

グローバル変数のデフォルト値はありますか? または、モデル チェッカーは可能なすべてのインターリービングをチェックします。つまり、この場合、 と の両方(x==0)で可能なすべての状態を使用し(x>0)ます。