Alloyガール 迷宮編 4

Tile signature の導入

僕: さて、第1回で2次元の格子構造の連結関係を Col -> Row -> Col -> Row の4項関係で表現してみたけど、第2回で推移閉包が使えなくて到達可能性の制約を表現できなくって困ってた、というのが前回までのあらすじ
Ruby: 2次元の座標1つに1つの atom を対応させるような signature を導入しようということにしたんでしたよね。けど第1回でその方法は遅くなるからやめとこうってことにしたような…
僕: 西尾さんのイラストロジックの例をみるとどうもそうなりそうだね。けどいちおうやってみよう
Alloy: では座標に対応する Tile という signature を定義して、Col -> Row -> Tile の関係を作りましょう。

sig Tile {}

sig Col {
  tile: Row -> one Tile
}
sig Row {}

僕: Col の宣言パラグラフの "tile: Row -> one Tile" で Col -> Row -> Tile の3項関係が宣言されている。
Ruby: あれ、Col は宣言にあらわれないですね
僕: 関係の宣言は signature の定義のなかでしかできないんだけど、暗黙にその signautre との関係として解釈されるんだよ
Alloy: 上記の title は仮に fact で書きなおすとすると次のようになるね

fact {
  all c: Col | c.tile in Row -> one Tile
}

僕: Tile の atom が全て tile の関係に含まれることと、全ての Tile がただ1つの座標(Col, Row)に対応することを制約に追加する

fact {
  // tile に含まれない Tile はなし
  Tile in tile[Col, Row]
  // Row, Col の組と Tile は必ず1対1対応
  all t: Tile | one tile.t
}

Ruby: あれ、宣言の "Row -> one Tile" の one は1対1対応の制約とは関係ないんですか?
僕: 宣言の Tile の多重度の指定は、「Col -> Row の組み合わせに対して必ず1つだけ Tile が対応する」ことを意味している。けど複数の Col -> Row に同じ Tile が対応することは許してしまっているんだ
Ruby: あ、Tile を1つだけ持ってるけど、それが別の Col -> Row と別々ってことは指定してないってことですね
Alloy: どうしてもオブジェクト指向的な表現になってしまうようね。tile は Col や Row が Tile を「所有している」わけではないのよ
Ruby: ご、ごめんなさい…
僕: 前も話したけど、アナロジーは理解を助けることもあるのでそれで納得できるならいいんじゃないかな。とはいえ 3項関係の多重度の解釈はちょっと難しいよね
Ruby: Tile が tile に全て含まれるっていう制約も必要なんですか?
Alloy: 言われなければわたしは全ての可能性を網羅するわよ
僕: 実のところこの制約は必須というわけではないよね。どの座標にも対応していない余分な Tile があっても、無視するだけだ。けど無視されるだけの atom があっても無駄だし、後でみるように scope で Tile の数は迷路のサイズによって指定するので、全て含まれていて欲しい
Alloy: おそらくこの制約はスコープの指定と他の制約との兼ねあいで自動的に満たされるんだけど、意図を明確にするために書いても特に害はないかな
僕: 次に以前 Col -> Row -> Col -> Row の4項関係として宣言した link は Tile -> Tile の2項関係として宣言する

// 隣接する Tile
fun adjacent (t: Tile) : Tile {
  let col = tile.t.Row, row = tile.t[Col] |
    tile[col.prev, row] +
    tile[col.next, row] +
    tile[col, row.prev] +
    tile[col, row.next]
}

sig Tile {
  link: some Tile
} {
  // 自分自身との接続はなし
  no this & link
  // 接続先は必ず隣接する(4近傍の) Tile
  link in adjacent[this]
}

Ruby: ある Tile に隣接する Tile を表す式を adjacent という function で定義しているんですね。あれ、でもこれ t が盤の端っこだった時が考慮されてないような
Alloy: col.prev, col.next や row.prev, row.next が「存在しない」場合のことを気にしているのなら、その時はたとえば tile[col.prev, row] が空集合になるだけなので自動的に無視されるわ
Ruby: えっと…あ、なるほど、tile[col, row] は row.col.tile と同義で、row や col が空集合({})なら結果も空集合({})で、 '+' は集合和なのでその方向が無視されるだけですね
僕: このへんエッジケースを気にせずに書けるのは関係ベースの記述のいいところだよね

到達可能性の制約

僕: ついに「全てのTileが繋がっている」という制約を追加する

fact {
  // link の連結は反射的
  link = ~link
  // 全ての Tile は link で繋がる
  all t: Tile | t.^link = Tile
}

