せっかくファンクションネットを学んだので、「ハノイの塔」のモデルを作ってみることにします。
ハノイの塔とは
ハノイの塔については、Wikiにアニメーションもあるのでそれを見ていただくのが早いと思いますが、「仕様」を引用します。
以下のルールに従ってすべての円盤を右端の杭に移動させられれば完成。
- 3本の杭と、中央に穴の開いた大きさの異なる複数の円盤から構成される。
- 最初はすべての円盤が左端の杭に小さいものが上になるように順に積み重ねられている。
- 円盤を一回に一枚ずつどれかの杭に移動させることができるが、小さな円盤の上に大きな円盤を乗せることはできない。
ブロックゲームと動きが似ているので、ちょっとした改造で作れそうですね。
モデリングしてみる
改造のポイントは以下の通りです。
- テーブルに相当する置き場所「杭」が3つになるので、プレースも3つにする。
- 持ち上げ動作も、杭ごとにイベントを定義する。
- 杭の一番下における円盤は1つだけなので、
ontableトークンの数に制約を追加する。 - 円盤の大小関係の制約がある。
CとDについては、イベントのガード条件を以下のように定義。
c ・・・ tokenCount(ontableA,0)
d ・・・ x<y
その結果が、以下の通りです。
汚くてビジーですね。おそらく、MISTA（あるいはファンクションネット）の表現力の理解不足による、冗長なモデルだと思います。
たとえば改造点aについて、杭の数と同じだけプレースを用意するのではなく、変数化できそうな気がします。
また改造点bについて、「3つの杭のいずれかに円盤があって、かつアームが円盤をもっていない場合」という論理を表現する方法がわからないため、やむなくイベントも個別に定義したりしています。
MISTAには条件を表現するさまざまな演算子が用意されていますので、このモデルももっとシンプルにリファクタリングできるのではないかと思います。
さらにいうと、「持ち上げた元の場所にもう一度下ろすような遷移は冗長なのでガードしたい」ですし、そもそもholdingというプレースを設けずに、moveみたいなイベントで代替した方がさっぱりするでしょう。
でもまあ・・・とりあえずこれで動くんでね！
シミュレーションしてみる
初期状態は、杭Aに下から5・4・3・2・1の順番で円盤を積まれています。
終了状態は、それを同じ形で杭Cに移した状態になっています。
この条件で Verify Goal State Reachability を実行すると、62手で到達することがわかります。「上げ」「下げ」がセットなので、実質31手。
ハノイの塔の最小手順は、円盤数nに対し2n-1ということなので、このシミュレーション結果は最小手順になっているようですね。
ちなみにn=6でチェックすると、
No path is found to reach the following goal under the given search conditions: [G1] clear(1), on(1, 2), on(2, 3), on(3, 4), on(4, 5), on(5, 6), ontableC(6).
到達できないことになっている・・・。
実際にハノイの塔をやってみると、再帰的な操作になることがわかります。n=5ができるのに、n=6ができないというのはちょっと不思議ですね。
いろいろ試してみたところ、n=6の途中出てくるはずの状態
clear(1), on(1, 2), on(2, 3), on(3, 4), on(4, 5), ontableC(5), clear(6), ontableB(6)
つまり小さい方からn-1枚が重なっていて、一番大きな1枚だけ別の杭にある、という状態には到達できる。またこの途中状態から、定義した終了状態にも到達できる。
推測として、検証するツリーが大きくなりすぎて、n=6は到達不可能と判断したのかな？と。
あるいはこのモデルは単に間違っているのかもしれませんが・・・。
おわりに
ハノイの塔はシンプルなゲームですが、それでもモデルを実装しようとすると暗黙の条件が漏れたりしますし、慣れと試行錯誤が必要です。
モデルの実装とシミュレーションを通じて仕様を固めていくというのは、設計でもテストでも有効だなと感じます。というか楽しいんですよね、モデリングって。
ということで、ツールでのモデリングから、シラバスに戻ってみようと思います。
