SPIN/PROMELAによるモデルチェッキング

デザインワークショップ( http://www.process.jp/index.php?DW2005) の課題に挑戦し、PROMELAでモデルを記述してみた。経過は以下に置いてある。

いまさらながらですが、formal methodを勉強したからといって、別に完全かつ無矛盾な仕様をスラスラ書けるようになるわけではないのですよね。あらためて痛感しております。