ヒビルテ(2013-03-27)

2013-03-27 [長年日記]

λ. 「異様に難しいドラクエの謎解き」をモデル検査器で解く

ドラクエ７のバロックの塔 (バロックタワー) の謎解き (ギミック) が異様に難しい。一応自力で解いてみたけど、手数が結構掛かってしまったので、最適なパターンが無いのか気になった。

この手の問題は、昔書いた「油売り算」と同じで、モデル検査器(Model Checker)を使うと簡単に解ける。

モデル検査器というのは何かというと、並行システムとかのような複雑な状態遷移を持つようなシステムに対して、エラー状態に到達しないだとか、デッドロックしないだとかの性質を検証するツールで、逆にそういうことが起こりうる場合には、それに至る状態遷移列を「反例」としして出力するような機能を持っている。そこで、この手の問題の場合、状態と可能な手からなる状態遷移系を考えて、ゴールとなるような状態を「エラー」として、モデル検査器にかけてあげると、ゴールに至る状態遷移列が「反例」として得られる。

ということで、モデル検査器SPINを使って6手が最短であることを確認してみる。まず、以下が検査用の状態遷移系の記述(BaroqueTower.pml)。非決定的に状態遷移を繰り返し、目的の状態になったら表明違反を発生させるように書いておくのがポイント。

/* 0:左の像, 1:上の像, 2:右の像, 3:下の像 */
byte dir[4]

/* 像を時計回りに90度回転させる */
inline rotate(n)
{
  dir[n] = (dir[n] + 1) % 4
}

/* 石から反時計回りに3つの像を回転させる */
/* 0:左上の石, 1:右上の石, 2:右下の石, 3:左下石 */
inline push_button(idx)
{
  atomic{
    rotate(idx)
    rotate((idx+3) % 4)
    rotate((idx+2) % 4)
  }
}

active proctype main()
{
  atomic {
    dir[0] = 3; /* 左の像 */
    dir[1] = 3; /* 上の像 */
    dir[2] = 0; /* 右の像 */
    dir[3] = 0; /* 下の像 */
    printf("[%d,%d,%d,%d]\n", dir[0], dir[1], dir[2], dir[3]);
  }

  /* 非決定的に色々試す */
  do
  :: atomic {
       int k;
       if
       :: true -> k = 0
       :: true -> k = 1
       :: true -> k = 2
       :: true -> k = 3
       fi;
       push_button(k);
       printf("%d -> [%d,%d,%d,%d]\n", k, dir[0], dir[1], dir[2], dir[3]);
     }

     /* 解けたら表明違反が発生するように */
     assert(! (!dir[0] && !dir[1] && !dir[2] && !dir[3]) );
  od
}

これを元に検査器を生成してコンパイルする。

% spin -a BaroqueTower.pml
% gcc -O2 -DREACH -o pan pan.c

こうして生成された検査器には「-i search for shortest path to error」というオプションがあるので、「pan -i」としてエラーに至る最短パスを探させる。結果は BaroqueTower.pml.trail というファイルに書き込まれる。

% pan -i

得られたパスの情報を元にシミュレーションさせる。

% spin -k BaroqueTower.pml.trail BaroqueTower.pml
      [3,3,0,0]
      1 -> [0,0,0,1]
      1 -> [1,1,0,2]
      2 -> [2,2,1,2]
      2 -> [3,3,2,2]
      3 -> [3,0,3,3]
      0 -> [0,0,0,0]
spin: BaroqueTower.pml:46, Error: assertion violated
spin: text of failed assertion: assert(!((((!(dir[0])&&!(dir[1]))&&!(dir[2]))&&!(dir[3]))))
spin: trail ends after 37 steps
#processes: 1
		dir[0] = 0
		dir[1] = 0
		dir[2] = 0
		dir[3] = 0
 37:	proc  0 (main) BaroqueTower.pml:32 (state 29)
1 process created

ということで、最短パス(の一つ)は「右上→右上→右下→右下→左下→左上」(1,1,2,2,3,0)で、6手未満のパスはないことが確認できる。

まあ、これくらいの規模の問題なら、モデル検査器を使わずに、自分で適当にプログラムを書いて状態遷移系を探索しても、大したことはないけれど。