Ruby: 全ての Tile から到達可能な集合は Tile 全体と同じ、ということですね
僕: これ、冗長なんだよなぁ。link が反射的という制約があるから、どこか1箇所、たとえば入口から到達可能なのが Tile 全体、というだけで自動的に全体が相互に到達可能ってことになるので
Alloy: そうね、1箇所だけでもいいはず
僕: そうしたら早くなる?
Alloy: えっ? えーと…
僕: (まあ筆者の能力を越えた回答は期待できないか) よし、それは次回の宿題ということにしよう。

スコープの設定と計算時間

僕: この他に入口、出口の設定も Tile を使うように書き変えて、全体は以下のようになった

module maze_maker/simple_maze

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

// 隣接する Tile
fun adjacent (t: Tile) : Tile {
  let col = tile.t.Row, row = tile.t[Col] |
    tile[col.prev, row] +
    tile[col.next, row] +
    tile[col, row.prev] +
    tile[col, row.next]
}

sig Tile {
  link: some Tile
} {
  // 自分自身との接続はなし
  no this & link
  // 接続先は必ず隣接する(4近傍の) Tile
  link in adjacent[this]
}

one sig Entrance extends Tile {}
one sig Exit extends Tile {}

sig Col {
  tile: Row -> one Tile
}
sig Row {}

//  Tile が盤の端
pred edge (t: Tile) {
  let col = tile.t.Row, row = tile.t[Col] |
    col = cols/first or col = cols/last or row = rows/first or row = rows/last
}

fact {
  // tile に含まれない Tile はなし
  Tile in tile[Col, Row]
  // Row, Col の組と Tile は必ず1対1対応
  all t: Tile | one tile.t
  // link の連結は反射的
  link = ~link
  // 全ての Tile は link で繋がる
  all t: Tile | t.^link = Tile
  // 入口と出口はいずれも盤面の端に位置する
  edge[Entrance]
  edge[Exit]
}

run {
} for exactly 7 Col, exactly 7 Row, exactly 49 Tile

僕: 今回迷路のサイズは 7x7 にした
Ruby: 前回は 10x10 でしたよね?
僕: うん、すでにネタバレしてる感もあるけど 10x10 だとメモリ不足で落ちちゃったんだ。ヒープサイズを 4096MB まで大きくしたけど。それでどうやら 7x7 が限界だった
Alloy: い、言っておきますけどね、わたしは「小さいスコープでほとんどのモデルの不具合は再現できる」という思想の元で作られているから、スコープを大きく設定して使うのは本来の使いかたじゃないのよ
僕: はい、わかってます。酷使してすみません…。ちなみに1つのインスタンスを生成するのにうちの環境で約20分かかりました
Alloy: 業務で本格的なモデルの検証に使う場合は数時間かけるような計算もざららしいから、まあ計算時間的にはかわいいものね
僕: そうなのか…。まあしばらく流していたらいくつかインスタンスXML を取得できたのでこれも画像化しよう
Ruby: あたしの出番ですねっ!
僕: モデルを変更したので XML の解釈もまた変えないといけないんだ。まあこれも本来の使い途からちょっと離れてるからしかたないね。よろしく
Ruby: はいっ! REXML と rcairo を使って…ゴニョゴニョ
僕: なお、この連載で使う AlloyRubyスクリプトGitHub で公開するようにしました
Ruby: できましたっ!!

f:id:alloy_newbie:20140421024539p:plain

僕: おおっ、なんかそれっぽいな
Ruby: けどなんかこんなのもありました

f:id:alloy_newbie:20140421024601p:plain

僕: ああ、入口と出口が隣り合って繋がってしまっているのか。これは迷路とは言えないなぁ
Ruby: 入口と出口が隣同士じゃないっていう制約が必要ですね
僕: ううーん、そうかな? 入口と出口が隣でも、壁があってすぐに到達できなければそれはそれでいいような気もする
Alloy: 「すぐに到達できない」というのはどういう意味かしら
僕: えーと最短経路で N ステップ以上、とか?
Alloy: なかなか挑戦しがいのありそうな制約ね
Ruby: それに、やっぱり 7x7 だとちょっと簡単すぎるような気はしますね
僕: そうだね、そこもどうするか考えないと
Alloy: 課題は山盛りみたいだけど、最初の成果物としてはこんなものでいいかしら?
僕: うん、小さいながらも迷路っぽいもの"も"作れるモデルを Alloy で作成できたっていうのは、まあおもしろいと思うよ。これを足がかりにもう少し研究してみよう
Ruby: (今日は出番があってよかった)
僕: ではまた次回!