今回は手順を求める問題と、仕様の改善について。
手順を求める例としてはハノイの塔や、舟で川を渡る「ヤギ、キャベツ、狼」等がよく挙げられる。
ここでは「ダイ・ハード３ ジャグ問題」をやってみよう。
問題
Alloy の次に手を出すべきじゃないかと考えている TLA+ の記事 [TLA+] ダイ・ハードジャグ問題から仕様を考える より。
ちょうど4ガロンの水を入れないと爆弾が爆発する
ただし今手元にあるのは3ガロンと5ガロンのジャグしかない
どういう手順を踏めばちょうど4ガロンを測れるか
Alloy で書く
まずちょっと考える
この問題はどんな手順で成り立つのか、少し考えてみる。
３と５を使って４を作り出したいのだから、３＋１か５−１を作れればいいだろう。
思いついた手順はこうだ。
- ５ガロンを汲む
- ３ガロンジャグいっぱいまで移す
５ガロンジャグには２ガロン残っている - ３ガロンジャグを空にする
- ５ガロンジャグから３ガロンジャグに移す
３ガロンジャグには２ガロン入っている - ５ガロンを汲む
- ３ガロンジャグいっぱいまで移す
これで５ガロンジャグに４ガロン残っている。
この手順か、より短い手順を見つけられればよい。
ルールを整理する
上で考えた手順から、こんなことが書ければいいだろう。
前提：
・小さいジャグ（３ガロン）と大きいジャグ（５ガロン）がある
初期状態：
・両ジャグとも空
完了条件：
いずれかを満たす
・大きいジャグに４ガロン入っている
・大きいジャグに１ガロン、小さいジャグに３ガロン入っている
１手順の内容：
いずれかの行動ができる
・小さいジャグいっぱいに水を汲む
・大きいジャグいっぱいに水を汲む
・小さいジャグを空にする
・大きいジャグを空にする
・小さいジャグから大きいジャグに水を移す
大きいジャグいっぱいになったらそこで止める
・大きいジャグから小さいジャグに水を移す
小さいジャグいっぱいになったらそこで止める
書いてみる
Alloyでは、util/orderingを使って順序のある状態を表現できる。
util/ordering [対象]で指定した対象について、first,last,next等が使えるようになる。
これらを使って、Alloy ではこんな風に記述する。
// Die Hard 3 Jugs Problems
open util/ordering [Step]
sig Step {
action: lone Action, // 見やすいように何をしたか記録
small, big: Int // 各Jugに何ガロン入っているか
}
enum Action { FillSmall, FillBig, EmptySmall, EmptyBig, SmallToBig, BigToSmall }
pred complete[s:Step] {
(s.big=4) || (s.big=1 && s.small=3)
}
fact {
// 初期状態
first.small = 0
first.big = 0
no first.action
// 最終状態
last.complete
// Step間遷移
all s,s':Step | s'=s.next =>
fillSmall[s,s'] || fillBig[s,s'] || emptySmall[s,s'] || emptyBig[s,s']
|| smallToBig[s,s'] || bigToSmall[s,s']
}
run {} for 10 Step // どこにあっても同じなので試しやすいここに置いた
let smallCapacity = 3
let bigCapacity = 5
pred fillSmall[s,s':Step] {
s'.action = FillSmall
s'.small = smallCapacity
s'.big = s.big // 変化しないものも明記
}
pred fillBig[s,s':Step] {
s'.action = FillBig
s'.big = bigCapacity
s'.small = s.small
}
pred emptySmall[s,s':Step] {
s'.action = EmptySmall
s'.small = 0
s'.big = s.big
}
pred emptyBig[s,s':Step] {
s'.action = EmptyBig
s'.big = 0
s'.small = s.small
}
pred smallToBig[s,s':Step] {
s'.action = SmallToBig
let move = min[s.small + sub[bigCapacity, s.big]] {
s'.big = s.big.add[move]
s'.small = s.small.sub[move]
}
}
pred bigToSmall[s,s':Step] {
s'.action = BigToSmall
let move = min[s.big + sub[smallCapacity, s.small]] {
s'.small = s.small.add[move]
s'.big = s.big.sub[move]
}
}
s'.big = s.bigといった変化しないものを書くことについて、TLA+ の Lamport 先生はこれは厳密に数学ではなく「That's a bad idea」であると話しているとのこと。
だがこれは数学ではなく、正確に仕様を記述しようという形式仕様記述の話なので問題ないと思う。
（正確に記述し証明するためには数学的であるべきという、形式手法の根本的な主張があるわけだが）
形式仕様記述としては書かれていないことは未定であるという立場を貫くべきで、省略可能にするなら代わりに「他は s と同じ」と書く必要があり（とても書きたい）、しかし s の内容によっては複数の解釈ができる恐れもある。
例えば s.big=s.small+2 だったとして、s'.big が s.big と同じとは「s.small+2」なのか「s'.small+2」なのか？
なおmin[]は Int の集合から最小値を求める関数で、min[m + n]の+は数値の加算ではなく Int 集合への追加だ。
Alloy で+や-が出てきたら、それは集合演算だと考えよう（*はまた全然違う）。
結果
実行すると、例えばこんな成功例を示してくれる。
last.completeを書かなければ、完了状態に至らない失敗例もたくさん挙げてくれる。
run {}時に与える最大Step数を減らしていって、解が見つかる最低手順を特定できる。
仕様を改善する
ネットでよく見る紹介記事では、前項相当で完了する。
確かに最少手順を求める目的は達成したが、それでいいのか？
最少ではない10 Stepを指定した前項の結果例には無駄がある。
無駄を許容する記述をしているので当然だが、無駄の発生しない条件を仕様化したくはないか？
何が無駄か結果例を見てみよう。
まず「Step3とStep4で両ジャグの水量が変わらない」点が目に付く。
それだけか？いや、「Step1とStep4で両ジャグの水量が等しい」のが無駄だ。
両ジャグの水量が等しくなるStepが離れていればいるほど大きな無駄だ。
無駄を排除する
「それがね、Alloyさん。実は他のStepと両ジャグの水量とも等しくなることは、完了状態になるまでなかったんですよ」
// Step間遷移
all s:Step-last | let s'=s.next {
s.complete => {
no s'.action
s'.small = s.small
s'.big = s.big
} else {
fillSmall[s,s'] || fillBig[s,s'] || emptySmall[s,s'] || emptyBig[s,s']
|| smallToBig[s,s'] || bigToSmall[s,s']
}
}
// ループ排除：未完了状態では、他Stepと両ジャグの水量が等しくなることはない
no disj s,s':Step | (!s'.complete) && (s.small = s'.small) && (s.big = s'.big)
最大Step以前に完了した場合に備え、「完了後は何もしない」記述を追加。
ループ排除の記述を追加。
無駄手順例は挙げられなくなり、指定Step数より少ない手順があることが見えやすくなった。
別な問題に読み替える
この問題は「３と５と＋とーを使って４を作りたい」と読み替えられる。
例）最初に挙げた手順なら、5-(3-(5-3))
そちら方向で解いてみるのも面白いかもしれない。
ただしジャグが１つずつしかない本問題では、式に現れない 手順3.や4. のような手間が必要になる。
また問題とあまり似ていない読み替えをすると、結局元の問題ではどうすればいいの？となるので注意。
参考
蛇足
TLA+ の VS Code プラグイン もすごくいい。
Amazon AWS で効果をあげた記事（参考）などを読んで興味を持ったら、調べてみるのもよいだろう。