The problem

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

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
56
{-# 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. 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 some actions are not enabled in certain states. candidates lists the under approximation of all valid actions for a given state.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
prop_opt = withTests (TestLimit 10000) . property $ simulate 0 $ pure initial
where
simulate depth s
| depth > 10 = success
| otherwise = do
State{..} <- s
assert $ bigJug /= 4
step <- forAll $ Gen.element $ candidates bigJug smallJug
simulate (depth+1) $ fmap (flip fsm step) s

-- only use meaningful actions
candidates 0 0 = [FillBig, FillSmall]
candidates x 0 = [BigIntoSmall, FillSmall]
candidates 0 y = [SmallIntoBig, FillBig]
candidates x y = [SmallIntoBig, BigIntoSmall, EmptyBig, EmptySmall]

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 21 tests.

┏━━ bucket.hs ━━━
40 ┃ prop_opt = withTests (TestLimit 10000) . property $ simulate 0 $ pure initial
41 ┃ where
42 ┃ simulate depth s
43 ┃ | depth > 10 = success
44 ┃ | otherwise = do
45 ┃ State{..} <- s
46 ┃ assert $ bigJug /= 4
┃ ^^^^^^^^^^^^^^^^^^^^
47 ┃ step <- forAll $ Gen.element $ candidates bigJug smallJug
┃ │ FillBig
┃ │ BigIntoSmall
┃ │ EmptySmall
┃ │ BigIntoSmall
┃ │ FillBig
┃ │ BigIntoSmall
48 ┃ simulate (depth+1) $ fmap (flip fsm step) s
49 ┃
50 ┃ -- only use meaningful actions
51 ┃ candidates 0 0 = [FillBig, FillSmall]
52 ┃ candidates x 0 = [BigIntoSmall, FillSmall]
53 ┃ candidates 0 y = [SmallIntoBig, FillBig]
54 ┃ candidates x y = [SmallIntoBig, BigIntoSmall, EmptyBig, EmptySmall]

This failure can be reproduced by running:
> recheck (Size 20) (Seed 5595253989157475403 4915698641304675725) <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.