dataState = 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 :: Gen [Step] steps = Gen.list (Range.linear 120) Gen.enumBounded

prop_solution :: Property prop_solution = withTests (TestLimit100000) . 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 9463 tests and 1 shrink.

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 compartively. However, the shrinking mechanism is valuable in practice.