で、だいたい動かし方が分かってきたところで PROMELA について、 と行きたい所だが、WEB に結構情報があるので(例えば、Basic Spin Manual など)、 次の例題を考え中。
基本的な形は、複数のプロセスが共通の資源(グローバル変数や channel など)に対して操作を行うモデルを実装し、以下の点を検証する形となる。
処理のその時点で満たすべき条件を確認する。条件を満たさない場合をエラーとして検出する。
assert(判定条件)
デッドロックでは無い終了状態に到達することを確認する。そのために、プログラム中で終了状態とみなす箇所を追加する構文がある。 (何も指定していないと、生成した全てのプロセスが最後まで実行され、かつ全ての channel が空であるときを終了状態とみなす)
end: /* end〜 と言うように end の3文字で始まるユニークな名前のラベルで指定する */
処理が進む(無限ループに陥らない)ことを確認する。そのために、プログラム中のループで処理が進む箇所を示す構文がある。 処理が進まないループがある (= non-progress cycles がある)事を検出するには、pan.c をコンパイルするときのオプションで -DNP を渡し、 pan -l を実行する。
progress: /* progress〜 と言うように progress の8文字で始まるユニークな名前のラベルで指定する */
後はよく分かっていない。