前回「Pr: 0 Tr: 6」で探索が切れているように見える部分が気になったので、デバッグしてみました。調べられた感じでは、プロセスの削除順序が関係しているようです。一応、「プロセスは生成順序と逆順で消滅する」と記載のある資料を見つけたのでこの記述の…

今回は2プロセスが動作するサンプルモデルを作成して状態空間の探索を追ってみました。前回と同じように読み解けるかと思いきや、よくわからない動きを見ることとなりました。使用したソースは以下となります。 使用したソースから検証器の実行まで 単に2プ…

SPINの検証器が状態空間をどのように探索しているのかが気になったので、状態ベクトルを出力させながら追ってみました。使用したソースは以下となります。 使用したソースから検証器の実行まで 分岐を2箇所に用意した計4経路を通るような以下のソースを用意…