SPINとPromelaのメモ

mtype は、メッセージタイプの略らしい。　mtype = { ... } という形で宣言される列挙型。定数を宣言。

mtype = { ack, nak, err, next, accept }
と書いたものは
#define ack 5
#define nak 4
#define err 3
#define next 2
#define accept 1
と同義。

★表明　
assertで真偽を判定する。
使い方。Run　Verificationする前に、Basic　Verification　ParametersのSafetyラジオボタンのAssertionsを有効にしておく。

assert（t=1）としたとき、t≠となると実行結果中でerrorが表示される。

★progressラベル
進行性検査（そこに∞回到達するか検査）を行うときに使う。
使い方　Non Progress cycle にチェック入れる。

★公平性を仮定した進行性検査
使い方　Non Progress cycleを選択しWith Weak Fairnessにチェックを入れる。

複数プロセスには公平に実行のチャンスがやってくるという前提のもと検査を行うので、ただの進行性検査よりは検査をパスし易くなる。

★Never Claim
成立してほしくない性質を状態遷移モデルで定義する。
受理（終了状態）になるとエラーとなるように。

使い方　
never{　}で囲んだ中にNeverClaim（成立してほしくない）振る舞いを記述する。

★inline
マクロの定義。
繰り返し同じコードを書く手間を省くのに役立つ。