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 を使って…ゴニョゴニョ
僕: なお、この連載で使う Alloy と Ruby のスクリプトは GitHub で公開するようにしました
Ruby: できましたっ!!

f:id:alloy_newbie:20140421024539p:plain

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

f:id:alloy_newbie:20140421024601p:plain

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

Alloyガール 迷宮編 3

Alloyの制約パラグラフのリファクタリング

僕: 今日はちょっとしたTipsを紹介しようかなと思う
Alloy: 前回も本題の迷路の生成は進んでなかったと思うけど
僕: いちおう進捗はあるんだけど、その中で気がついたこととか記録しておきたくてね

僕: 迷宮編1 で作ったsimple_maze.alsの制約のうちいくつかは、もっとシンプルに書けるということに気がついたんだ。たとえばこれ

  // 全ての位置が paths に含まれている
  all col: Col, row: Row | (col -> row) in paths[Col, Row]

僕: わざわざ all e | F の形式で書いてるけど、これって結局 Col -> Row が paths[Col, Row] に含まれるってことだからこれでいいはず

  // 全ての位置が paths に含まれている
  Col -> Row in paths[Col, Row]

Alloy: なるほど。おそらく出力されるSATも同一になると思うよ
僕: ただ、Alloyに慣れないうちはこういう書き換えにも慎重になるんだよ。よく勘違いで解がなくなってしまったり、思っていたような制約が効かなくなるという失敗をやるからね
Alloy: わたしは言われた通りに解析しているだけなのだけど
僕: うん、間違っているのは僕なんだけど、まあともかく間違えてないか確認しながら書き換えたい。実はAlloy本を読み返しているとそういうときに使える方法がちゃんと書かれてたよ

  pred constrain1 {
    all col: Col, row: Row | (col -> row) in paths[Col, Row]
  }
  pred constrain2 {
    Col -> Row in paths[Col, Row]
  }
  assert checkConstrainEquality {
    constrain1 iff constrain2
  }
  check checkConstraintEquality for 10 Col, 10 Row

僕: iff は論理式がどちらも真か、どちらも偽の時に真になる二項演算子だ
Alloy: <=> という演算子を使うこともできるわね
僕: まあようするにどちらの制約も同じ意味の時に真になる。これを check で反例がないか確認して、みつからなければ大丈夫だろうと。もちろん指定したスコープの範囲内ではみつからないということだけど
Alloy: 厳密に言うと、fact や signature のブロックにあるその他の制約の元においては同じ結果になるということを確認したことになるのだけどね
僕: というと?
Alloy: つまり、simple_maze.alsに上のassert+checkを追加して検証した場合、"paths の連結は反射的"などのその他の制約を満たすような組み合わせのpathsしか検証の対象にならないのだから、"一般的に"2つの論理式が同じ意味かどうか確認しているわけではないということね
僕: なるほど、そうか。"一般的"に置き換え可能かどうかチェックしようと思ったら上のような検証のためだけのファイルを作ってチェックしたほうがいいんだね
Alloy: 今回のケースでは問題ないようだけどね

Ruby: (今回出番がなかった…)

Alloyガール 迷宮編 2

推移閉包

僕: さて、前回は迷路らしきものを作ることはできたけど、入口から出口まで到達できないという問題があった
Ruby: 条件が足りなかったんですね
僕: A から関係 rel を辿って B まで到達できるというのを表現するイディオムならわかるぞ、Alloy本*1で何度もやったからね

B in A.^rel

僕: こうだ。"^" は関係の「推移閉包」を得る演算子だ
Ruby: すいいへいほう?
僕: えーとつまり rel に含まれる任意の 2つのタプル a -> b と b -> c があったときに、それを連結した a -> c も含むような関係のことだ。

all a, b, c: univ | (a -> b in ^rel && b -> c in ^rel) => a -> c in ^rel

