quickcheck-dynamic 3.4.2 → 4.0.0
raw patch · 9 files changed
+260/−177 lines, 9 files
Files
- CHANGELOG.md +13/−4
- README.md +1/−1
- quickcheck-dynamic.cabal +2/−2
- src/Test/QuickCheck/DynamicLogic/Internal.hs +27/−19
- src/Test/QuickCheck/StateModel.hs +163/−111
- src/Test/QuickCheck/StateModel/Variables.hs +5/−1
- test/Spec/DynamicLogic/Counters.hs +1/−1
- test/Spec/DynamicLogic/RegistryModel.hs +38/−37
- test/Test/QuickCheck/StateModelSpec.hs +10/−1
CHANGELOG.md view
@@ -7,11 +7,20 @@ As a minor extension, we also keep a semantic version for the `UNRELEASED` changes. -## UNRELEASED--## 3.4.2 - 2025-07-14+## 4.0.0 - 2025-03-12 -* Added support for `Quickcheck-2.16`.+* **BREAKING**: Removed `Realized`+ - To migrate uses of `Realized` with `IOSim`, index the state type on the choice of `RunModel` monad+ and index the relevant types:+ ```+ -- Turn:+ data ModelState = State { threadId :: Var ThreadId }+ -- Into:+ data ModelState m = State { threadId :: Var (ThreadId m) }+ ```+* **BREAKING**: Moved `Error state` from `StateModel` to `RunModel` and indexed it on both the `state` and the monad `m`+* **BREAKING**: Changed `PerformResult` from `PerformResult (Error state) a` to `PerformResult state m a`+* Added a `moreActions` property modifier to allow controlling the length of action sequences. ## 3.4.1 - 2024-03-22
README.md view
@@ -17,7 +17,7 @@ comments. Checkout [StateModel](https://hackage.haskell.org/package/quickcheck-dynamic/docs/src/Test.QuickCheck.StateModel.html) and [DynamicLogic](https://hackage.haskell.org/package/quickcheck-dynamic/docs/Test-QuickCheck-DynamicLogic.html) modules for some usage instructions.-* For a concrete standalone example, have a look at `Registry` and `RegistryModel` modules from the companion [quickcheck-io-sim-compat](https://github.com/input-output-hk/quickcheck-dynamic/tree/main/quickcheck-io-sim-compat) package (not currently available on hackage), a multithreaded Thread registry inspired by the Erlang version of QuickCheck described in [this article](https://mengwangoxf.github.io/Papers/Erlang18.pdf)+* For a concrete standalone example, have a look at the [`Registry`](https://github.com/input-output-hk/quickcheck-dynamic/blob/main/quickcheck-dynamic/test/Spec/DynamicLogic/Registry.hs) and [`RegistryModel`](https://github.com/input-output-hk/quickcheck-dynamic/blob/main/quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs) module from the test suite, which respectively implement and model a multithreaded Thread registry inspired by the Erlang version of QuickCheck described in [this article](https://mengwangoxf.github.io/Papers/Erlang18.pdf) * For more documentation on how to quickcheck-dynamic is used to test Plutus DApps, check this [tutorial](https://plutus-apps.readthedocs.io/en/latest/plutus/tutorials/contract-models.html).
quickcheck-dynamic.cabal view
@@ -1,12 +1,12 @@ cabal-version: 2.2 name: quickcheck-dynamic-version: 3.4.2+version: 4.0.0 license: Apache-2.0 license-files: LICENSE NOTICE -maintainer: arnaud.bailly@iohk.io+maintainer: sebastian.nagel@iohk.io author: Ulf Norell category: Testing synopsis: A library for stateful property-based testing
src/Test/QuickCheck/DynamicLogic/Internal.hs view
@@ -4,8 +4,7 @@ import Control.Arrow (second) import Control.Monad import Data.Typeable-import Test.QuickCheck (Gen, Property, Testable)-import Test.QuickCheck qualified as QC+import Test.QuickCheck hiding (generate) import Test.QuickCheck.DynamicLogic.CanGenerate import Test.QuickCheck.DynamicLogic.Quantify import Test.QuickCheck.DynamicLogic.SmartShrinking@@ -340,8 +339,7 @@ -- | Simplest "execution" function for `DynFormula`. -- Turns a given a `DynFormula` paired with an interpreter function to produce some result from an----- `Actions` sequence into a proper `Property` than can then be run by QuickCheck.+-- `Actions` sequence into a proper `Property` that can be run by QuickCheck. forAllScripts :: (DynLogicModel s, Testable a) => DynFormula s@@ -361,8 +359,8 @@ let d = unDynFormula f sz n = unsafeNextVarIndex $ vars s in case generate chooseUniqueNextStep d n s 500 of- Nothing -> QC.counterexample "Generating Non-unique script in forAllUniqueScripts" False- Just test -> validDLTest d test . applyMonitoring d test . QC.property $ k (scriptFromDL test)+ Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False+ Just test -> validDLTest test . applyMonitoring d test . property $ k (scriptFromDL test) -- | Creates a `Property` from `DynFormula` with some specialised isomorphism for shrinking purpose. forAllMappedScripts@@ -375,23 +373,38 @@ forAllMappedScripts to from f k = QC.withSize $ \n -> let d = unDynFormula f n- in QC.forAllShrinkBlind- (QC.Smart 0 <$> QC.sized ((from <$>) . generateDLTest d))+ in forAllShrinkBlind+ (Smart 0 <$> sized ((from <$>) . generateDLTest d)) (shrinkSmart ((from <$>) . shrinkDLTest d . to))- $ \(QC.Smart _ script) ->+ $ \(Smart _ script) -> withDLScript d k (to script) withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property withDLScript d k test =- validDLTest d test . applyMonitoring d test . QC.property $ k (scriptFromDL test)+ validDLTest test . applyMonitoring d test . property $ k (scriptFromDL test) withDLScriptPrefix :: (DynLogicModel s, Testable a) => DynFormula s -> (Actions s -> a) -> DynLogicTest s -> Property withDLScriptPrefix f k test = QC.withSize $ \n -> let d = unDynFormula f n test' = unfailDLTest d test- in validDLTest d test' . applyMonitoring d test' . QC.property $ k (scriptFromDL test')+ in validDLTest test' . applyMonitoring d test' . property $ k (scriptFromDL test') +-- | Validate generated test case.+--+-- Test case generation does not always produce a valid test case. In+-- some cases, we did not find a suitable test case matching some+-- `DynFormula` and we are `Stuck`, hence we want to discard the test+-- case and start over ; in other cases we found a genuine issue with+-- the formula leading to the impossibility of producing a valid test+-- case.+validDLTest :: StateModel s => DynLogicTest s -> Property -> Property+validDLTest test prop =+ case test of+ DLScript{} -> counterexample (show test) prop+ Stuck{} -> property Discard+ _other -> counterexample (show test) False+ generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s) generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size @@ -503,7 +516,7 @@ nextSteps' gen (Monitor _f d) = nextSteps' gen d chooseOneOf :: [(Double, a)] -> Gen a-chooseOneOf steps = QC.frequency [(round (w / never), return s) | (w, s) <- steps]+chooseOneOf steps = frequency [(round (w / never), return s) | (w, s) <- steps] never :: Double never = 1.0e-9@@ -573,7 +586,7 @@ keepTryingUntil 0 _ _ = return Nothing keepTryingUntil n g p = do x <- g- if p x then return $ Just x else QC.scale (+ 1) $ keepTryingUntil (n - 1) g p+ if p x then return $ Just x else scale (+ 1) $ keepTryingUntil (n - 1) g p shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s] shrinkDLTest _ (Looping _) = []@@ -697,7 +710,7 @@ propPruningGeneratedScriptIsNoop :: DynLogicModel s => DynLogic s -> Property propPruningGeneratedScriptIsNoop d =- QC.forAll (QC.sized $ \n -> QC.choose (1, max 1 n) >>= generateDLTest d) $ \test ->+ forAll (sized $ \n -> choose (1, max 1 n) >>= generateDLTest d) $ \test -> let script = case test of BadPrecondition s _ _ -> s Looping s -> s@@ -763,11 +776,6 @@ stuck (Weight w d) s = w < never || stuck d s stuck (ForAll _ _) _ = False stuck (Monitor _ d) s = stuck d s--validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property -> Property-validDLTest _ Stuck{} _ = False QC.==> False-validDLTest _ test@DLScript{} p = QC.counterexample (show test) p-validDLTest _ test _ = QC.counterexample (show test) False scriptFromDL :: DynLogicTest s -> Actions s scriptFromDL (DLScript s) = Actions $ sequenceSteps s
src/Test/QuickCheck/StateModel.hs view
@@ -1,5 +1,7 @@ {-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} -- | Model-Based Testing library for use with Haskell QuickCheck.@@ -23,9 +25,9 @@ EnvEntry (..), pattern (:=?), Env,- Realized, Generic, IsPerformResult,+ Options (..), monitorPost, counterexamplePost, stateAfter,@@ -38,12 +40,14 @@ computePrecondition, computeArbitraryAction, computeShrinkAction,+ generateActionsWithOptions,+ shrinkActionsWithOptions,+ defaultOptions,+ moreActions, ) where import Control.Monad-import Control.Monad.Identity import Control.Monad.Reader-import Control.Monad.State import Control.Monad.Writer (WriterT, runWriterT, tell) import Data.Data import Data.Kind@@ -52,8 +56,7 @@ import Data.Set qualified as Set import Data.Void import GHC.Generics-import Test.QuickCheck (Arbitrary, Gen, Property, Smart (..), counterexample, frequency, resize, shrinkList, sized, tabulate)-import Test.QuickCheck qualified as QC+import Test.QuickCheck as QC import Test.QuickCheck.DynamicLogic.SmartShrinking import Test.QuickCheck.Monadic import Test.QuickCheck.StateModel.Variables@@ -107,13 +110,6 @@ -- anything. data Action state a - -- | The type of errors that actions can throw. If this is defined as anything- -- other than `Void` `perform` is required to return `Either (Error state) a`- -- instead of `a`.- type Error state-- type Error state = Void- -- | Display name for `Action`. -- This is useful to provide sensible statistics about the distribution of `Action`s run -- when checking a property.@@ -163,31 +159,6 @@ deriving instance (forall a. Show (Action state a)) => Show (Any (Action state)) --- | The result required of `perform` depending on the `Error` type--- of a state model. If there are no errors, `Error state = Void`, and--- so we don't need to specify if the action failed or not.-type family PerformResult e a where- PerformResult Void a = a- PerformResult e a = Either e a--class IsPerformResult e a where- performResultToEither :: PerformResult e a -> Either e a--instance {-# OVERLAPPING #-} IsPerformResult Void a where- performResultToEither = Right--instance {-# OVERLAPPABLE #-} (PerformResult e a ~ Either e a) => IsPerformResult e a where- performResultToEither = id---- TODO: maybe it makes sense to write--- out a long list of these instances-type family Realized (m :: Type -> Type) a :: Type-type instance Realized IO a = a-type instance Realized (StateT s m) a = Realized m a-type instance Realized (ReaderT r m) a = Realized m a-type instance Realized (WriterT w m) a = Realized m a-type instance Realized Identity a = a- newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, Endo Property) m a} deriving (Functor, Applicative, Monad) @@ -211,7 +182,33 @@ counterexamplePost :: Monad m => String -> PostconditionM m () counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c) +-- | The result required of `perform` depending on the `Error` type.+-- If there are no errors, `Error state = Void`, and+-- so we don't need to specify if the action failed or not.+type family PerformResult state (m :: Type -> Type) a where+ PerformResult state m a = EitherIsh (Error state m) a++type family EitherIsh e a where+ EitherIsh Void a = a+ EitherIsh e a = Either e a++class IsPerformResult e a where+ performResultToEither :: EitherIsh e a -> Either e a++instance {-# OVERLAPPING #-} IsPerformResult Void a where+ performResultToEither = Right++instance {-# OVERLAPPABLE #-} (EitherIsh e a ~ Either e a) => IsPerformResult e a where+ performResultToEither = id+ class (forall a. Show (Action state a), Monad m) => RunModel state m where+ -- | The type of errors that actions can throw. If this is defined as anything+ -- other than `Void` `perform` is required to return `Either (Error state) a`+ -- instead of `a`.+ type Error state m++ type Error state m = Void+ -- | Perform an `Action` in some `state` in the `Monad` `m`. This -- is the function that's used to exercise the actual stateful -- implementation, usually through various side-effects as permitted@@ -222,57 +219,57 @@ -- -- The `Lookup` parameter provides an /environment/ to lookup `Var -- a` instances from previous steps.- perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a))+ perform :: Typeable a => state -> Action state a -> LookUp -> m (PerformResult state m a) -- | Postcondition on the `a` value produced at some step. -- The result is `assert`ed and will make the property fail should it be `False`. This is useful -- to check the implementation produces expected values.- postcondition :: (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool+ postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM m Bool postcondition _ _ _ _ = pure True -- | Postcondition on the result of running a _negative_ `Action`. -- The result is `assert`ed and will make the property fail should it be `False`. This is useful -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't -- been updated during the execution of the negative action.- postconditionOnFailure :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> PostconditionM m Bool+ postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM m Bool postconditionOnFailure _ _ _ _ = pure True -- | Allows the user to attach additional information to the `Property` at each step of the process. -- This function is given the full transition that's been executed, including the start and ending -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform` -- while executing this step.- monitoring :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> Property -> Property+ monitoring :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> Property -> Property monitoring _ _ _ _ prop = prop -- | Allows the user to attach additional information to the `Property` if a positive action fails.- monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property+ monitoringFailure :: state -> Action state a -> LookUp -> Error state m -> Property -> Property monitoringFailure _ _ _ _ prop = prop -type LookUp m = forall a. Typeable a => Var a -> Realized m a+type LookUp = forall a. Typeable a => Var a -> a -type Env m = [EnvEntry m]+type Env = [EnvEntry] -data EnvEntry m where- (:==) :: Typeable a => Var a -> Realized m a -> EnvEntry m+data EnvEntry where+ (:==) :: Typeable a => Var a -> a -> EnvEntry infix 5 :== -pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m+pattern (:=?) :: forall a. Typeable a => Var a -> a -> EnvEntry pattern v :=? val <- (viewAtType -> Just (v, val)) -viewAtType :: forall a m. Typeable a => EnvEntry m -> Maybe (Var a, Realized m a)+viewAtType :: forall a. Typeable a => EnvEntry -> Maybe (Var a, a) viewAtType ((v :: Var b) :== val) | Just Refl <- eqT @a @b = Just (v, val) | otherwise = Nothing -lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a)+lookUpVarMaybe :: forall a. Typeable a => Env -> Var a -> Maybe a lookUpVarMaybe [] _ = Nothing lookUpVarMaybe (((v' :: Var b) :== a) : env) v = case eqT @a @b of Just Refl | v == v' -> Just a _ -> lookUpVarMaybe env v -lookUpVar :: Typeable a => Env m -> Var a -> Realized m a+lookUpVar :: Typeable a => Env -> Var a -> a lookUpVar env v = case lookUpVarMaybe env v of Nothing -> error $ "Variable " ++ show v ++ " is not bound at type " ++ show (typeRep v) ++ "!" Just a -> a@@ -368,57 +365,101 @@ <> go (computeNextState aState act var) steps instance forall state. StateModel state => Arbitrary (Actions state) where- arbitrary = do- (as, rejected) <- arbActions initialAnnotatedState 1- return $ Actions_ rejected (Smart 0 as)- where- arbActions :: Annotated state -> Int -> Gen ([Step state], [String])- arbActions s step = sized $ \n ->- let w = n `div` 2 + 1- in frequency- [ (1, return ([], []))- ,- ( w- , do- (mact, rej) <- satisfyPrecondition- case mact of- Just (Some act@ActionWithPolarity{}) -> do- let var = mkVar step- (as, rejected) <- arbActions (computeNextState s act var) (step + 1)- return ((var := act) : as, rej ++ rejected)- Nothing ->- return ([], [])- )- ]- where- satisfyPrecondition = sized $ \n -> go n (2 * n) [] -- idea copied from suchThatMaybe- go m n rej- | m > n = return (Nothing, rej)- | otherwise = do- a <- resize m $ computeArbitraryAction s- case a of- Some act ->- if computePrecondition s act- then return (Just (Some act), rej)- else go (m + 1) n (actionName (polarAction act) : rej)+ arbitrary = generateActionsWithOptions defaultOptions+ shrink = shrinkActionsWithOptions defaultOptions - shrink (Actions_ rs as) =- map (Actions_ rs) (shrinkSmart (map (prune . map fst) . concatMap customActionsShrinker . shrinkList shrinker . withStates) as)- where- shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]- shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act'@ActionWithPolarity{} <- computeShrinkAction s act]+data QCDProperty state = QCDProperty+ { runQCDProperty :: Actions state -> Property+ , qcdPropertyOptions :: Options state+ } - customActionsShrinker :: [(Step state, Annotated state)] -> [[(Step state, Annotated state)]]- customActionsShrinker acts =- let usedVars = mconcat [getAllVariables a <> getAllVariables (underlyingState s) | (_ := a, s) <- acts]- binding (v := _, _) = Some v `Set.member` usedVars- -- Remove at most one non-binding action- go [] = [[]]- go (p : ps)- | binding p = map (p :) (go ps)- | otherwise = ps : map (p :) (go ps)- in go acts+instance StateModel state => Testable (QCDProperty state) where+ property QCDProperty{..} =+ forAllShrink+ (generateActionsWithOptions qcdPropertyOptions)+ (shrinkActionsWithOptions qcdPropertyOptions)+ runQCDProperty +class QCDProp state p | p -> state where+ qcdProperty :: p -> QCDProperty state++instance QCDProp state (QCDProperty state) where+ qcdProperty = id++instance Testable p => QCDProp state (Actions state -> p) where+ qcdProperty p = QCDProperty (property . p) defaultOptions++modifyOptions :: QCDProperty state -> (Options state -> Options state) -> QCDProperty state+modifyOptions p f =+ let opts = qcdPropertyOptions p+ in p{qcdPropertyOptions = f opts}++moreActions :: QCDProp state p => Rational -> p -> QCDProperty state+moreActions r p =+ modifyOptions (qcdProperty p) $ \opts -> opts{actionLengthMultiplier = actionLengthMultiplier opts * r}++-- NOTE: indexed on state for forwards compatibility, e.g. when we+-- want to give an explicit initial state+data Options state = Options {actionLengthMultiplier :: Rational}++defaultOptions :: Options state+defaultOptions = Options{actionLengthMultiplier = 1}++-- | Generate arbitrary actions with the `GenActionsOptions`. More flexible than using the type-based+-- modifiers.+generateActionsWithOptions :: forall state. StateModel state => Options state -> Gen (Actions state)+generateActionsWithOptions Options{..} = do+ (as, rejected) <- arbActions [] [] initialAnnotatedState 1+ return $ Actions_ rejected (Smart 0 as)+ where+ arbActions :: [Step state] -> [String] -> Annotated state -> Int -> Gen ([Step state], [String])+ arbActions steps rejected s step = sized $ \n -> do+ let w = round (actionLengthMultiplier * fromIntegral n) `div` 2 + 1+ continue <- frequency [(1, pure False), (w, pure True)]+ if continue+ then do+ (mact, rej) <- satisfyPrecondition+ case mact of+ Just (Some act@ActionWithPolarity{}) -> do+ let var = mkVar step+ arbActions+ ((var := act) : steps)+ (rej ++ rejected)+ (computeNextState s act var)+ (step + 1)+ Nothing ->+ return (reverse steps, rejected)+ else return (reverse steps, rejected)+ where+ satisfyPrecondition = sized $ \n -> go n (2 * n) [] -- idea copied from suchThatMaybe+ go m n rej+ | m > n = return (Nothing, rej)+ | otherwise = do+ a <- resize m $ computeArbitraryAction s+ case a of+ Some act ->+ if computePrecondition s act+ then return (Just (Some act), rej)+ else go (m + 1) n (actionName (polarAction act) : rej)++shrinkActionsWithOptions :: forall state. StateModel state => Options state -> Actions state -> [Actions state]+shrinkActionsWithOptions _ (Actions_ rs as) =+ map (Actions_ rs) (shrinkSmart (map (prune . map fst) . concatMap customActionsShrinker . shrinkList shrinker . withStates) as)+ where+ shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]+ shrinker (v := act, s) = [(unsafeCoerceVar v := act', s) | Some act'@ActionWithPolarity{} <- computeShrinkAction s act]++ customActionsShrinker :: [(Step state, Annotated state)] -> [[(Step state, Annotated state)]]+ customActionsShrinker acts =+ let usedVars = mconcat [getAllVariables a <> getAllVariables (underlyingState s) | (_ := a, s) <- acts]+ binding (v := _, _) = Some v `Set.member` usedVars+ -- Remove at most one non-binding action+ go [] = [[]]+ go (p : ps)+ | binding p = map (p :) (go ps)+ | otherwise = ps : map (p :) (go ps)+ in go acts+ -- Running state models data Annotated state = Metadata@@ -502,47 +543,58 @@ :: forall state m e . ( StateModel state , RunModel state m- , e ~ Error state+ , e ~ Error state m , forall a. IsPerformResult e a ) => Actions state- -> PropertyM m (Annotated state, Env m)+ -> PropertyM m (Annotated state, Env) runActions (Actions_ rejected (Smart _ actions)) = do- (finalState, env) <- runSteps initialAnnotatedState [] actions+ let bucket = \n -> let (a, b) = go n in show a ++ " - " ++ show b+ where+ go n+ | n < 100 = (d * 10, d * 10 + 9)+ | otherwise = let (a, b) = go d in (a * 10, b * 10 + 9)+ where+ d = div n 10+ monitor $ tabulate "# of actions" [show $ bucket $ length actions]+ (finalState, env, names, polars) <- runSteps initialAnnotatedState [] actions+ monitor $ tabulate "Actions" names+ monitor $ tabulate "Action polarity" $ map show polars 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.+-- | Core function to execute a sequence of `Step` given some initial `Env`ironment and `Annotated`+-- state. Return the list of action names and polarities to work around+-- https://github.com/nick8325/quickcheck/issues/416 causing repeated calls to tabulate being slow. runSteps :: forall state m e . ( StateModel state , RunModel state m- , e ~ Error state+ , e ~ Error state m , forall a. IsPerformResult e a ) => Annotated state- -> Env m+ -> Env -> [Step state]- -> PropertyM m (Annotated state, Env m)-runSteps s env [] = return (s, reverse env)+ -> PropertyM m (Annotated state, Env, [String], [Polarity])+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+ (s'', env'', names, polars) <- runSteps s' env' as+ pure (s'', env'', name : names, polar : polars) (NegPolarity, _) -> do (s', env') <- negativeActionResult ret- runSteps s' env' as+ (s'', env'', names, polars) <- runSteps s' env' as+ pure (s'', env'', name : names, polar : polars) where polar = polarity act
src/Test/QuickCheck/StateModel/Variables.hs view
@@ -31,12 +31,16 @@ import GHC.Generics import GHC.TypeLits import GHC.Word-import Test.QuickCheck (Gen, Smart (..), elements)+import Test.QuickCheck as QC -- | A symbolic variable for a value of type `a` newtype Var a = Var Int deriving (Eq, Ord, Typeable, Data) +-- | Create a fresh symbolic variable with given identifier. While 'Var's are+-- usually created by action generators, this function can be used for example+-- to create a 'Var' in the 'initialState' of a 'StateModel'. A good default+-- value for the identifier is '-1' as this will not be generated otherwise. mkVar :: Int -> Var a mkVar = Var
test/Spec/DynamicLogic/Counters.hs view
@@ -6,7 +6,7 @@ import Control.Monad.Reader import Data.IORef-import Test.QuickCheck (frequency)+import Test.QuickCheck import Test.QuickCheck.StateModel -- A very simple model with a single action that always succeed in
test/Spec/DynamicLogic/RegistryModel.hs view
@@ -10,8 +10,7 @@ import Data.List import Data.Map (Map) import Data.Map qualified as Map-import Test.QuickCheck (Gen, Property)-import Test.QuickCheck qualified as QC+import Test.QuickCheck import Test.QuickCheck.Monadic hiding (assert) import Test.QuickCheck.Monadic qualified as QC import Test.Tasty hiding (after)@@ -45,8 +44,6 @@ Unregister :: String -> Action RegState () KillThread :: Var ThreadId -> Action RegState () - type Error RegState = SomeException- precondition s (Register name tid) = name `Map.notMember` regs s && tid `notElem` Map.elems (regs s)@@ -58,30 +55,31 @@ validFailingAction _ _ = True arbitraryAction ctx s =- QC.frequency $- [- ( max 1 $ 10 - length (ctxAtType @ThreadId ctx)- , return $ Some Spawn- )- ,- ( 2 * Map.size (regs s)- , Some <$> (Unregister <$> probablyRegistered s)- )- ,- ( 10- , Some <$> (WhereIs <$> probablyRegistered s)- )- ]- ++ [ ( max 1 $ 3 - length (dead s)- , Some <$> (KillThread <$> arbitraryVar ctx)- )- | not . null $ ctxAtType @ThreadId ctx- ]- ++ [ ( max 1 $ 10 - Map.size (regs s)- , Some <$> (Register <$> probablyUnregistered s <*> arbitraryVar ctx)- )- | not . null $ ctxAtType @ThreadId ctx- ]+ let threadIdCtx = ctxAtType @ThreadId ctx+ in frequency $+ [+ ( max 1 $ 10 - length threadIdCtx+ , return $ Some Spawn+ )+ ,+ ( 2 * Map.size (regs s)+ , Some <$> (Unregister <$> probablyRegistered s)+ )+ ,+ ( 10+ , Some <$> (WhereIs <$> probablyRegistered s)+ )+ ]+ ++ [ ( max 1 $ 3 - length (dead s)+ , Some <$> (KillThread <$> arbitraryVar ctx)+ )+ | not . null $ threadIdCtx+ ]+ ++ [ ( max 1 $ 10 - Map.size (regs s)+ , Some <$> (Register <$> probablyUnregistered s <*> arbitraryVar ctx)+ )+ | not . null $ threadIdCtx+ ] shrinkAction ctx _ (Register name tid) = [Some (Unregister name)]@@ -111,6 +109,8 @@ type RegM = ReaderT Registry IO instance RunModel RegState RegM where+ type Error RegState RegM = SomeException+ perform _ Spawn _ = do tid <- lift $ forkIO (threadDelay 10000000) pure $ Right tid@@ -135,18 +135,18 @@ postconditionOnFailure (s, _) act@Register{} _ res = do monitorPost $- QC.tabulate+ tabulate "Reason for -Register" [why s act] pure $ isLeft res postconditionOnFailure _s _ _ _ = pure True monitoring (_s, s') act@(showDictAction -> ShowDict) _ res =- QC.counterexample (show res ++ " <- " ++ show act ++ "\n -- State: " ++ show s')- . QC.tabulate "Registry size" [show $ Map.size (regs s')]+ counterexample (show res ++ " <- " ++ show act ++ "\n -- State: " ++ show s')+ . tabulate "Registry size" [show $ Map.size (regs s')] data ShowDict a where- ShowDict :: Show (Realized RegM a) => ShowDict a+ ShowDict :: Show a => ShowDict a showDictAction :: forall a. Action RegState a -> ShowDict a showDictAction Spawn{} = ShowDict@@ -167,13 +167,13 @@ why _ _ = "(impossible)" arbitraryName :: Gen String-arbitraryName = QC.elements allNames+arbitraryName = elements allNames probablyRegistered :: RegState -> Gen String-probablyRegistered s = QC.oneof $ map pure (Map.keys $ regs s) ++ [arbitraryName]+probablyRegistered s = oneof $ map pure (Map.keys $ regs s) ++ [arbitraryName] probablyUnregistered :: RegState -> Gen String-probablyUnregistered s = QC.elements $ allNames ++ (allNames \\ Map.keys (regs s))+probablyUnregistered s = elements $ allNames ++ (allNames \\ Map.keys (regs s)) shrinkName :: String -> [String] shrinkName name = [n | n <- allNames, n < name]@@ -184,7 +184,7 @@ prop_Registry :: Actions RegState -> Property prop_Registry s = monadicIO $ do- monitor $ QC.counterexample "\nExecution\n"+ monitor $ counterexample "\nExecution\n" reg <- lift setupRegistry runPropertyReaderT (runActions s) reg QC.assert True@@ -268,6 +268,7 @@ testGroup "registry model example" [ testProperty "prop_Registry" $ prop_Registry+ , testProperty "moreActions 10 $ prop_Registry" $ moreActions 10 prop_Registry , testProperty "canRegister" $ propDL canRegister- , testProperty "canRegisterNoUnregister" $ QC.expectFailure $ propDL canRegisterNoUnregister+ , testProperty "canRegisterNoUnregister" $ expectFailure $ propDL canRegisterNoUnregister ]
test/Test/QuickCheck/StateModelSpec.hs view
@@ -7,13 +7,14 @@ 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 (Property, Result (..), Testable, chatty, checkCoverage, choose, counterexample, cover, noShrinking, property, stdArgs) import Test.QuickCheck.Extras (runPropertyReaderT) import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick) import Test.QuickCheck.StateModel ( Actions, lookUpVarMaybe, mkVar,+ moreActions, runActions, underlyingState, viewAtType,@@ -29,6 +30,7 @@ testGroup "Running actions" [ testProperty "simple counter" $ prop_counter+ , testProperty "simple_counter_moreActions" $ moreActions 30 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@@ -38,6 +40,9 @@ , 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+ , testProperty+ "moreActions introduces long sequences of actions"+ prop_longSequences ] captureTerminal :: Testable p => p -> IO Result@@ -79,3 +84,7 @@ ref <- lift $ newIORef (0 :: Int) runPropertyReaderT (runActions actions) ref assert True++prop_longSequences :: Property+prop_longSequences =+ checkCoverage $ moreActions 10 $ \(Actions steps :: Actions SimpleCounter) -> cover 50 (100 < length steps) "Long sequences" True