{-# 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. 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 (TestLimit10000) . 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 00 = [FillBig, FillSmall] candidates x 0 = [BigIntoSmall, FillSmall] candidates 0 y = [SmallIntoBig, FillBig] candidates x y = [SmallIntoBig, BigIntoSmall, EmptyBig, EmptySmall]

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.