Alloyでいろいろ試してたんですけど、もしかしてこれ迷路とけるのかな？
ということで、とりあえず一本道を定義してみる。
module exec/maze
abstract sig Field{}
one sig F11, F12, F13 extends Field{
conn: set Field
}
pred show{
}
run show
F11、F12、F13というのが移動ブロックというイメージで。とりあえずつながってないインスタンスできた。
じゃあ接続を定義。
fact 迷路{
F12 in F11.conn
F11 + F13 in F12.conn
F12 in F13.conn
}
それぞれF11、F12、F13から移動できる場所を定義。
つながった！
よし、じゃあ迷路を探検するプレイヤーを置いてみましょう。
open util/ordering[Step]
sig Step{}
one sig Player{
place: Field one -> Step
}
時間ごとに動くので、util/orderingでStepを定義して、プレイヤーのPlayerを定義してます。
うーん、なんかよくわかんない。
ProjectionをStepに指定して表示してみます。
ずっとF13にいますね。まあいいか。
最初の位置はF11だと指定しておきます。
fact 初期位置{
Player.place.first = F11
}
よしよし、ちゃんとF11にいます。
んで、そのあとF13に飛んで、そのまま。F13すきやなー
まあ、好き勝手飛び回られても困るんで、つながってるところにしか移動できないようにします。
fact つながってるところにしか移動できない{
all s:Step | let s' = s.next {
Player.place.s' in Player.place.s.conn
}
}
そしたら、あれ、なんかエラーが
This name is ambiguous due to multiple matches: field this/F11
いろいろ悩んだけどよくわかんないんで、Alloyがみつけたインスタンスをテキスト形式で見てみます。
connまわりはこんな感じ。
this/F11={F11$0}
this/F11<:conn={F11$0->F12$0}
this/F12={F12$0}
this/F12<:conn={F12$0->F11$0, F12$0->F13$0}
this/F13={F13$0}
this/F13<:conn={F13$0->F12$0}
よくわからないまでも、テキスト形式のインスタンスを見るとなんとなく問題点がわかったりします。
あ、なんかF11、F12、F13それぞれにconnがありますね。確かにそういう定義にしてます。これらが別々のものとして扱われていたようです。
ということで、connはFieldのフィールドにします。
abstract sig Field{
conn: set Field
}
one sig F11, F12, F13 extends Field{}
これで、ちゃんとインスタンスがみつけられるようになりました。見てみると、F11→F12→F11の順に移動します。
ここで、定義が多くなったときに書きやすいよう、迷路の定義の書き方をかえておきます。
fact 迷路{
F11->F12 +
F12->F11 + F12->F13 +
F13->F12
in conn
}
さて、それでは、F13をゴールとして、Alloyさんがちゃんとゴールにたどりつけるか試してみましょう。
pred show{
some s:Step | Player.place.s=F13
}
きゃあ！ショートカットされたｗ
Alloyさん・・・
まあ、迷路の定義で、その経路を含むことは指定していますが、その経路以外を含まないことは指定してないので、ちゃんと、その経路だけを含むようにしましょう。in じゃなくて=にすればいいみたい。
fact 迷路{
F11->F12 +
F12->F11 + F12->F13 +
F13->F12
= conn
}
これで、ショートカットされずに一歩ずつF11からF13まで進むようになりました。
あとで気づいたのだけど、最初の接続インスタンスで、別候補みると、ショートカットも出てました。Alloyの出した実例は、全部みておいたほうがよさそうです。
じゃあ、もう少し複雑な迷路にしてみましょう。こんな感じの迷路にしてみます。
フィールドの定義を増やします
one sig
F11, F12, F13,
F21, F22, F23,
F31, F32, F33
extends Field{}
で、接続はこんな感じに
fact 迷路{
F11->F12 +
F12->F11 + F12->F13 +
F13->F12 +
F13->F23 +
F21->F22 + F21->F31 +
F22->F21 + F22->F23 + F22->F32 +
F23->F13 + F23->F22 +
F31->F21 +
F32->F22 + F32->F33 +
F33->F32
= conn
}
あとはゴールの位置を変えて実行です。
pred show{
some s:Step | Player.place.s=F33
}
あれ、見つからない。
デフォルトだとインスタンス数が３つまでなんですけど、今回３ステップではゴールみつからないので、10ステップくらい動かしてみましょう。
run show for 10 Step
これで無事7ステップ目でF33にたどり着きました！
論理パズル解決言語Alloyすごいです！問題を定義すれば、勝手に解法をみつけてくれます。
ほかにも「３人が並んでいる。和子の隣に健二がいて、高志は健二の隣にいない。真ん中はだれか」みたいなのも
Alloyは、形式手法とか肩肘はって使うんじゃなくて、論理的な考え事をするときにちょっと試してみるくらいの感覚で使うのがいい気がします。
そうすると、手軽で便利で、そして強力なツールになると思います。
最終的なソースはこんな感じ。
module exec/maze
open util/ordering[Step]
sig Step{}
abstract sig Field{
conn: set Field
}
one sig
F11, F12, F13,
F21, F22, F23,
F31, F32, F33
extends Field{}
one sig Player{
place: Field one -> Step
}
fact 迷路{
F11->F12 +
F12->F11 + F12->F13 +
F13->F12 +
F13->F23 +
F21->F22 + F21->F31 +
F22->F21 + F22->F23 + F22->F32 +
F23->F13 + F23->F22 +
F31->F21 +
F32->F22 + F32->F33 +
F33->F32
= conn
}
fact 初期位置{
Player.place.first = F11
}
fact つながってるところにしか移動できない{
all s:Step | let s' = s.next {
Player.place.s' in Player.place.s.conn
}
}
pred show{
some s:Step | Player.place.s=F33
}
run show for 10 Step
ついでに、上の論理パズル。
open util/ordering[人]
abstract sig 人{}
one sig 和子,健二,高志 extends 人{}
fact 和子の隣に健二がいて{
健二 in (和子.next + 和子.prev)
}
fact 高志は健二の隣にいない{
not 高志 in (健二.next + 健二.prev)
}
pred 真ん中はだれか{
some p:人 | #(p.next + p.prev) = 2
}
run 真ん中はだれか
