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