In the examples included with the TLA+ Tools distribution, Leslie Lamport includes a solution to the so-called Die Hard Problem:
In the movie Die Hard 3, the heros must obtain exactly 4 gallons of water using a 5 gallon jug, a 3 gallon jug and a water faucet.
Today, as an excercise in using the natural numbers in Alloy, I translated the TLA+ solution into Alloy 3:
module tristram/diehard
open util/natural
open util/ordering[State] as SO
/* Define names for Natural numbers Two to Five
(Zero and One are defined in util/natural):
*/
lone sig Two in Natural {}
lone sig Three in Natural {}
lone sig Four in Natural {}
lone sig Five in Natural {}
fact {
Two = inc(One)
Three = inc(Two)
Four = inc(Three)
Five = inc(Four)
}
sig State {
small : Natural,
big : Natural
}
pred init(s : State) {
s.small = Zero
s.big = Zero
}
pred emptysmall(s, s' : State) {
s'.small = Zero
s'.big = s.big
}
pred emptybig(s, s' : State) {
s'.small = s.small
s'.big = Zero
}
pred fillsmall(s, s' : State) {
s'.small = Three
s'.big = s.big
}
pred fillbig(s, s' : State) {
s'.small = s.small
s'.big = Five
}
pred smalltobig(s, s' : State) {
let t = add(s.small,s.big) |
s'.big = if util/natural/lt(t, Five) then t else Five
s'.small = sub(s.small, sub(s'.big, s.big))
}
pred bigtosmall(s, s' : State) {
let t = add(s.small, s.big) |
s'.small = if util/natural/lt(t, Three) then t else Three
s'.big = sub(s.big, sub(s'.small, s.small))
}
fact Traces {
init(SO/first())
all s : State - SO/last() |
let s' = SO/next(s) |
emptysmall(s, s') or
emptybig(s, s') or
fillsmall(s, s') or
fillbig(s, s') or
smalltobig(s, s') or
bigtosmall(s, s')
}
pred show() {
SO/last().small = Four or
SO/last().big = Four
}
/* 7 is the smallest scope for States that gives a solution.
This was found by progressively increasing the scope.
We need scope 9 for the naturals (0..8) because smalltobig
and bigtosmall use the sum of s.small and s.big:
*/
run show for 7 but 9 Natural