quickcheck-dynamic 3.4.0 → 3.4.1
raw patch · 8 files changed
+288/−128 lines, 8 filesdep +tasty-hunit
Dependencies added: tasty-hunit
Files
- CHANGELOG.md +6/−0
- quickcheck-dynamic.cabal +4/−2
- src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs +10/−6
- src/Test/QuickCheck/StateModel.hs +88/−61
- test/Spec.hs +2/−2
- test/Spec/DynamicLogic/CounterModel.hs +0/−57
- test/Spec/DynamicLogic/Counters.hs +97/−0
- test/Test/QuickCheck/StateModelSpec.hs +81/−0
CHANGELOG.md view
@@ -7,6 +7,12 @@ As a minor extension, we also keep a semantic version for the `UNRELEASED` changes. +## UNRELEASED++## 3.4.1 - 2024-03-22++* [#70](https://github.com/input-output-hk/quickcheck-dynamic/pull/70) Expose `IsPerformResult` typeclass+ ## 3.4.0 - 2024-03-01 * Added some lightweight negative-shrinking based on a simple dependency analysis.
quickcheck-dynamic.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: quickcheck-dynamic-version: 3.4.0+version: 3.4.1 license: Apache-2.0 license-files: LICENSE@@ -90,10 +90,11 @@ main-is: Spec.hs hs-source-dirs: test other-modules:- Spec.DynamicLogic.CounterModel+ Spec.DynamicLogic.Counters Spec.DynamicLogic.Registry Spec.DynamicLogic.RegistryModel Test.QuickCheck.DynamicLogic.QuantifySpec+ Test.QuickCheck.StateModelSpec ghc-options: -rtsopts build-depends:@@ -104,4 +105,5 @@ , quickcheck-dynamic , stm , tasty+ , tasty-hunit , tasty-quickcheck
src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs view
@@ -3,12 +3,16 @@ import Test.QuickCheck -- | This combinator captures the 'smart shrinking' implemented for the--- Smart type wrapper in Test.QuickCheck.Modifiers.+-- `Smart` type wrapper in [Test.QuickCheck.Modifiers](https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Modifiers.html#t:Smart).+-- It interleaves the output of the given shrinker to try to converge to more+-- interesting values faster. shrinkSmart :: (a -> [a]) -> Smart a -> [Smart a]-shrinkSmart shr (Smart i x) = take i' ys `ilv` drop i' ys+shrinkSmart shrinker (Smart i x) = take i' ys `interleave` drop i' ys where- ys = [Smart j y | (j, y) <- [0 ..] `zip` shr x]+ ys = [Smart j y | (j, y) <- [0 ..] `zip` shrinker x]+ i' = 0 `max` (i - 2)- [] `ilv` bs = bs- as `ilv` [] = as- (a : as) `ilv` (b : bs) = a : b : (as `ilv` bs)++ [] `interleave` bs = bs+ as `interleave` [] = as+ (a : as) `interleave` (b : bs) = a : b : (as `interleave` bs)
src/Test/QuickCheck/StateModel.hs view
@@ -2,7 +2,7 @@ {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} --- | Simple (stateful) Model-Based Testing library for use with Haskell QuickCheck.+-- | Model-Based Testing library for use with Haskell QuickCheck. -- -- This module provides the basic machinery to define a `StateModel` from which /traces/ can -- be generated and executed against some /actual/ implementation code to define monadic `Property`@@ -25,12 +25,14 @@ Env, Realized, Generic,+ IsPerformResult, monitorPost, counterexamplePost, stateAfter, runActions, lookUpVar, lookUpVarMaybe,+ viewAtType, initialAnnotatedState, computeNextState, computePrecondition,@@ -191,6 +193,13 @@ instance MonadTrans PostconditionM where lift = PostconditionM . lift +evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()+evaluatePostCondition post = do+ (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post+ monitor mon+ unless b $ monitor onFail+ assert b+ -- | Apply the property transformation to the property after evaluating -- the postcondition. Useful for collecting statistics while avoiding -- duplication between `monitoring` and `postcondition`.@@ -238,23 +247,6 @@ monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property monitoringFailure _ _ _ _ prop = prop -computePostcondition- :: forall m state a- . RunModel state m- => (state, state)- -> ActionWithPolarity state a- -> LookUp m- -> Either (Error state) (Realized m a)- -> PostconditionM m Bool-computePostcondition ss (ActionWithPolarity a p) l r- | p == PosPolarity = case r of- Right ra -> postcondition ss a l ra- -- NOTE: this is actually redundant as this handled- -- at the call site for this function, but this is- -- good hygiene?- Left _ -> pure False- | otherwise = postconditionOnFailure ss a l r- type LookUp m = forall a. Typeable a => Var a -> Realized m a type Env m = [EnvEntry m]@@ -514,47 +506,82 @@ ) => Actions state -> PropertyM m (Annotated state, Env m)-runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions+runActions (Actions_ rejected (Smart _ actions)) = do+ (finalState, env) <- runSteps initialAnnotatedState [] actions+ unless (null rejected) $+ monitor $+ tabulate "Actions rejected by precondition" rejected+ return (finalState, env)++-- | Core function to execute a sequence of `Step` given some initial `Env`ironment+-- and `Annotated` state.+runSteps+ :: forall state m e+ . ( StateModel state+ , RunModel state m+ , e ~ Error state+ , forall a. IsPerformResult e a+ )+ => Annotated state+ -> Env m+ -> [Step state]+ -> PropertyM m (Annotated state, Env m)+runSteps s env [] = return (s, reverse env)+runSteps s env ((v := act) : as) = do+ pre $ computePrecondition s act+ ret <- run $ performResultToEither <$> perform (underlyingState s) action (lookUpVar env)+ let name = show polar ++ actionName action+ monitor $ tabulate "Actions" [name]+ monitor $ tabulate "Action polarity" [show polar]+ case (polar, ret) of+ (PosPolarity, Left err) ->+ positiveActionFailed err+ (PosPolarity, Right val) -> do+ (s', env') <- positiveActionSucceeded ret val+ runSteps s' env' as+ (NegPolarity, _) -> do+ (s', env') <- negativeActionResult ret+ runSteps s' env' as where- loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)- loop _s env [] = do- unless (null rejected) $- monitor $- tabulate "Actions rejected by precondition" rejected- return (_s, reverse env)- loop s env ((v := act) : as) = do- pre $ computePrecondition s act- ret <- run $ performResultToEither <$> perform (underlyingState s) (polarAction act) (lookUpVar env)- let name = show (polarity act) ++ actionName (polarAction act)- monitor $ tabulate "Actions" [name]- monitor $ tabulate "Action polarity" [show $ polarity act]- if- | polarity act == PosPolarity- , Left err <- ret -> do- monitor $- monitoringFailure @state @m- (underlyingState s)- (polarAction act)- (lookUpVar env)- err- stop False- | otherwise -> do- let var = unsafeCoerceVar v- s' = computeNextState s act var- env'- | Right val <- ret = (var :== val) : env- | otherwise = env- monitor $ monitoring @state @m (underlyingState s, underlyingState s') (polarAction act) (lookUpVar env') ret- (b, (Endo mon, Endo onFail)) <-- run- . runWriterT- . runPost- $ computePostcondition @m- (underlyingState s, underlyingState s')- act- (lookUpVar env)- ret- monitor mon- unless b $ monitor onFail- assert b- loop s' env' as+ polar = polarity act++ action = polarAction act++ positiveActionFailed err = do+ monitor $+ monitoringFailure @state @m+ (underlyingState s)+ action+ (lookUpVar env)+ err+ stop False++ positiveActionSucceeded ret val = do+ (s', env', stateTransition) <- computeNewState ret+ evaluatePostCondition $+ postcondition+ stateTransition+ action+ (lookUpVar env)+ val+ pure (s', env')++ negativeActionResult ret = do+ (s', env', stateTransition) <- computeNewState ret+ evaluatePostCondition $+ postconditionOnFailure+ stateTransition+ action+ (lookUpVar env)+ ret+ pure (s', env')++ computeNewState ret = do+ let var = unsafeCoerceVar v+ s' = computeNextState s act var+ env'+ | Right val <- ret = (var :== val) : env+ | otherwise = env+ stateTransition = (underlyingState s, underlyingState s')+ monitor $ monitoring @state @m stateTransition action (lookUpVar env') ret+ pure (s', env', stateTransition)
test/Spec.hs view
@@ -2,9 +2,9 @@ module Main (main) where -import Spec.DynamicLogic.CounterModel qualified import Spec.DynamicLogic.RegistryModel qualified import Test.QuickCheck.DynamicLogic.QuantifySpec qualified+import Test.QuickCheck.StateModelSpec qualified import Test.Tasty main :: IO ()@@ -15,6 +15,6 @@ testGroup "dynamic logic" [ Spec.DynamicLogic.RegistryModel.tests- , Spec.DynamicLogic.CounterModel.tests , Test.QuickCheck.DynamicLogic.QuantifySpec.tests+ , Test.QuickCheck.StateModelSpec.tests ]
− test/Spec/DynamicLogic/CounterModel.hs
@@ -1,57 +0,0 @@-module Spec.DynamicLogic.CounterModel where--import Control.Monad.Reader-import Data.IORef-import Test.QuickCheck-import Test.QuickCheck.Extras-import Test.QuickCheck.Monadic-import Test.QuickCheck.StateModel-import Test.Tasty hiding (after)-import Test.Tasty.QuickCheck--data Counter = Counter Int- deriving (Show, Generic)--deriving instance Show (Action Counter a)-deriving instance Eq (Action Counter a)-instance HasVariables (Action Counter a) where- getAllVariables _ = mempty--instance StateModel Counter where- data Action Counter a where- Inc :: Action Counter ()- Reset :: Action Counter Int-- initialState = Counter 0-- arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)]-- nextState (Counter n) Inc _ = Counter (n + 1)- nextState _ Reset _ = Counter 0--instance RunModel Counter (ReaderT (IORef Int) IO) where- perform _ Inc _ = do- ref <- ask- lift $ modifyIORef ref succ- perform _ Reset _ = do- ref <- ask- lift $ do- n <- readIORef ref- writeIORef ref 0- pure n-- postcondition (Counter n, _) Reset _ res = pure $ n == res- postcondition _ _ _ _ = pure True--prop_counter :: Actions Counter -> Property-prop_counter as = monadicIO $ do- ref <- lift $ newIORef (0 :: Int)- runPropertyReaderT (runActions as) ref- assert True--tests :: TestTree-tests =- testGroup- "counter tests"- [ testProperty "prop_conter" $ prop_counter- ]
+ test/Spec/DynamicLogic/Counters.hs view
@@ -0,0 +1,97 @@+{-# LANGUAGE NamedFieldPuns #-}++-- | Define several variant models of /counters/ which are useful to+-- test or use examples for various behaviours of the runtime.+module Spec.DynamicLogic.Counters where++import Control.Monad.Reader+import Data.IORef+import Test.QuickCheck+import Test.QuickCheck.StateModel++-- A very simple model with a single action that always succeed in+-- predictable way. This model is useful for testing the runtime.+newtype SimpleCounter = SimpleCounter {count :: Int}+ deriving (Eq, Show, Generic)++deriving instance Eq (Action SimpleCounter a)+deriving instance Show (Action SimpleCounter a)+instance HasVariables (Action SimpleCounter a) where+ getAllVariables _ = mempty++instance StateModel SimpleCounter where+ data Action SimpleCounter a where+ IncSimple :: Action SimpleCounter Int++ arbitraryAction _ _ = pure $ Some IncSimple++ initialState = SimpleCounter 0++ nextState SimpleCounter{count} IncSimple _ = SimpleCounter (count + 1)++instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where+ perform _ IncSimple _ = do+ ref <- ask+ lift $ atomicModifyIORef' ref (\count -> (succ count, count))++-- A very simple model with a single action whose postcondition fails in a+-- predictable way. This model is useful for testing the runtime.+newtype FailingCounter = FailingCounter {failingCount :: Int}+ deriving (Eq, Show, Generic)++deriving instance Eq (Action FailingCounter a)+deriving instance Show (Action FailingCounter a)+instance HasVariables (Action FailingCounter a) where+ getAllVariables _ = mempty++instance StateModel FailingCounter where+ data Action FailingCounter a where+ Inc' :: Action FailingCounter Int++ arbitraryAction _ _ = pure $ Some Inc'++ initialState = FailingCounter 0++ nextState FailingCounter{failingCount} Inc' _ = FailingCounter (failingCount + 1)++instance RunModel FailingCounter (ReaderT (IORef Int) IO) where+ perform _ Inc' _ = do+ ref <- ask+ lift $ atomicModifyIORef' ref (\count -> (succ count, count))++ postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4++-- A generic but simple counter model+data Counter = Counter Int+ deriving (Show, Generic)++deriving instance Show (Action Counter a)+deriving instance Eq (Action Counter a)+instance HasVariables (Action Counter a) where+ getAllVariables _ = mempty++instance StateModel Counter where+ data Action Counter a where+ Inc :: Action Counter ()+ Reset :: Action Counter Int++ initialState = Counter 0++ arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)]++ nextState (Counter n) Inc _ = Counter (n + 1)+ nextState _ Reset _ = Counter 0++instance RunModel Counter (ReaderT (IORef Int) IO) where+ perform _ Inc _ = do+ ref <- ask+ lift $ modifyIORef ref succ+ perform _ Reset _ = do+ ref <- ask+ lift $ do+ n <- readIORef ref+ writeIORef ref 0+ pure n++ postcondition (Counter n, _) Reset _ res = pure $ n == res+ postcondition _ _ _ _ = pure True
+ test/Test/QuickCheck/StateModelSpec.hs view
@@ -0,0 +1,81 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PatternSynonyms #-}++module Test.QuickCheck.StateModelSpec where++import Control.Monad.Reader (lift)+import Data.IORef (newIORef)+import Data.List (isInfixOf)+import Spec.DynamicLogic.Counters (Counter (..), FailingCounter, SimpleCounter (..))+import Test.QuickCheck (Property, Result (..), Testable, chatty, choose, counterexample, noShrinking, property, stdArgs)+import Test.QuickCheck.Extras (runPropertyReaderT)+import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)+import Test.QuickCheck.StateModel (+ Actions,+ lookUpVarMaybe,+ mkVar,+ runActions,+ underlyingState,+ viewAtType,+ pattern Actions,+ )+import Test.QuickCheck.Test (test, withState)+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.HUnit (testCase, (@?))+import Test.Tasty.QuickCheck (testProperty)++tests :: TestTree+tests =+ testGroup+ "Running actions"+ [ testProperty "simple counter" $ prop_counter+ , testProperty "returns final state updated from actions" prop_returnsFinalState+ , testProperty "environment variables indices are 1-based " prop_variablesIndicesAre1Based+ , testCase "prints distribution of actions and polarity" $ do+ Success{output} <- captureTerminal prop_returnsFinalState+ "100.00% +Inc" `isInfixOf` output @? "Output does not contain '100.00% +Inc'"+ "Action polarity" `isInfixOf` output @? "Output does not contain 'Action polarity'"+ , testCase "prints counterexample as sequence of steps when postcondition fails" $ do+ Failure{output} <- captureTerminal prop_failsOnPostcondition+ "do action $ Inc'" `isInfixOf` output @? "Output does not contain \"do action $ Inc'\": " <> output+ ]++captureTerminal :: Testable p => p -> IO Result+captureTerminal p =+ withState stdArgs{chatty = False} $ \st ->+ test st (property p)++prop_counter :: Actions Counter -> Property+prop_counter as = monadicIO $ do+ ref <- lift $ newIORef (0 :: Int)+ runPropertyReaderT (runActions as) ref+ assert True++prop_returnsFinalState :: Actions SimpleCounter -> Property+prop_returnsFinalState actions@(Actions as) =+ monadicIO $ do+ ref <- lift $ newIORef (0 :: Int)+ (s, _) <- runPropertyReaderT (runActions actions) ref+ assert $ count (underlyingState s) == length as++prop_variablesIndicesAre1Based :: Actions SimpleCounter -> Property+prop_variablesIndicesAre1Based actions@(Actions as) =+ noShrinking $ monadicIO $ do+ ref <- lift $ newIORef (0 :: Int)+ (_, env) <- runPropertyReaderT (runActions actions) ref+ act <- pick $ choose (0, length as - 1)+ monitor $+ counterexample $+ unlines+ [ "Env: " <> show (viewAtType @Int <$> env)+ , "Actions: " <> show as+ , "Act: " <> show act+ ]+ assert $ null as || lookUpVarMaybe env (mkVar $ act + 1) == Just act++prop_failsOnPostcondition :: Actions FailingCounter -> Property+prop_failsOnPostcondition actions =+ monadicIO $ do+ ref <- lift $ newIORef (0 :: Int)+ runPropertyReaderT (runActions actions) ref+ assert True