diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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). diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal --- a/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic.cabal @@ -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 diff --git a/src/Test/QuickCheck/DynamicLogic/Internal.hs b/src/Test/QuickCheck/DynamicLogic/Internal.hs --- a/src/Test/QuickCheck/DynamicLogic/Internal.hs +++ b/src/Test/QuickCheck/DynamicLogic/Internal.hs @@ -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 diff --git a/src/Test/QuickCheck/StateModel.hs b/src/Test/QuickCheck/StateModel.hs --- a/src/Test/QuickCheck/StateModel.hs +++ b/src/Test/QuickCheck/StateModel.hs @@ -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 diff --git a/src/Test/QuickCheck/StateModel/Variables.hs b/src/Test/QuickCheck/StateModel/Variables.hs --- a/src/Test/QuickCheck/StateModel/Variables.hs +++ b/src/Test/QuickCheck/StateModel/Variables.hs @@ -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 diff --git a/test/Spec/DynamicLogic/Counters.hs b/test/Spec/DynamicLogic/Counters.hs --- a/test/Spec/DynamicLogic/Counters.hs +++ b/test/Spec/DynamicLogic/Counters.hs @@ -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 diff --git a/test/Spec/DynamicLogic/RegistryModel.hs b/test/Spec/DynamicLogic/RegistryModel.hs --- a/test/Spec/DynamicLogic/RegistryModel.hs +++ b/test/Spec/DynamicLogic/RegistryModel.hs @@ -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 ] diff --git a/test/Test/QuickCheck/StateModelSpec.hs b/test/Test/QuickCheck/StateModelSpec.hs --- a/test/Test/QuickCheck/StateModelSpec.hs +++ b/test/Test/QuickCheck/StateModelSpec.hs @@ -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