ノベルゲームの設計段階におけるモデル検査

computer 吉里吉里

http://www.epics.jp/doc/dsw04_seiki.pdf

上の論文のように、モデル検査をゲームのフラグ管理に応用しようという研究は既にあるようですが、ゲームのデータとは別にモデルを作った場合は、ゲームとモデルの一貫性を保つのが困難なため、煩雑さは避けられませんし、また、既存のゲームスクリプトをパースしてモデルに変換するにしても、スクリプト言語のセマンティクスを確立する必要があります。仮に吉里吉里のKAGで後者をやろうとしても、非常に自由度の高い言語ですから、スクリプタをいくら制限しても漏れが出てしまうことはあるでしょう。

そこで、モデルからKAGを吐くやり方はどうかと考えました。シナリオライター（フラグ管理をする人）にUPPAALでモデルを記述させ、そのモデルからKAGに変換するのです。UPPAALならば、プログラミングについてよく知らなくても、代入と分岐さえ分かればモデルを構築できます。何より、ゲームの設計段階において、モデル検査を行うことができるというのが大きな利点ではないでしょうか。

確かにSPINに比べてUPPAALの記述力は高くありませんが、しかし誰にでも使えるGUIが備わっています。Promelaコードをプログラマ以外の人間が書くのは困難ですし、そもそもPromelaコードをKAGスクリプトに変換するのが大変です。UPPAALならば、状態遷移に対するupdateやguardなどがXMLのタグ上できちんと分離されているので、パースは容易です。

スクリプタの記述するスクリプトと、モデルから書き出すスクリプトは完全に別物として扱います。モデルから書き出すスクリプトに人間が手を加えるようなことはあってはなりません。また、スクリプタの記述するスクリプトにおいて分岐先の明示的な記述は基本的になくなります。これは、スクリプトからシナリオを追うのが若干わかりにくくなるというデメリットもあります。ただし、シナリオ構造がある程度複雑なものになるのであれば、モデル検査をしようがしまいが、シナリオとは別にフラグ管理表のようなものが必要になると思われるので、この点はさほど問題にはならないでしょう。テキストそのものと分岐構造の分離をより一層進めれば、モデル検査が容易になるのです。

実際にUPPAALの上でどのような検証式を用いるのかというと、少なくとも、全てのテキストの到達可能性を調べることは基本でしょう。それ以外に関しては、対象のゲームがどのようなゲームであるかによりますね。いつでも告白できるゲームであれば、「同時に2人とは付き合うことができない」など。