川渡り問題の代表的なひとつが Alloy 本にも載っている。
そして同様の問題が Alloy Tutorial のutil/orderingの項にもある。
今回は自分で書くのではなく、Tutorial のリストを読んでみる。

問題

Alloy本 A.3.5 ヤギ、キャベツ、狼

１人の農夫が、１頭のヤギと、１玉のキャベツと、１匹の狼を川の向こう側に運びたい。
しかし彼のボートには一度に１つしか載せるスペースがない。
もしヤギをキャベツと一緒にしたまま農夫が離れると、ヤギがキャベツを食べてしまう。
もしヤギを狼と一緒にしておくと、ヤギが食べられてしまう。
彼はどうすべきか？

Alloy Tutorial の例

Alloy Tutorial Chapter 2 に Fox,Chicken,Grain の例が載っている。
もちろん正しく書かれたものなのだが、述語crossRiverの記述がとても理解しづらかった。

私がTutorial テキストを読まずコードだけ読んだことは秘密だ。

リスト

AlloyTutorialより

/* Impose an ordering on the State. */
open util/ordering[State]

/* Farmer and his possessions are objects. */
abstract sig Object { eats: set Object }
one sig Farmer, Fox, Chicken, Grain extends Object {}

/* Defines what eats what and the farmer is not around. */
fact { eats = Fox->Chicken + Chicken->Grain}

/* Stores the objects at near and far side of river. */
sig State { near, far: set Object }

/* In the initial state, all objects are on the near side. */
fact { first.near = Object && no first.far }

/* At most one item to move from 'from' to 'to' */
pred crossRiver [from, from', to, to': set Object] {
  one x: from | {
    from' = from - x - Farmer - from'.eats
    to' = to + x + Farmer
  }
}

/* crossRiver transitions between states */
fact {
  all s: State, s': s.next {
    Farmer in s.near =>
      crossRiver [s.near, s'.near, s.far, s'.far]
    else
      crossRiver [s.far, s'.far, s.near, s'.near]
  }
}

/* the farmer moves everything to the far side of the river. */
run { last.far=Object } for exactly 8 State

最大１アイテムと言いながら、なぜxはloneではなくoneなのか。loneに変えてはいけないのか。
よく調べてみるとxにはFarmerが選ばれることもあり、Farmer = xなので何も運ばないケースになる。
loneに変えると、xに要素が割り当てられないときfrom'やto'が不定になる。
言葉にするとxは「何か運ぶ時はそのアイテム、何も運ばない時は農夫自身」であり、結局それって何？となる。

何であるのか簡単に説明できないテクニカルなxを使わず、「いつ何を運ぶか」がわかるように書いた方がよいのではないだろうか。
ここはcrossRiverの細かいテクニックや振る舞いに注目してほしいのではなく、util/orderingの使い方を理解してほしい場面のはずだ。

実行結果

現ソースではステップ実行でも Table View でも、各Stateで何を運んだのか運ばなかったのかわかりづらい。
「彼はどうすべきか」という問題に正面から答えられていないように思う。

TableViewで見る

┌───────────┬────────┐
│this/Object│eats    │
├───────────┼────────┤
│Chicken⁰   │Grain⁰  │
├───────────┼────────┤
│Farmer⁰    │        │
├───────────┼────────┤
│Fox⁰       │Chicken⁰│
├───────────┼────────┤
│Grain⁰     │        │
└───────────┴────────┘
┌──────────┬────────┬────────┐
│this/State│near    │far     │
├──────────┼────────┼────────┤
│State⁰    │Chicken⁰│        │
│          ├────────┤        │
│          │Farmer⁰ │        │
│          ├────────┤        │
│          │Fox⁰    │        │
│          ├────────┤        │
│          │Grain⁰  │        │
├──────────┼────────┼────────┤
│State¹    │Fox⁰    │Chicken⁰│
│          ├────────┼────────┤
│          │Grain⁰  │Farmer⁰ │
├──────────┼────────┼────────┤
│State²    │Farmer⁰ │Chicken⁰│
│          ├────────┼────────┤
│          │Fox⁰    │        │
│          ├────────┤        │
│          │Grain⁰  │        │
├──────────┼────────┼────────┤
│State³    │Fox⁰    │Chicken⁰│
│          ├────────┼────────┤
│          │        │Farmer⁰ │
│          │        ├────────┤
│          │        │Grain⁰  │
├──────────┼────────┼────────┤
│State⁴    │Chicken⁰│Grain⁰  │
│          ├────────┼────────┤
│          │Farmer⁰ │        │
│          ├────────┤        │
│          │Fox⁰    │        │
├──────────┼────────┼────────┤
│State⁵    │Chicken⁰│Farmer⁰ │
│          ├────────┼────────┤
│          │        │Fox⁰    │
│          │        ├────────┤
│          │        │Grain⁰  │
├──────────┼────────┼────────┤
│State⁶    │Chicken⁰│Fox⁰    │
│          ├────────┼────────┤
│          │Farmer⁰ │Grain⁰  │
├──────────┼────────┼────────┤
│State⁷    │        │Chicken⁰│
│          │        ├────────┤
│          │        │Farmer⁰ │
│          │        ├────────┤
│          │        │Fox⁰    │
│          │        ├────────┤
│          │        │Grain⁰  │
└──────────┴────────┴────────┘

改善案

