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.

dataState = 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' }

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

dataState = 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 (TestLimit100000) . property $ do s <- forAll steps let (State big small) = execute s assert $ big /= 4 where steps :: Gen [Step] steps = Gen.list (Range.linear 120) 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.

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.

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

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