§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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
{-# 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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
{-# 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:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
✗ <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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
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:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
✗ <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)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
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
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
$ 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.