「モデル検査」のススメ

あれは20世紀が終わろうとしていた、ある日のことだった。私は、Windows用のスクリプトエンジンを書いていたのだが、音源周りの実装に苦慮していた。スクリプトエンジンを複数起動した際に、プロセス同士が協調し、良い具合に音源を排他制御して欲しい。様々な手法を試してみるのだが、どうも上手くいかない。このときは、スクリプトエンジンを複数起動するという機能の優先度が低かったため、大きな問題にはならなかったが、コード書きとして、この時の負けた感じを忘れることはない。

こうした問題は、並列処理の世界では古典的な部類に入る。例えば「食事する哲学者の問題」は有名だろう。「食事する哲学者の問題」の解法には、調停者としてウェイターをおくものがあるが、これはマルチエージェントモデルで「黒板アーキテクチャ」が好まれる理由を示唆している。

90年代以降、デジタル・ゲーム開発では、要求される機能が増え、ソフトウェアとして複雑になった。この複雑さとの戦いにおいて、我々の主力兵器は「実績のある設計」だ。開発経験とともに洗練され、時代に伴って変化した部分はあるが、ソフトウェアとしてのデジタル・ゲームの基本設計は、この20年間変わっていない。ソフトウェア工学におけるアーキテクチャ・パターン、デザイン・パターンが有用であるのと同じように、デジタル・ゲーム開発というドメインに「実績のある設計」があることは、とても心強い。

その一方で、デジタル・ゲームには常に何か新しさが求められる。まれに、優秀なゲームデザインが、既存ソフトウェアの新しい解釈のみによって新規性を実現することがある。この場合は技術的な新規性をゲームに持ち込む必要は無い。が、多くの場合、ゲームとして実現したい新規性はソフトウェアにも新しい複雑さを持ち込む。先に述べた並列処理も、ネットワークを介した多人数プレイや、メニーコアCPUの効率的な活用のために、持ち込まれた複雑さだ。

現在、こうした複雑さを工学的に扱うために「適切な枠組みを設定し、問題を、その枠組み内での探索に帰着させる」という考え方が広く使われている。ソフトウェア工学で言う「形式手法」と呼ばれる分野でも、この考え方が使われている。ここでは、ソフトウェア開発のさまざまな工程で、数学的に厳密な手続きを用いる手法が提案されている。ソフトウェアの振る舞いを網羅的に探索する「モデル検査」も、その一つだ。

この「モデル検査」、実はデジタル・ゲームと非常に相性が良い。デジタル・ゲームは「実績のある設計」の上に、作品毎のシステムが構築されるので、「実績のある設計」の部分の振る舞いは安定しているとみなすことができる。作品毎固有のシステムの部分のみを検証すれば十分であることが多い。例えば、実績があるゲームエンジンを用いてアクションゲームを作る場合、ゲームエンジンの品質は確認済として、登場するオブジェクト間の相互作用のみをモデル化し、検証することが出来る。オンラインゲームであれば、非同期に振る舞うプレイヤ、NPCなどのエージェントが、サーバ上の黒板にアクセスする際、処理のどこまでをアトミックにするべきか、という検証も出来る。また、DSLで表現されるゲームシナリオは進行バグを抱えやすいが、状態遷移モデルとして捉えやすく、「モデル検査」の大好物である。

デジタル・ゲームに、ソフトウェアとしての品質がどの程度求められるかは、経営判断なのかも知れない。でも、遊んでいたゲームが突然止まってしまった時のプレイヤの気持ちを、あなたはよく知っているはずだ。もし、優秀な技術者と、品質のためにコストをかけることが可能な機会があったら、このコラムを思い出して欲しい。