レイトン教授ナゾ配信『ウサギ』ソルバをAlloyで書いた

『レイトン教授 奇跡の仮面』では毎日パズルを配信してくれるんだけど、

レイトン教授と奇跡の仮面(特典なし) - 3DS

その中の『ウサギ』シリーズの1つがどうしても解けなくて、ついAlloyでソルバを書いてしまった。
ムシャクシャしてやった。反省はしていない。

『ウサギ』シリーズの説明はコチラが詳しそう。動画も拝借してみる。

ということで、ソルバを公開してみたりする。
みんなこんなのに頼っちゃダメだよ（はあと）

open util/ordering [Rabbit] as rab

abstract sig Carrot {
  x: Int, y: Int
}
{
  x >= 0
  y >= 0
}

one sig C0_0 extends Carrot { } { x = 0 y = 0 }
one sig C1_0 extends Carrot { } { x = 1 y = 0 }
one sig C2_0 extends Carrot { } { x = 2 y = 0 }
one sig C3_0 extends Carrot { } { x = 3 y = 0 }
one sig C0_1 extends Carrot { } { x = 0 y = 1 }
one sig C2_1 extends Carrot { } { x = 2 y = 1 }
one sig C0_2 extends Carrot { } { x = 0 y = 2 }
one sig C1_2 extends Carrot { } { x = 1 y = 2 }
one sig C3_2 extends Carrot { } { x = 3 y = 2 }
one sig C0_3 extends Carrot { } { x = 0 y = 3 }
one sig C2_3 extends Carrot { } { x = 2 y = 3 }
one sig C4_3 extends Carrot { } { x = 4 y = 3 }
one sig C3_4 extends Carrot { } { x = 3 y = 4 }

run { } for exactly 13 Rabbit

sig Rabbit {
  at: disj Carrot,
  go: Direction 
}
{
  this != last => {
    move [this, this.next]
    go in DOWN => this.next.@go not in UP
    go in UP => this.next.@go not in DOWN
    go in RIGHT=> this.next.@go not in LEFT
    go in LEFT=> this.next.@go not in RIGHT
  }
}

enum Direction { UP, RIGHT, DOWN, LEFT }

pred move (r, r': Rabbit) {
  r.go in UP =>  goUp [r, r']
  r.go in DOWN =>  goDown [r, r']
  r.go in RIGHT =>  goRight [r, r']
  r.go in LEFT =>  goLeft [r, r']
}

pred goUp (r, r': Rabbit) {
  r'.at not in  (r + r.prevs).at
  upper[r'.at, r.at]
  all c: Carrot | upper [c, r.at] => c in r'.at or c in r.prevs.at or upper[c, r'.at]
}
pred goDown (r, r': Rabbit) {
  r'.at not in (r + r.prevs).at
  downer[r'.at, r.at]
  all c: Carrot | downer [c, r.at] => c in r'.at or c in r.prevs.at or downer[c, r'.at]
}
pred goRight (r, r': Rabbit) {
  r'.at not in (r + r.prevs).at
  righter[r'.at, r.at]
  all c: Carrot | righter [c, r.at] => c in r'.at or c in r.prevs.at or righter[c, r'.at]
}
pred goLeft (r, r': Rabbit) {
  r'.at not in (r + r.prevs).at
  lefter[r'.at, r.at]
  all c: Carrot | lefter [c, r.at] => c in r'.at or c in r.prevs.at or lefter[c, r'.at]
}
pred upper (c1, c2: Carrot) {
  c1.x = c2.x
  c1.y < c2.y
}
pred downer (c1, c2: Carrot) {
  c1.x = c2.x
  c1.y > c2.y
}
pred righter (c1, c2: Carrot) {
  c1.x > c2.x
  c1.y = c2.y
}
pred lefter (c1, c2: Carrot) {
  c1.x < c2.x
  c1.y = c2.y
}

Carrotでニンジンの座標を1つ1つ定義して、あと run {} for exactly XX Rabbit の XX にニンジンの数（＝ウサギの動くステップ数）を入れる。

出力はTreeビューだと幾分か見やすいと思う。暇だったら専用ビューワを書くかもしれない。