Catra's Diary

_ SPiN その5

「SPINによる設計モデル検証」(近代化学社)参照で、前回の修正。 前回の progress については説明が適切では無かったので。

• 進行性を確認する、つまり繰り返す動作が定義されている中で指定した場所を通らずに無限に処理を継続することが無いか、 一方の処理により他方が飢餓状態に陥ることが無いか、を確認するため、必ず通る事を確認したい居場所に progress ラベルを置く。

• 成立してはいけない性質をオートマトンで記述し、特別なプロセスとして検査したい性質を記述するため、 Never Claim という特別なプロセスを記述する。

  SPIN では有限の記号列、無限の記号列に対応したオートマトンを利用することができる。