僕: ちなみに "." はちゃんと説明しなかったけど、結合演算子
Ruby: メソッド呼び出しみたいですね
Alloy: それとはまったく別物ですけどね。 A.B は A の関係に含まれるタプルの最後の atom と B の関係に含まれる最初の atom が一致する全組み合わせを連結して、1つの関係にする演算子
僕: A が集合(arity が 1 の関係)で、B が2項関係の場合は A の全要素に B を関数として適用するようなイメージも考えられるけどね
Ruby: 関数ですか?
僕: たとえば B が { 1 -> 1, 2 -> 4, 3 -> 9, 4 -> 16 } というタプルを持つ2項関係だとすると、これは関数みたいじゃない?
Ruby: 1.B = 1, 2.B = 4, 3.B = 9 となるんですね
Alloy: 2項関係が「関数的」という時にはタプルの最初の atom が同じようなタプルが 2つ以上含まれていないという条件があるけどね
Ruby: あっ、そうですね B = { 1 -> 1, 1 -> 2 } のような関係だと 1.B が 1 か 2 かどちらかに決まらないです。でもこういう時はどうなるんですか?
Alloy: だから "." は別に関数適用でもメソッド呼び出しでもないから、ルール通り全ての組み合わせで連結されるだけ。 { 1 } . { 1 -> 1, 1 -> 2 } = { 1, 2 }
僕: そうだね、別の言語でのパラダイムはイメージしやすくするために例として上げるぶんにはいいけど、あくまで関係演算子だということは理解しておかないといけないかもね

僕: さて推移閉包に戻るけど、Alloy の文ではないけどこんな表現もできるね

^rel = rel + rel.rel + rel.rel.rel + rel.rel.rel.rel + ...

Ruby: 再帰的なんですね
僕: えっ?
Ruby: なんとなくメソッドの再帰的呼び出しみたいだなぁって思って
僕: うーんまあ繰り返しが任意の回数続くからそうかもなぁ…あれ?
Ruby: どうかしました?
僕: そうか、推移閉包演算子って「任意回数の繰り返し」が含まれている演算子なんだなぁ
Alloy: そう。推移閉包と反射的推移閉包は Alloy の表現力を高める重要な演算子。処理系内部で関係の展開が行なわれる

4項関係の推移閉包?

Alloy: ところで4項関係の paths でどうやって到達可能性を表現するつもり?
僕: えーっと、こんなふうにできるのかな

  // 全ての位置に入口から到達できる
  all col: Col, row: Row | (col -> row) in (^paths)[entrance_x, entrance_y]

Alloy: 以下のようなエラーになるよ

A type error has occurred:
^ can be used only with a binary relation.
Instead, its possible type(s) are:
{this/Col->this/Row->this/Col->this/Row}

僕: あっ、そうか、推移閉包は2項関係にしか使えないんだ。ええと、それじゃあ fun を使って…

fun reachable (col: Col, row: Row) : Col -> Row {
  col -> row + reachable [adjacent[col, row].Row, Col.(adjacent[col, row])]
}
(...snip...)

  // 全ての位置に入口から到達できる
  all col: Col, row: Row | (col -> row) in reachable [entrance_x, entrance_y]

Alloy: それもだめ。 fun は再帰的な定義はできない

A syntax error has occurred:
fun this/reachable cannot call itself recursively!

僕: そうか、高階論理が使えないというのは、そういうことか…
Alloy: そうね、推移閉包と反射的推移閉包が特別扱いと言えるかもね
Ruby: じゃあ、次はどうしましょう?
僕: え、えーっと…あれっ、もしかして 4項関係にしたのはまずかったかな
Alloy: 前回口を挟んだものかどうか迷ってたのだけど、4項関係だと推移閉包が使えないので記述力は落ちることになるね
僕: あー、あの三点リーダー(…)はそういう事だったのか
Ruby: どうしようもないんでしょうか
僕: いや、こうなったらしかたないから、各座標(タイル)に対応する signature を導入してタイル間の行き来ができることを2項関係で表現してみよう
Ruby: はい! あれ、でもそれって…
僕: そうだね、最初にやめた方法だけど、やってみるしかないね。と、今日はこのくらいにしておこう

お茶の時間

