Solving water pouring puzzle with Alloy

0_readme.md

Water pouring puzzle

Given a 5 quart jug, a 3 quart jug, and unlimited supply of water, can you measure exactly 4 quarts? (The jugs are irregularly shaped, so you can't eyeball half the volume or anything like that.)

The solution involves pouring water between the jugs.

I wanted to see if I could solve this puzzle with Alloy. My first attempt (specific.als) hardcodes the two jugs as named relations. It solves the puzzle (finds a counterexample) in about 500ms.

My second attempt (generic.als) is coded to allow for an arbitrary number of jugs and different sizes. It solves the puzzle in about 2000ms.

I'm interested in feedback on the code for both. In particular:

• Is this idiomatic Alloy?

• When filling or emptying a single jug, is there a nicer way to express that "other jugs are unchanged" than all r: Jug - j | r.(s'.jugAmounts) = r.(s.jugAmounts)?

• Why does the generic code take 4 times as long to solve? Is there a way to make it faster?

generic.als

open util/ordering[State]


sig Jug {
  max: Int
}


sig State {
  jugAmounts: Jug -> one Int
}


fact jugCapacity {
  all s: State {
    all j: s.jugAmounts.univ {
      j.(s.jugAmounts) >= 0
      and j.(s.jugAmounts) <= j.max
    }
  }

  -- jugs start empty
  first.jugAmounts = Jug -> 0
}


pred fill(s, s': State){
  one j: Jug {
    j.(s'.jugAmounts) = j.max
    all r: Jug - j | r.(s'.jugAmounts) = r.(s.jugAmounts)
  }
}


pred empty(s, s': State){
  one j: Jug {
    j.(s'.jugAmounts) = 0
    all r: Jug - j | r.(s'.jugAmounts) = r.(s.jugAmounts)
  }
}


pred pour(s, s': State){
  some x: Int {
    some from, to: Jug {
      from.(s'.jugAmounts) = 0 or to.(s'.jugAmounts) = to.max
      from.(s'.jugAmounts) = minus[from.(s.jugAmounts), x]
      to.(s'.jugAmounts) = plus[to.(s.jugAmounts), x]
      all r: Jug - from - to | r.(s'.jugAmounts) = r.(s.jugAmounts)
    }
  }
}


fact next {
  all s: State, s': s.next {
    fill[s, s']
    or empty[s, s']
    or pour[s, s']
  }
}


fact SpecifyPuzzle{
  all s: State | #s.jugAmounts = 2
  one j: Jug | j.max = 5
  one j: Jug | j.max = 3
}


assert no4 {
  all s: State {
    no a: Jug.(s.jugAmounts) | a = 4
  }
}

check no4 for 7

specific.als

open util/ordering[State]


sig State {
  threeJug: one Int, 
  fiveJug: one Int 
}


fact {
  all s: State {
    s.threeJug >= 0
    s.threeJug <= 3
    s.fiveJug >= 0
    s.fiveJug <= 5
  }

  first.threeJug = 0
  first.fiveJug = 0
}


pred Fill(s, s': State){
  (s'.threeJug = 3 and s'.fiveJug = s.fiveJug)
  or (s'.fiveJug = 5 and s'.threeJug = s.threeJug)
}


pred Empty(s, s': State){
  (s.threeJug > 0 and s'.threeJug = 0 and s'.fiveJug = s.fiveJug)
  or (s.fiveJug > 0 and s'.fiveJug = 0 and s'.threeJug = s.threeJug)
}


pred Pour3To5(s, s': State){
  some x: Int {
    s'.fiveJug = plus[s.fiveJug, x]
    and s'.threeJug = minus[s.threeJug, x]
    and (s'.fiveJug = 5 or s'.threeJug = 0)
  }
}


pred Pour5To3(s, s': State){
  some x: Int {
    s'.threeJug = plus[s.threeJug, x]
    and s'.fiveJug = minus[s.fiveJug, x]
    and (s'.threeJug = 3 or s'.fiveJug = 0)
  }
}


fact Next {
  all s: State, s': s.next {
    Fill[s, s']
    or Pour3To5[s, s']
    or Pour5To3[s, s']
    or Empty[s, s']
  }
}


assert notOne {
  no s: State | s.fiveJug = 4
}


check notOne for 7