Alloyガール 迷宮編 1

僕・Alloyさん・Rubyちゃん

僕: うん、ぶっちゃけ西尾さんの「Alloyガール」のパクりオマージュなんだ。正直ごめんなさい

Alloy: 2重の意味でオマージュよね。高階論理は苦手なのだけど

僕: まあこのほうが注目は集めやすいと思ってね。それからもうひとりの登場人物は…

Ruby: こんにちわっ、Rubyです

僕: 中の人的にそうなるよね

Alloy: 中の人? どういうことかな

僕: まあまあ

迷路を作る

僕: 最近子供が迷路にはまっててね

Alloy: あなた学生なのに子供がいるの?

僕: あっ、えーと親戚の子がね

Alloy: ふうん。

僕: できあいの迷路もいいんだけど、自分で作ってあげようかと思ってね。それで Alloy さんで迷路を作るっていうこともできるんじゃないかと

Ruby: わたしにもできると思いますけど…

僕: もちろんできると思うよ。そういうアルゴリズムを考えるのもおもしろいとは思うのだけど、Alloyさんなら宣言的に制約を記述することで迷路が作れるじゃないかなと思って

Alloy: 「迷路」というのが何を意味しているのかにもよるけど、それを過不足なく指定した制約があればもちろん可能よ

僕: うん。まあとりあえず自然言語で作ろうとしている迷路の仕様を書いてみよう

• 2次元の矩形状に「セル」が並んでいる。この「セル」の集合全体を「盤」とする
• あるセルは上下左右に存在するセルと繋がることができる
• 入口と出口は盤の端のセルにある
• 入口と出口は別のセル

僕: まあとりあえずマンハッタン形状*1でいいだろう。

Alloy: ずいぶん曖昧ね。それにこれだけだとはたしてあなたの言う「迷路」になるかな

僕: いろいろ抜けているのはわかっているけど、それはおいおいやっていこうかと

Ruby: 隣りのセルと繋がっていない場合に、そこに壁があるというイメージですね

僕: そうそう。格子状の構造で、迷路の壁はセルを塗り潰すんじゃなくてセルの間に壁を立てるような感じだ

Ruby: 上のようなのじゃなくて下のようなのってことですね

僕: そうそう

Alloyで迷路を作る

僕: Alloyで2次元の格子状の構造をどう表現するかなんだけど、これも「Alloyガール番外編「イラストロジック」 - 西尾泰和のはてなダイアリー」 が参考になった

Alloy: セルのひとつひとつをシグネチャにせずに Col -> Row -> Color の3項関係を使うと軽くできるということね

Ruby: 二次元配列みたいなものですか?

僕: うーん、まあ全てのColとRowの組み合わせを含むように制約を加えたらそういう理解のしかたもできるかもね。たださっきの仕様による迷路を表現しようとすると、セルには色分けのようなものはなくて、隣接するセルと繋がっているかどうかを関係で表現してあげる必要があるね

Ruby: えーっと、ということはCellオブジェクトみたいなものを作って相互に参照を作ればいいのかな

僕: Alloyだとシグネチャを導入して、2項関係を導入するということになるかな。けどそうすると、結局10x10の迷路だとCellのシグネチャの必要なスコープが100になってしまうね

Ruby: あっ、そうでした。明示的にCellを作っちゃダメなんでした。

僕: ダメってこともないかもしれないけどね。けどとりあえずそれはやめて、Col->Row->Col->Row の4項関係で表現することにしてみよう

Alloy: ...

Ruby: えっ、どういうことですか?

僕: Col、Rowのatomを Alloy の流儀に従って Col$0, Col$1, Row$0 とすると Col$0 -> Row$0 -> Col$1 -> Row$0 というタプルが関係に含まれていたら [ Col$0, Row$0 ] と [ Col$1, Row$0 ] という座標のセルが繋がっていると考えればいいんじゃないかな

Alloy: その場合 Col$1 -> Row$0 -> Col$0 -> Row$0 も含まれるほうが自然でしょうね

僕: あ、そうか、反射的なほうがいいな

Alloy: 正確には反射的という言葉は二項関係にのみ使えるものだけど、擬似的にセル間の2項関係と見做せばその通り

僕: それからさっきRubyちゃんが言ってたように、全てのセルが含まれるようにしたほうがいいかな。よし、こんなのでどうだろう

module maze_maker/simple_maze

open util/ordering[Col] as cols
open util/ordering[Row] as rows

// 迷路のサイズ
fun height : Int {
  10
}
fun width: Int {
  10
}

// 隣接する Cell
fun adjacent (col: Col, row: Row) : Col -> Row {
  col.prev -> row +
  col.next -> row +
  col -> row.prev +
  col -> row.next
}

sig Col {
  paths: Row -> Col -> Row
} {
  // 自分自身との接続はなし
  all row: Row | no (this -> row) & row.paths
  // 接続先は必ず隣接する(4近傍の) Cell
  all row: Row | row.paths in adjacent[this, row]
}
sig Row {}

one sig entrance_x extends Col {}
one sig entrance_y extends Row {}
one sig exit_x extends Col {}
one sig exit_y extends Row {}

//  位置が盤の端
pred edge (col: Col, row: Row) {
  col = cols/first or col = cols/last or row = rows/first or row = rows/last
}

fact {
  // 全ての位置が paths に含まれている
  all col: Col, row: Row | (col -> row) in paths[Col, Row]
  // paths の連結は反射的
  all c1, c2: Col, r1, r2: Row | (c1 -> r1 -> c2 -> r2) in paths => (c2 -> r2 -> c1 -> r1) in paths
  // 入口と出口はいずれも盤面の端に位置する
  edge[entrance_x, entrance_y]
  edge[exit_x, exit_y]
}

run {
  #Col = width
  #Row = height
} for 10

Ruby: おお、なんだかすごいですね!

僕: これをAlloyでExecuteしてみると、Instanceがみつかった

Ruby: ええっ!? なんですかこれ?

僕: AlloyのVisualizerで表示して理解するには無理があるね。大丈夫、AlloyのInstanceはメニューからXMLにダンプできるから、それを読み込んで実際に迷路として描画してみよう。Rubyちゃん、出番だよ

Ruby: はいっ!! えーっと rexml さんと cairo さんを呼び出してっと…できました!!

僕: あ、あれ…?

Alloy: 何? わたしはちゃんと言われた通りの制約を満たす例を上げているよ

僕: あ、そうか、全てのセルが paths に含まれるという制約はあるけど、これは孤立したセルがないというだけで、入口から出口に到達できることを保証はできないのか

Alloy: なんとなくそんな気はしていたんだけど、入口から出口まで繋っている必要があるということね

僕: そうです。それくらい気をきかせてくれても…

Alloy: 何か言った?

僕: いえ、なんでもないです。よし制約を追加するか…と言いたいところだけど、長くなったし今日はここまで

Ruby: 今日はわたしにもできるお仕事があって良かったです

次回：Alloyガール 迷宮編 2 予告

僕: ああーこれじゃだめだった

Alloy: だから高階論理は苦手って言ったでしょ

*1:0,90,180,270度の直線のみでできている