SPIN:順次の実行と値

これまで読んだSPIN本のどこかに書かれているかもしれませんが完全にスルーしていた内容を紹介します。(SPINモデル検査入門の8クイーン問題で知りました。)

以下の見出しでわかってしまいますが、以下のモデルを実行した際に
Hello, world!は出力されるでしょうか。

timeoutになる例

seq-stop.pml

byte b = 0;

active proctype p()
{
  b;
  printf("Hello, world!\n");
}

timeoutになる

$ spin seq-stop.pml 
      timeout
#processes: 1
		b = 0
  0:	proc  0 (p:1) seq-stop.pml:5 (state 1)
1 process created

なんとtimeoutになり、Hello, world!は出力されません。

通過する例

bの初期値を変更すると今度はprintfまで進みます。

seq-pass.pml

byte b = 1;

active proctype p()
{
  b;
  printf("Hello, world!\n");
}

通過する

$ spin seq-pass.pml 
      Hello, world!
1 process created

知ってました?