Solving Water Jug Problem by Contradiction

§The problem

Given unlimited amount of water and two water jugs, of capacity 5 and 3 liters, respectively. Can you get 4 liters of water? If so, how?

§“Ordinary” Solution

Before looking at how to solve it using contradiction, let’s try to tackle normally. Traversing the state graph using breadth-first search should do the job.

{-# LANGUAGE RecordWildCards #-}
import Data.List

data Step = FillBig
          | FillSmall
          | EmptyBig
          | EmptySmall
          | SmallIntoBig
          | BigIntoSmall
          deriving (Show, Eq, Ord, Enum, Bounded)

data State = State
  { bigJug :: Int
  , smallJug :: Int
  } deriving (Show, Eq)

big_capacity = 5
small_capacity = 3

fsm :: State -> Step -> State
fsm s FillBig = s { bigJug = big_capacity }
fsm s FillSmall = s { smallJug = small_capacity }
fsm s EmptyBig = s { bigJug = 0 }
fsm s EmptySmall = s { smallJug = 0 }
fsm (State big small) SmallIntoBig =
    let big' = min big_capacity (big + small) in
    State { bigJug = big'
          , smallJug = small - (big' - big) }
fsm (State big small) BigIntoSmall =
    let small' = min small_capacity (big + small) in
    State { bigJug = big - (small' - small)
          , smallJug = small' }

water_jug :: [Step]
water_jug = loop [(initial, [])]
  where
  initial = State{ bigJug = 0, smallJug = 0 }
  goal (State{..}, _) = bigJug == 4

  loop :: [(State, [Step])] -> [Step]
  loop frontier
    | Just (_, steps) <- find goal frontier = reverse steps
    | otherwise = loop $ concatMap expand frontier

  expand (state, history) = [(fsm state step, step:history) | step <- enumFrom FillBig]

main = do
  print $ water_jug

-- [FillBig,BigIntoSmall,EmptySmall,BigIntoSmall,FillBig,BigIntoSmall]

§Solution (Haskell)

The Haskell version is taken from http://clrnd.com.ar/posts/2017-04-21-the-water-jug-problem-in-hedgehog.html. I pasted the complete version below with minor modification on the list size and the number of test cases before giving up.

{-# LANGUAGE RecordWildCards #-}
import           Hedgehog
import           Hedgehog.Internal.Property (TestLimit(..), ShrinkLimit(..))
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

data Step = FillBig
          | FillSmall
          | EmptyBig
          | EmptySmall
          | SmallIntoBig
          | BigIntoSmall
          deriving (Show, Eq, Ord, Enum, Bounded)

data State = State
  { bigJug :: Int
  , smallJug :: Int
  } deriving (Show, Eq)

initial :: State
initial = State { bigJug = 0, smallJug = 0}

big_capacity = 5
small_capacity = 3

fsm :: State -> Step -> State
fsm s FillBig = s { bigJug = big_capacity }
fsm s FillSmall = s { smallJug = small_capacity }
fsm s EmptyBig = s { bigJug = 0 }
fsm s EmptySmall = s { smallJug = 0 }
fsm (State big small) SmallIntoBig =
    let big' = min big_capacity (big + small) in
    State { bigJug = big'
          , smallJug = small - (big' - big) }
fsm (State big small) BigIntoSmall =
    let small' = min small_capacity (big + small) in
    State { bigJug = big - (small' - small)
          , smallJug = small' }

prop_solution :: Property
prop_solution = withTests (TestLimit 100000) . property $ do
    s <- forAll steps
    let (State big small) = execute s
    assert $ big /= 4
 where
  steps :: Gen [Step]
  steps = Gen.list (Range.linear 1 20) Gen.enumBounded

  execute :: [Step] -> State
  execute = foldl fsm initial

main :: IO ()
main = do
  check prop_solution
  return ()

The output on my box is:

✗ <interactive> failed after 9463 tests and 1 shrink.

     ┏━━ bucket.hs ━━━
  42 ┃ prop_solution :: Property
  43 ┃ prop_solution = withTests (TestLimit 100000) . property $ do
  44 ┃     s <- forAll steps
     ┃     │ [ FillBig
     ┃     │ , BigIntoSmall
     ┃     │ , EmptySmall
     ┃     │ , BigIntoSmall
     ┃     │ , FillBig
     ┃     │ , BigIntoSmall
     ┃     │ ]
  45 ┃     let (State big small) = execute s
  46 ┃     assert $ big /= 4
     ┃     ^^^^^^^^^^^^^^^^^

  This failure can be reproduced by running:
  > recheck (Size 62) (Seed 546476640955800227 5762280480867254161) <property>

The result is pretty good with such a straightforward generator, which essentially picks from all possible steps defined by data Step. However, the number of test cases is rather large. Is there anything we can do to find the contradiction faster? The key insight is that not all semantically valid steps are sensible. For example, when the bug jug is already empty, applying EmpytBig doesn’t make any sense. The “optimized” version below shows that candidates prunes possible steps when at least one of the jug is empty while keeps the original behavior otherwise. Additionally, we give up a path if it’s too deep, reflected by depth > 10.

prop_opt = withTests (TestLimit 10000) . property $ simulate 0 $ initial
  where
    simulate depth s@State{..}
      | depth > 10 = success
      | otherwise = do
        assert $ bigJug /= 4
        step <- forAll $ Gen.element $ candidates bigJug smallJug
        simulate (depth+1) $ fsm s step

    -- only use meaningful actions
    candidates 0 0 = [FillBig, FillSmall]
    candidates x 0 = [BigIntoSmall, FillSmall]
    candidates 0 y = [SmallIntoBig, FillBig]
    candidates x y = [minBound .. maxBound]

The output on my box is:

✗ <interactive> failed after 25 tests.

     ┏━━ /home/albert/Dropbox/dev/program/haskell/src/hello.hs ━━━
  63 ┃ prop_opt = withTests (TestLimit 10000) . property $ simulate 0 $ initial
  64 ┃   where
  65 ┃     simulate depth s@State{..}
  66 ┃       | depth > 10 = success
  67 ┃       | otherwise = do
  68 ┃         assert $ bigJug /= 4
     ┃         ^^^^^^^^^^^^^^^^^^^^
  69 ┃         step <- forAll $ Gen.element $ candidates bigJug smallJug
     ┃         │ FillBig
     ┃         │ BigIntoSmall
     ┃         │ EmptySmall
     ┃         │ BigIntoSmall
     ┃         │ FillBig
     ┃         │ FillBig
     ┃         │ BigIntoSmall
  70 ┃         simulate (depth+1) $ fsm s step
  71 ┃
  72 ┃     -- only use meaningful actions
  73 ┃     candidates 0 0 = [FillBig, FillSmall]
  74 ┃     candidates x 0 = [BigIntoSmall, FillSmall]
  75 ┃     candidates 0 y = [SmallIntoBig, FillBig]
  76 ┃     candidates x y = [minBound .. maxBound]

  This failure can be reproduced by running:
  > recheck (Size 24) (Seed 17320316036822848788 3613693507781047643) <property>

§Solution (SPIN)

byte small, big

byte small_size = 3
byte big_size = 5

init {
loop:
  if
  :: big == 4 ->
      /* should fail, we found one solution */
      assert(false)
  :: else
  fi

  if
  :: small = 0
  :: big = 0
  :: small = small_size
  :: big = big_size
  :: small + big > big_size -> small = (small+big)-big_size; big = big_size
  :: small + big > small_size ->  big = (small+big)-small_size; small = small_size
  :: small + big <= big_size -> big = small + big ; small = 0
  :: small + big <= small_size -> small = small + big ; big = 0
  fi
  assert(big <= big_size && small <= small_size)
  goto loop
}

$ spin -run -O bucket.pml
pan:1: assertion violated 0 (at depth 71)
pan: wrote bucket.pml.trail
...
$ spin -p -t bucket.pml
using statement merging
  1:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
  2:    proc  0 (:init::1) bucket.pml:18 (state 8)      [small = small_size]
  3:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
  4:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
  5:    proc  0 (:init::1) bucket.pml:19 (state 9)      [big = big_size]
  6:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
  7:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
  8:    proc  0 (:init::1) bucket.pml:16 (state 6)      [small = 0]
  9:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
 10:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
 11:    proc  0 (:init::1) bucket.pml:21 (state 13)     [(((small+big)>small_size))]
 12:    proc  0 (:init::1) bucket.pml:21 (state 14)     [big = ((small+big)-small_size)]
 13:    proc  0 (:init::1) bucket.pml:21 (state 15)     [small = small_size]
 14:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
 15:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
 16:    proc  0 (:init::1) bucket.pml:16 (state 6)      [small = 0]
 17:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
 18:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
 19:    proc  0 (:init::1) bucket.pml:23 (state 19)     [(((small+big)<=small_size))]
 20:    proc  0 (:init::1) bucket.pml:23 (state 20)     [small = (small+big)]
 21:    proc  0 (:init::1) bucket.pml:23 (state 21)     [big = 0]
 22:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
 23:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
 24:    proc  0 (:init::1) bucket.pml:19 (state 9)      [big = big_size]
 25:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
 26:    proc  0 (:init::1) bucket.pml:12 (state 3)      [else]
 27:    proc  0 (:init::1) bucket.pml:21 (state 13)     [(((small+big)>small_size))]
 28:    proc  0 (:init::1) bucket.pml:21 (state 14)     [big = ((small+big)-small_size)]
 29:    proc  0 (:init::1) bucket.pml:21 (state 15)     [small = small_size]
 30:    proc  0 (:init::1) bucket.pml:25 (state 24)     [assert(((big<=big_size)&&(small
 31:    proc  0 (:init::1) bucket.pml:9 (state 1)       [((big==4))]
spin: bucket.pml:11, Error: assertion violated
...

§Conclusion

Spin takes less code to solve this problem, but the output is a bit hard to decipher. Property-base testing is a more general technique, so a little more boilerplates comparatively. However, the shrinking mechanism is valuable in practice.