このサンプルとutil/orderingの（ひいては Alloy の）面白さは、農夫がどうすべきかのアルゴリズムを全く書かなくても達成状況を指定すると途中経過を提示してくれる点にある。

ということで、読みこなしやすく結果が見やすいように修正したほうがよいと思う。

修正版リスト

どの段階で何を運ぶのか運ばないのか (move) を State 改め Step に加えた。
改めたのは State より Step の方が順序を持っていることが伝わりやすいと思ったため。
双方向で使えるcrossOverのイディオムは Alloy 本でも多用されているが、読みやすいわけではない。
また、Step に１フィールド増えたためそのまま使うと引数が２つ増える。
初見での読みやすさを重視して fact 内に直接展開した。
動くもの（農夫＋move）がまとまって見えるように、カッコで囲った。
動かないのに食べられて消える eats の意味合いが少しわかりやすくなったのではないか。

改善案

/* Impose an ordering on the Step. */
open util/ordering[Step]

/* Farmer and his possessions are objects. */
abstract sig Object { eats: set Object }
one sig Farmer, Fox, Chicken, Grain extends Object {}

/* Defines what eats what and the farmer is not around. */
fact { eats = Fox->Chicken + Chicken->Grain }

/* Stores cross river transitions. */
sig Step {
    move: lone Object - Farmer,     // At most one item to move by Farmer
    near, far: set Object           // Objects at near and far side of river
}
/* In the initial step, all objects are on the near side. */
fact {
    first.near = Object
    first.far = none
    no first.move    
}

/* cross river transitions between steps. */
fact {
    all s:Step-last, s':s.next {
        Farmer in s.near => {
            s'.move in s.near
            s'.near = s.near - (Farmer + s'.move) - s'.near.eats
            s'.far = s.far + (Farmer + s'.move)
        } else {
            s'.move in s.far
            s'.far = s.far - (Farmer + s'.move) - s'.far.eats
            s'.near = s.near + (Farmer + s'.move)
        }
    }
}

/* the farmer moves everything to the far side of the river. */
run { last.far = Object } for 8 Step

実行結果

TableViewで見る

    ┌───────────┬────────┐
    │this/Object│eats    │
    ├───────────┼────────┤
    │Chicken⁰   │Grain⁰  │
    ├───────────┼────────┤
    │Farmer⁰    │        │
    ├───────────┼────────┤
    │Fox⁰       │Chicken⁰│
    ├───────────┼────────┤
    │Grain⁰     │        │
    └───────────┴────────┘
    ┌─────────┬────────┬────────┬────────┐
    │this/Step│move    │near    │far     │
    ├─────────┼────────┼────────┼────────┤
    │Step⁰    │        │Chicken⁰│        │
    │         │        ├────────┤        │
    │         │        │Farmer⁰ │        │
    │         │        ├────────┤        │
    │         │        │Fox⁰    │        │
    │         │        ├────────┤        │
    │         │        │Grain⁰  │        │
    ├─────────┼────────┼────────┼────────┤
    │Step¹    │Chicken⁰│Fox⁰    │Chicken⁰│
    │         ├────────┼────────┼────────┤
    │         │        │Grain⁰  │Farmer⁰ │
    ├─────────┼────────┼────────┼────────┤
    │Step²    │        │Farmer⁰ │Chicken⁰│
    │         │        ├────────┼────────┤
    │         │        │Fox⁰    │        │
    │         │        ├────────┤        │
    │         │        │Grain⁰  │        │
    ├─────────┼────────┼────────┼────────┤
    │Step³    │Grain⁰  │Fox⁰    │Chicken⁰│
    │         ├────────┼────────┼────────┤
    │         │        │        │Farmer⁰ │
    │         │        │        ├────────┤
    │         │        │        │Grain⁰  │
    ├─────────┼────────┼────────┼────────┤
    │Step⁴    │Chicken⁰│Chicken⁰│Grain⁰  │
    │         ├────────┼────────┼────────┤
    │         │        │Farmer⁰ │        │
    │         │        ├────────┤        │
    │         │        │Fox⁰    │        │
    ├─────────┼────────┼────────┼────────┤
    │Step⁵    │Fox⁰    │Chicken⁰│Farmer⁰ │
    │         ├────────┼────────┼────────┤
    │         │        │        │Fox⁰    │
    │         │        │        ├────────┤
    │         │        │        │Grain⁰  │
    ├─────────┼────────┼────────┼────────┤
    │Step⁶    │        │Chicken⁰│Fox⁰    │
    │         │        ├────────┼────────┤
    │         │        │Farmer⁰ │Grain⁰  │
    ├─────────┼────────┼────────┼────────┤
    │Step⁷    │Chicken⁰│        │Chicken⁰│
    │         ├────────┤        ├────────┤
    │         │        │        │Farmer⁰ │
    │         │        │        ├────────┤
    │         │        │        │Fox⁰    │
    │         │        │        ├────────┤
    │         │        │        │Grain⁰  │
    └─────────┴────────┴────────┴────────┘

余談

最初のコメントを Google 翻訳にかけてみた。
　"Impose an ordering on the State." → "州に命令を下す。"
ああ、うん、そうですね..
いきなり壮大な話になってびっくりした。

参考

Daniel Jackson : 抽象によるソフトウェア設計 ―Alloyではじめる形式手法
Alloy Tutorial