Ruby: なんだか今日はのんびりでしたね
僕: うん、正直いきなり Alloy の文法とか演算子の説明とか何もなしだったのでよくなかったかなぁと思って
Alloy: けど演算子の説明にしても結合演算子に `.` と `[]` の2つあることを抜かしてたりして中途半端ね
僕: そのへんどうしたものかなぁ。詳しくは Alloy 本を読むか、英語なら 公式サイトの Documentation を読んで、ということになるし。
Ruby: 抽象によるソフトウェア設計のリンクを貼っておけばいいですね!
僕: 自分なりに、エッセンスっぽいところをかいつまんでいるつもりだけど、あまり細かい説明を続けても話が続かないし
Alloy: どちらかというと、本題のほうがなかなかうまくいかないから細かい説明で時間稼ぎをしているんじゃないの
僕: うっ…

*1:「抽象によるソフトウェア設計 ―Alloyではじめる形式手法 | コンピュータ・一般書,プログラミング,開発技法 | オーム社Web-Shop」

Alloyガール 迷宮編 1の補遺

集合のサイズの制約 vs スコープ指定

僕: 昨日迷路を生成するために書いたモデル、迷路のサイズを指定するために Col と Row のサイズを指定する制約を書いたんだけど…

(...snip...)
// 迷路のサイズ
fun height : Int {
  10
}
fun width: Int {
  10
}
(...snip...)
run {
  #Col = width[]
  #Row = height[]
} for 10

僕: よく考えてみたら run に与えるスコープの指定でシグネチャのアトムの数が指定できるからこういうふうに書くこともできるんだね

run {} for exactly 10 Row, exactly 10 Col

Alloy: 指定がないシグネチャのスコープは 3になるから、サイズに応じた指定が必要。それと exactly 10 Row は Row の atom がちょうど 10個という意味。exactly がないと10個以下という意味になるのでサイズを指定したい時には exactly が必要ね
僕: この2つの書きかたを比べると、スコープで指定するほうが高速に終わるみたいだ。

(Row, Col のサイズ制約版)
Executing "Run run$1 for 10"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   136722 vars. 10220 primary vars. 244255 clauses. 12438ms.
   Instance found. Predicate is consistent. 330ms.
(スコープによる指定版)
Executing "Run run$1 for exactly 10 Row, exactly 10 Col"
   Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20
   136722 vars. 10220 primary vars. 244255 clauses. 12479ms.
   Instance found. Predicate is consistent. 105ms.

僕: 多分 136722 vars... の行が SAT に変換しているところで、その次が SAT ソルバで制約を充足するインスタンスを探すのにかかった時間だと思うけど、SATへの変換は変数の数は変わってないようだし時間もあまり変化ないね。一方ソルバが解く時間はスコープを使って指定するほうが短いみたいだ
Alloy: 集合のサイズの制約を使うほうでは #Col < width や #Row < height になるような場合も検査した上で棄却するけど、スコープでの指定ではそもそも検査対象にならないから、というところかな
僕: そういうことかなぁ。まあこの例では SAT への変換が時間がかかっているので全体としての影響はあまりないんだけどね
Alloy: これは1つめのインスタンスをみつけるまでの時間だけだから、たくさんのインスタンスの結果を列挙するような場合には次第に影響が大きくなってくるでしょうね
僕: なるほど、じゃあスコープで指定する方法に変えよう

スコープの変更方法

僕: うーん、しかしスコープの指定ってパラメータ化できないのかな
Alloy: スコープの指定には function の呼び出しは使えないね
僕: テンプレート化して .als ファイル自体を生成するしかないのかな…

Alloyガール 迷宮編 1

僕・Alloyさん・Rubyちゃん

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

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

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

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

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

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

僕: まあまあ

迷路を作る

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

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

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

Alloy: ふうん。

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

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

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

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

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

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

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

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

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

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

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

f:id:alloy_newbie:20140319020234p:plain

f:id:alloy_newbie:20140319020248p:plain

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がみつかった

f:id:alloy_newbie:20140319023604p:plain

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

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

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

f:id:alloy_newbie:20140319023957p:plain

僕: あ、あれ…?

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

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

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

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

Alloy: 何か言った?

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

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

 

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

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

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

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