ヤギ、キャベツ、狼

前回に続いて、抽象によるソフトウェア設計−Alloyではじめる形式手法− の練習問題を考える。

---

A.3.5 「ヤギ、キャベツ、狼」

一人の農夫が、一頭のヤギと、一玉のキャベツと、一匹の狼を川の向こう側に運びたい。しかし彼のボートには一度に一つしか載せるスペースがない。もしヤギをキャベツと一緒にしたまま農夫が離れると、ヤギがキャベツを食べてしまう。もしヤギと狼を一緒にしておくと、ヤギが食べられてしまう。彼はどうすべきか？ Alloyで解け。
(ヒント: Alloyの標準ディストリビューションにはモジュールutil/orderingがあり、全順序を定義できる。)

---

util/orderingの使い方を知らなかったが、他のサンプルプログラムを見てわかった。firstとlastに最初と最後の状態を指定、ある状態から次の状態の変化はnextで指定すればよいらしい。
各状態で可能な農夫の動作は四通りある。(手ぶらで移動、三通りの荷物のどれかと一緒に移動)
nextの状態として、この四通りの状態を選言で並べればよい。

open util/ordering [S]
enum 岸 {こちら, あちら}

-- 状態
sig S {
  人: 岸,
  狼: 岸,
  山羊: 岸,
  キャベツ: 岸
} {
  -- 安全な状態の条件
  狼 != 山羊 or 人 = 狼
  山羊 != キャベツ or 人 = 山羊
}

one sig スタート extends S {} {
  人 = こちら
  狼 = こちら
  山羊 = こちら
  キャベツ = こちら
}
one sig ゴール extends S {} {
  人 = あちら
  狼 = あちら
  山羊 = あちら
  キャベツ = あちら
}

-- 境界条件
fact {
  first = スタート
  last = ゴール
}

-- 移動
fact move {
  all a: S, b: a.next {
    (b.人 != a.人) and (
      (b.狼 = a.狼 && b.山羊 = a.山羊 && b.キャベツ = a.キャベツ) ||
      (b.狼 != a.狼 && b.山羊 = a.山羊 && b.キャベツ = a.キャベツ) ||
      (b.狼 = a.狼 && b.山羊 != a.山羊 && b.キャベツ = a.キャベツ) ||
      (b.狼 = a.狼 && b.山羊 = a.山羊 && b.キャベツ != a.キャベツ)
    )
  }
}

pred show {}
run show for 8

パズル自体の答えは、川渡り問題に載っている。