quickcheck-dynamic 1.1.0 → 2.0.0
raw patch · 6 files changed
+112/−111 lines, 6 filesdep +mtl
Dependencies added: mtl
Files
- CHANGELOG.md +7/−0
- quickcheck-dynamic.cabal +20/−12
- src/Test/QuickCheck/DynamicLogic.hs +1/−3
- src/Test/QuickCheck/DynamicLogic/Core.hs +9/−16
- src/Test/QuickCheck/DynamicLogic/Quantify.hs +0/−3
- src/Test/QuickCheck/StateModel.hs +75/−77
CHANGELOG.md view
@@ -9,6 +9,13 @@ ## UNRELEASED +## 2.0.0 - 2022-10-11++* **BREAKING**: Add `Realized` type family to distinguish between the model- and real type of an action+* **BREAKING**: Introduce `RunModel` type class to interpret Model-generated sequence of actions against real-world implementation+ * Move `perform` method from `StateModel` to this new type-class+ * Also split `postcondition` and `monitoring` out from the `StateModel` to the `RunModel` type class+* Added Thread registry example based on io-sim concurrency simulation library ## 1.1.0 - 2022-08-27
quickcheck-dynamic.cabal view
@@ -1,16 +1,16 @@ cabal-version: 2.2 name: quickcheck-dynamic-version: 1.1.0+version: 2.0.0 license: Apache-2.0 license-files: LICENSE NOTICE- + maintainer: arnaud.bailly@iohk.io author: Ulf Norell category: Testing synopsis:- A library for stateful property-based testing + A library for stateful property-based testing homepage: https://github.com/input-output-hk/quickcheck-dynamic#readme @@ -23,7 +23,7 @@ build-type: Simple extra-doc-files: README.md extra-source-files: CHANGELOG.md- + source-repository head type: git location: https://github.com/input-output-hk/quickcheck-dynamic@@ -31,16 +31,23 @@ common lang default-language: Haskell2010 default-extensions:- DeriveFoldable DeriveFunctor- DeriveGeneric- DeriveLift- DeriveTraversable- ExplicitForAll- GeneralizedNewtypeDeriving+ DeriveDataTypeable+ StandaloneDeriving ImportQualifiedPost+ TupleSections+ LambdaCase+ PatternSynonyms+ GADTs+ TypeApplications ScopedTypeVariables- StandaloneDeriving+ TypeFamilies+ FlexibleContexts+ FlexibleInstances+ MultiParamTypeClasses+ RankNTypes+ ViewPatterns+ TypeOperators ghc-options: -Wall -Wnoncanonical-monad-instances -Wunused-packages@@ -61,4 +68,5 @@ build-depends: QuickCheck -any, base >=4.7 && <5,- random -any+ random -any,+ mtl -any
src/Test/QuickCheck/DynamicLogic.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE FlexibleContexts #-}- -- | Monadic interface for writing /Dynamic Logic/ properties. -- -- This interface offers a much nicer experience than manipulating the@@ -64,7 +62,7 @@ instance MonadFail (DL s) where fail = errorDL -action :: (Show a, Typeable a, Eq (Action s a)) => Action s a -> DL s ()+action :: (Typeable a, Eq (Action s a)) => Action s a -> DL s () action cmd = DL $ \_ k -> DL.after cmd $ k () anyAction :: DL s ()
src/Test/QuickCheck/DynamicLogic/Core.hs view
@@ -1,10 +1,3 @@-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}- module Test.QuickCheck.DynamicLogic.Core ( module Test.QuickCheck.DynamicLogic.Quantify, DynLogic,@@ -95,7 +88,7 @@ -- | Given `f` must be `True` after /some/ action. -- `f` is passed the state resulting from executing the `Action`. after ::- (Show a, Typeable a, Eq (Action s a)) =>+ (Typeable a, Eq (Action s a)) => Action s a -> (s -> DynFormula s) -> DynFormula s@@ -474,8 +467,8 @@ where shrink' _ [] _ = [] shrink' d (step : as) s =- [] :- reverse (takeWhile (not . null) [drop (n - 1) as | n <- iterate (* 2) 1])+ []+ : reverse (takeWhile (not . null) [drop (n - 1) as | n <- iterate (* 2) 1]) ++ case step of Do (Var i := act) -> [Do (Var i := act') : as | Some act' <- shrinkAction s act]@@ -513,13 +506,13 @@ prune _ _ [] = [] prune ds s (Do (var := act) : rest) | precondition s act =- case [d' | d <- ds, d' <- stepDL d s (Do $ var := act)] of- [] -> prune ds s rest- ds' ->- Do (var := act) :- prune ds' (nextState s act var) rest+ case [d' | d <- ds, d' <- stepDL d s (Do $ var := act)] of+ [] -> prune ds s rest+ ds' ->+ Do (var := act)+ : prune ds' (nextState s act var) rest | otherwise =- prune ds s rest+ prune ds s rest prune ds s (Witness a : rest) = case [d' | d <- ds, d' <- stepDL d s (Witness a)] of [] -> prune ds s rest
src/Test/QuickCheck/DynamicLogic/Quantify.hs view
@@ -1,6 +1,3 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE TypeFamilies #-} {-# OPTIONS_GHC -fno-warn-name-shadowing #-} -- | This module defines Quantifications, which are used together with
src/Test/QuickCheck/StateModel.hs view
@@ -1,16 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE QuantifiedConstraints #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -- | Simple (stateful) Model-Based Testing library for use with Haskell QuickCheck.@@ -28,17 +17,21 @@ Actions (..), pattern Actions, EnvEntry (..),+ pattern (:=?), Env,+ Realized, stateAfter, runActions, runActionsInState, lookUpVar, lookUpVarMaybe,- invertLookupVarMaybe, ) where import Control.Monad+import Control.Monad.Reader+import Control.Monad.State import Data.Data+import Data.Kind import Test.QuickCheck as QC import Test.QuickCheck.DynamicLogic.SmartShrinking import Test.QuickCheck.Monadic@@ -61,8 +54,6 @@ -- the action is /rejected/ and a new one is tried. This is also useful when shrinking a trace -- in order to ensure that removing some `Action` still produces a valid trace. The `precondition` can be -- somewhat redundant with the generator's conditions,--- * `postcondition`: This function is evaluated during test execution after `perform`ing the action, it allows--- the model to express expectations about the output of actual code given some "transition". class ( forall a. Show (Action state a) , Show state@@ -103,7 +94,7 @@ -- | Shrinker for `Action`. -- Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness -- of property-based testing.- shrinkAction :: (Show a, Typeable a) => state -> Action state a -> [Any (Action state)]+ shrinkAction :: Typeable a => state -> Action state a -> [Any (Action state)] shrinkAction _ _ = [] -- | Initial state of generated traces.@@ -114,7 +105,7 @@ -- by `perform`ing the `Action` inside the `state` so that further actions can use `Lookup` -- to retrieve that data. This allows the model to be ignorant of those values yet maintain -- some references that can be compared and looked for.- nextState :: state -> Action state a -> Var a -> state+ nextState :: Typeable a => state -> Action state a -> Var a -> state nextState s _ _ = s -- | Precondition for filtering generated `Action`.@@ -123,63 +114,70 @@ precondition :: state -> Action state a -> Bool precondition _ _ = True +-- 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++class Monad m => RunModel state m where+ -- | 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+ -- by `m`. It produces a value of type `a`, eg. some observable+ -- output from the `Action` that should later be kept in the+ -- environment through a `Var a` also passed to the `nextState`+ -- function.+ --+ -- The `Lookup` parameter provides an /environment/ to lookup `Var+ -- a` instances from previous steps.+ perform :: forall a. Typeable a => state -> Action state a -> LookUp m -> m (Realized 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 -> Action state a -> LookUp -> a -> Bool- postcondition _ _ _ _ = True+ postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> m Bool+ postcondition _ _ _ _ = pure True -- | Allows the user to attach 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 :: Show a => (state, state) -> Action state a -> LookUp -> a -> Property -> Property- monitoring _ _ _ _ = id---- | 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--- by `m`. It produces a value of type `a`, eg. some observable--- output from the `Action` that should later be kept in the--- environment through a `Var a` also passed to the `nextState`--- function.------ The `Lookup` parameter provides an /environment/ to lookup `Var--- a` instances from previous steps.-newtype RunModel state m = RunModel {perform :: forall a. state -> Action state a -> LookUp -> m a}+ monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property+ monitoring _ _ _ _ prop = prop -type LookUp = forall a. Typeable a => Var a -> a+type LookUp m = forall a. Typeable a => Var a -> Realized m a -type Env = [EnvEntry]+type Env m = [EnvEntry m] -data EnvEntry where- (:==) :: (Show a, Typeable a) => Var a -> a -> EnvEntry+data EnvEntry m where+ (:==) :: Typeable a => Var a -> Realized m a -> EnvEntry m infix 5 :== -deriving instance Show EnvEntry+pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m+pattern v :=? val <- (viewAtType -> Just (v, val)) -lookUpVarMaybe :: Typeable a => Env -> Var a -> Maybe a+viewAtType :: forall a m. Typeable a => EnvEntry m -> Maybe (Var a, Realized m 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 [] _ = Nothing-lookUpVarMaybe ((v' :== a) : env) v =- case cast (v', a) of- Just (v'', a') | v == v'' -> Just a'+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 -> Var a -> a+lookUpVar :: Typeable a => Env m -> Var a -> Realized m a lookUpVar env v = case lookUpVarMaybe env v of Nothing -> error $ "Variable " ++ show v ++ " is not bound!" Just a -> a -invertLookupVarMaybe :: (Typeable a, Eq a) => Env -> a -> Maybe (Var a)-invertLookupVarMaybe [] _ = Nothing-invertLookupVarMaybe ((v :== a) : env) a' =- case cast (v, a) of- Just (v', a'') | a' == a'' -> Just v'- _ -> invertLookupVarMaybe env a'- data Any f where- Some :: (Show a, Typeable a, Eq (f a)) => f a -> Any f+ Some :: (Typeable a, Eq (f a)) => f a -> Any f Error :: String -> Any f deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))@@ -194,7 +192,7 @@ data Step state where (:=) ::- (Show a, Typeable a, Eq (Action state a), Show (Action state a)) =>+ (Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state@@ -238,11 +236,11 @@ | d > 10 = ("(" ++) . shows (Actions as) . (")" ++) | null as = ("Actions []" ++) | otherwise =- ("Actions \n [" ++)- . foldr- (.)- (shows (last as) . ("]" ++))- [shows a . (",\n " ++) | a <- init as]+ ("Actions \n [" ++)+ . foldr+ (.)+ (shows (last as) . ("]" ++))+ [shows a . (",\n " ++) | a <- init as] instance (StateModel state) => Arbitrary (Actions state) where arbitrary = do@@ -272,14 +270,14 @@ go m n rej | m > n = return (Nothing, rej) | otherwise = do- a <- resize m $ arbitraryAction s- case a of- Some act ->- if precondition s act- then return (Just (Some act), rej)- else go (m + 1) n (actionName act : rej)- Error _ ->- go (m + 1) n rej+ a <- resize m $ arbitraryAction s+ case a of+ Some act ->+ if precondition s act+ then return (Just (Some act), rej)+ else go (m + 1) n (actionName act : rej)+ Error _ ->+ go (m + 1) n rej shrink (Actions_ rs as) = map (Actions_ rs) (shrinkSmart (map (prune . map fst) . shrinkList shrinker . withStates) as)@@ -292,9 +290,9 @@ loop _s [] = [] loop s ((var := act) : as) | precondition s act =- (var := act) : loop (nextState s act var) as+ (var := act) : loop (nextState s act var) as | otherwise =- loop s as+ loop s as withStates :: StateModel state => [Step state] -> [(Step state, state)] withStates = loop initialState@@ -311,20 +309,18 @@ runActions :: forall state m.- (StateModel state, Monad m) =>- RunModel state m ->+ (StateModel state, RunModel state m) => Actions state ->- PropertyM m (state, Env)+ PropertyM m (state, Env m) runActions = runActionsInState @_ @m initialState runActionsInState :: forall state m.- (StateModel state, Monad m) =>+ (StateModel state, RunModel state m) => state ->- RunModel state m -> Actions state ->- PropertyM m (state, Env)-runActionsInState state RunModel{..} (Actions_ rejected (Smart _ actions)) = loop state [] actions+ PropertyM m (state, Env m)+runActionsInState st (Actions_ rejected (Smart _ actions)) = loop st [] actions where loop _s env [] = do unless (null rejected) $@@ -335,8 +331,10 @@ ret <- run (perform s act (lookUpVar env)) let name = actionName act monitor (tabulate "Actions" [name])- let s' = nextState s act (Var n)- env' = (Var n :== ret) : env- monitor (monitoring (s, s') act (lookUpVar env') ret)- assert $ postcondition s act (lookUpVar env) ret+ let var = Var n+ s' = nextState s act var+ env' = (var :== ret) : env+ monitor (monitoring @state @m (s, s') act (lookUpVar env') ret)+ b <- run $ postcondition (s, s') act (lookUpVar env) ret+ assert b loop s' env' as