« Falcon by Helen Macdonald | Main | The Economics of Colonizing Other Planets »

The Die Hard Problem in Alloy 3

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 {
  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

Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.
Author Email (optional):
Author URL (optional):
All HTML will be escaped. Hyperlinks will be created for URLs automatically.