Solving Water Jug Problem by Contradiction

The problem

Given two water jugs, of capacity 5 and 3 litters, respectively. How can you get 4 litters water?

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
import           Hedgehog
import Hedgehog.Internal.Property (TestLimit(..))
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

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

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

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

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

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


steps :: Monad m => Gen m [Step]
steps = Gen.list (Range.linear 1 20) (Gen.enum FillBig BigIntoSmall)

prop_solution :: Property
prop_solution = withTests (TestLimit 100000) . property $ do
s <- forAll steps
let (State big small) = execute s
assert $ big /= 4

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 2498 tests and 6 shrinks.

┏━━ /home/albert/Dropbox/dev/program/haskell/src/hello.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 97) (Seed 6197458196003709193 4582823049016921821) <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 test.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 compartively. However, the shrinking mechanism is valuable in practice.