{-# 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. -- -- 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` -- to be asserted by QuickCheck. module Test.QuickCheck.StateModel ( StateModel (..), RunModel (..), Any (..), Step (..), LookUp, Var (..), -- we export the constructors so that users can construct test cases Actions (..), pattern Actions, EnvEntry (..), Env, stateAfter, runActions, runActionsInState, lookUpVar, lookUpVarMaybe, invertLookupVarMaybe, ) where import Control.Monad import Data.Data import Test.QuickCheck as QC import Test.QuickCheck.DynamicLogic.SmartShrinking import Test.QuickCheck.Monadic -- | The typeclass users implement to define a model against which to validate some implementation. -- -- To implement a `StateModel`, user needs to provide at least the following: -- -- * A datatype for `Action`s: Each test case is a sequence of `Action`s that's supposed to lead from -- some `initialState` to some end state, -- * A generator for traces of `Action`s, the `arbitraryAction` function, -- * An `initialState`, -- * A /transition/ function, `nextState`, that "interprets" each `Action` and producing some new `state`. -- -- For finer grained control over the testing process, one can also define: -- -- * `shrinkAction`: Shrinking is an important part of MBT as it allows QuickCheck engine to look for simpler -- test cases when something goes wrong which makes troubleshooting easier, -- * `precondition`: Filters generated `Action` depending on the `state`. When `precondition` is False then -- 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 ) => StateModel state where -- | The type of `Action` relevant for this `state`. -- -- This is expected to be defined as a GADT where the `a` parameter is instantiated to some -- observable output from the SUT a given action is expected to produce. For example, here -- is a fragment of the `Action RegState` (taken from the `Spec.Dynamic.RegistryModel` module) : -- -- @ -- data Action RegState a where -- Spawn :: Action RegState ThreadId -- Register :: String -> Var ThreadId -> Action RegState (Either ErrorCall ()) -- KillThread :: Var ThreadId -> Action RegState () -- @ -- -- The @Spawn@ action should produce a @ThreadId@, whereas the @KillThread@ action does not return -- anything. data Action state a -- | Display name for `Action`. -- This is useful to provide sensible statistics about the distribution of `Action`s run -- when checking a property. -- -- Default implementation uses a poor-man's string manipulation method to extract the -- constructor name from the value. actionName :: Action state a -> String actionName = forall a. [a] -> a head forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> [String] words forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. Show a => a -> String show -- | Generator for `Action` depending on `state`. -- The generated values are wrapped in `Any` type to allow the model to /not/ generate an action under -- some circumstances: Any generated `Error` value will be ignored when generating a trace for testing. arbitraryAction :: state -> Gen (Any (Action state)) -- | 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 state _ Action state a _ = [] -- | Initial state of generated traces. initialState :: state -- | Transition function for the model. -- The `Var a` parameter is useful to keep reference to actual value of type `a` produced -- 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 state s Action state a _ Var a _ = state s -- | Precondition for filtering generated `Action`. -- This function is applied before the action is performed, it is useful to refine generators that -- can produce more values than are useful. precondition :: state -> Action state a -> Bool precondition state _ Action state a _ = Bool True -- | 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 state _ Action state a _ LookUp _ a _ = Bool 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 (state, state) _ Action state a _ LookUp _ a _ = forall a. a -> a 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 {forall state (m :: * -> *). RunModel state m -> forall a. state -> Action state a -> LookUp -> m a perform :: forall a. state -> Action state a -> LookUp -> m a} type LookUp = forall a. Typeable a => Var a -> a type Env = [EnvEntry] data EnvEntry where (:==) :: (Show a, Typeable a) => Var a -> a -> EnvEntry infix 5 :== deriving instance Show EnvEntry lookUpVarMaybe :: Typeable a => Env -> Var a -> Maybe a lookUpVarMaybe :: forall a. Typeable a => [EnvEntry] -> Var a -> Maybe a lookUpVarMaybe [] Var a _ = forall a. Maybe a Nothing lookUpVarMaybe ((Var a v' :== a a) : [EnvEntry] env) Var a v = case forall a b. (Typeable a, Typeable b) => a -> Maybe b cast (Var a v', a a) of Just (Var a v'', a a') | Var a v forall a. Eq a => a -> a -> Bool == Var a v'' -> forall a. a -> Maybe a Just a a' Maybe (Var a, a) _ -> forall a. Typeable a => [EnvEntry] -> Var a -> Maybe a lookUpVarMaybe [EnvEntry] env Var a v lookUpVar :: Typeable a => Env -> Var a -> a lookUpVar :: forall a. Typeable a => [EnvEntry] -> Var a -> a lookUpVar [EnvEntry] env Var a v = case forall a. Typeable a => [EnvEntry] -> Var a -> Maybe a lookUpVarMaybe [EnvEntry] env Var a v of Maybe a Nothing -> forall a. HasCallStack => String -> a error forall a b. (a -> b) -> a -> b $ String "Variable " forall a. [a] -> [a] -> [a] ++ forall a. Show a => a -> String show Var a v forall a. [a] -> [a] -> [a] ++ String " is not bound!" Just a a -> a a invertLookupVarMaybe :: (Typeable a, Eq a) => Env -> a -> Maybe (Var a) invertLookupVarMaybe :: forall a. (Typeable a, Eq a) => [EnvEntry] -> a -> Maybe (Var a) invertLookupVarMaybe [] a _ = forall a. Maybe a Nothing invertLookupVarMaybe ((Var a v :== a a) : [EnvEntry] env) a a' = case forall a b. (Typeable a, Typeable b) => a -> Maybe b cast (Var a v, a a) of Just (Var a v', a a'') | a a' forall a. Eq a => a -> a -> Bool == a a'' -> forall a. a -> Maybe a Just Var a v' Maybe (Var a, a) _ -> forall a. (Typeable a, Eq a) => [EnvEntry] -> a -> Maybe (Var a) invertLookupVarMaybe [EnvEntry] env a a' data Any f where Some :: (Show a, 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)) instance Eq (Any f) where Some (f a a :: f a) == :: Any f -> Any f -> Bool == Some (f a b :: f b) = case forall {k} (a :: k) (b :: k). (Typeable a, Typeable b) => Maybe (a :~: b) eqT @a @b of Just a :~: a Refl -> f a a forall a. Eq a => a -> a -> Bool == f a b Maybe (a :~: a) Nothing -> Bool False Error String s == Error String s' = String s forall a. Eq a => a -> a -> Bool == String s' Any f _ == Any f _ = Bool False data Step state where (:=) :: (Show a, Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state infix 5 := deriving instance (forall a. Show (Action state a)) => Show (Step state) newtype Var a = Var Int deriving (Var a -> Var a -> Bool forall a. Var a -> Var a -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Var a -> Var a -> Bool $c/= :: forall a. Var a -> Var a -> Bool == :: Var a -> Var a -> Bool $c== :: forall a. Var a -> Var a -> Bool Eq, Var a -> Var a -> Bool Var a -> Var a -> Ordering Var a -> Var a -> Var a forall a. Eq (Var a) forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a forall a. Var a -> Var a -> Bool forall a. Var a -> Var a -> Ordering forall a. Var a -> Var a -> Var a min :: Var a -> Var a -> Var a $cmin :: forall a. Var a -> Var a -> Var a max :: Var a -> Var a -> Var a $cmax :: forall a. Var a -> Var a -> Var a >= :: Var a -> Var a -> Bool $c>= :: forall a. Var a -> Var a -> Bool > :: Var a -> Var a -> Bool $c> :: forall a. Var a -> Var a -> Bool <= :: Var a -> Var a -> Bool $c<= :: forall a. Var a -> Var a -> Bool < :: Var a -> Var a -> Bool $c< :: forall a. Var a -> Var a -> Bool compare :: Var a -> Var a -> Ordering $ccompare :: forall a. Var a -> Var a -> Ordering Ord, Int -> Var a -> ShowS forall a. Int -> Var a -> ShowS forall a. [Var a] -> ShowS forall a. Var a -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Var a] -> ShowS $cshowList :: forall a. [Var a] -> ShowS show :: Var a -> String $cshow :: forall a. Var a -> String showsPrec :: Int -> Var a -> ShowS $cshowsPrec :: forall a. Int -> Var a -> ShowS Show, Typeable, Var a -> DataType Var a -> Constr forall {a}. Data a => Typeable (Var a) forall a. Data a => Var a -> DataType forall a. Data a => Var a -> Constr forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a forall a u. Data a => Int -> (forall d. Data d => d -> u) -> Var a -> u forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u] forall a r r'. Data a => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r forall a r r'. Data a => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r forall a (m :: * -> *). (Data a, Monad m) => (forall d. Data d => d -> m d) -> Var a -> m (Var a) forall a (m :: * -> *). (Data a, MonadPlus m) => (forall d. Data d => d -> m d) -> Var a -> m (Var a) forall a (c :: * -> *). Data a => (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var a) forall a (c :: * -> *). Data a => (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var a -> c (Var a) forall a (t :: * -> *) (c :: * -> *). (Data a, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c (Var a)) forall a (t :: * -> * -> *) (c :: * -> *). (Data a, Typeable t) => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a)) forall a. Typeable a -> (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var a) forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var a -> c (Var a) forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Var a)) gmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Var a -> m (Var a) $cgmapMo :: forall a (m :: * -> *). (Data a, MonadPlus m) => (forall d. Data d => d -> m d) -> Var a -> m (Var a) gmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Var a -> m (Var a) $cgmapMp :: forall a (m :: * -> *). (Data a, MonadPlus m) => (forall d. Data d => d -> m d) -> Var a -> m (Var a) gmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Var a -> m (Var a) $cgmapM :: forall a (m :: * -> *). (Data a, Monad m) => (forall d. Data d => d -> m d) -> Var a -> m (Var a) gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Var a -> u $cgmapQi :: forall a u. Data a => Int -> (forall d. Data d => d -> u) -> Var a -> u gmapQ :: forall u. (forall d. Data d => d -> u) -> Var a -> [u] $cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u] gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r $cgmapQr :: forall a r r'. Data a => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r gmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r $cgmapQl :: forall a r r'. Data a => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r gmapT :: (forall b. Data b => b -> b) -> Var a -> Var a $cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Var a -> Var a dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a)) $cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *). (Data a, Typeable t) => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a)) dataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Var a)) $cdataCast1 :: forall a (t :: * -> *) (c :: * -> *). (Data a, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c (Var a)) dataTypeOf :: Var a -> DataType $cdataTypeOf :: forall a. Data a => Var a -> DataType toConstr :: Var a -> Constr $ctoConstr :: forall a. Data a => Var a -> Constr gunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var a) $cgunfold :: forall a (c :: * -> *). Data a => (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var a) gfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var a -> c (Var a) $cgfoldl :: forall a (c :: * -> *). Data a => (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var a -> c (Var a) Data) instance Eq (Step state) where (Var Int i := Action state a act) == :: Step state -> Step state -> Bool == (Var Int j := Action state a act') = Int i forall a. Eq a => a -> a -> Bool == Int j Bool -> Bool -> Bool && forall a (f :: * -> *). (Show a, Typeable a, Eq (f a)) => f a -> Any f Some Action state a act forall a. Eq a => a -> a -> Bool == forall a (f :: * -> *). (Show a, Typeable a, Eq (f a)) => f a -> Any f Some Action state a act' -- Action sequences use Smart shrinking, but this is invisible to -- client code because the extra Smart constructor is concealed by a -- pattern synonym. -- We also collect a list of names of actions which were generated, -- but were then rejected by their precondition. data Actions state = Actions_ [String] (Smart [Step state]) pattern Actions :: [Step state] -> Actions state pattern $bActions :: forall state. [Step state] -> Actions state $mActions :: forall {r} {state}. Actions state -> ([Step state] -> r) -> ((# #) -> r) -> r Actions as <- Actions_ _ (Smart _ as) where Actions [Step state] as = forall state. [String] -> Smart [Step state] -> Actions state Actions_ [] (forall a. Int -> a -> Smart a Smart Int 0 [Step state] as) {-# COMPLETE Actions #-} instance Semigroup (Actions state) where Actions_ [String] rs (Smart Int k [Step state] as) <> :: Actions state -> Actions state -> Actions state <> Actions_ [String] rs' (Smart Int _ [Step state] as') = forall state. [String] -> Smart [Step state] -> Actions state Actions_ ([String] rs forall a. [a] -> [a] -> [a] ++ [String] rs') (forall a. Int -> a -> Smart a Smart Int k ([Step state] as forall a. Semigroup a => a -> a -> a <> [Step state] as')) instance Eq (Actions state) where Actions [Step state] as == :: Actions state -> Actions state -> Bool == Actions [Step state] as' = [Step state] as forall a. Eq a => a -> a -> Bool == [Step state] as' instance (forall a. Show (Action state a)) => Show (Actions state) where showsPrec :: Int -> Actions state -> ShowS showsPrec Int d (Actions [Step state] as) | Int d forall a. Ord a => a -> a -> Bool > Int 10 = (String "(" forall a. [a] -> [a] -> [a] ++) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. Show a => a -> ShowS shows (forall state. [Step state] -> Actions state Actions [Step state] as) forall b c a. (b -> c) -> (a -> b) -> a -> c . (String ")" forall a. [a] -> [a] -> [a] ++) | forall (t :: * -> *) a. Foldable t => t a -> Bool null [Step state] as = (String "Actions []" forall a. [a] -> [a] -> [a] ++) | Bool otherwise = (String "Actions \n [" forall a. [a] -> [a] -> [a] ++) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr forall b c a. (b -> c) -> (a -> b) -> a -> c (.) (forall a. Show a => a -> ShowS shows (forall a. [a] -> a last [Step state] as) forall b c a. (b -> c) -> (a -> b) -> a -> c . (String "]" forall a. [a] -> [a] -> [a] ++)) [forall a. Show a => a -> ShowS shows Step state a forall b c a. (b -> c) -> (a -> b) -> a -> c . (String ",\n " forall a. [a] -> [a] -> [a] ++) | Step state a <- forall a. [a] -> [a] init [Step state] as] instance (StateModel state) => Arbitrary (Actions state) where arbitrary :: Gen (Actions state) arbitrary = do ([Step state] as, [String] rejected) <- state -> Int -> Gen ([Step state], [String]) arbActions forall state. StateModel state => state initialState Int 1 forall (m :: * -> *) a. Monad m => a -> m a return forall a b. (a -> b) -> a -> b $ forall state. [String] -> Smart [Step state] -> Actions state Actions_ [String] rejected (forall a. Int -> a -> Smart a Smart Int 0 [Step state] as) where arbActions :: state -> Int -> Gen ([Step state], [String]) arbActions :: state -> Int -> Gen ([Step state], [String]) arbActions state s Int step = forall a. (Int -> Gen a) -> Gen a sized forall a b. (a -> b) -> a -> b $ \Int n -> let w :: Int w = Int n forall a. Integral a => a -> a -> a `div` Int 2 forall a. Num a => a -> a -> a + Int 1 in forall a. [(Int, Gen a)] -> Gen a frequency [ (Int 1, forall (m :: * -> *) a. Monad m => a -> m a return ([], [])) , ( Int w , do (Maybe (Any (Action state)) mact, [String] rej) <- Gen (Maybe (Any (Action state)), [String]) satisfyPrecondition case Maybe (Any (Action state)) mact of Just (Some Action state a act) -> do ([Step state] as, [String] rejected) <- state -> Int -> Gen ([Step state], [String]) arbActions (forall state a. StateModel state => state -> Action state a -> Var a -> state nextState state s Action state a act (forall a. Int -> Var a Var Int step)) (Int step forall a. Num a => a -> a -> a + Int 1) forall (m :: * -> *) a. Monad m => a -> m a return ((forall a. Int -> Var a Var Int step forall a state. (Show a, Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state := Action state a act) forall a. a -> [a] -> [a] : [Step state] as, [String] rej forall a. [a] -> [a] -> [a] ++ [String] rejected) Just Error{} -> forall a. HasCallStack => String -> a error String "impossible" Maybe (Any (Action state)) Nothing -> forall (m :: * -> *) a. Monad m => a -> m a return ([], []) ) ] where satisfyPrecondition :: Gen (Maybe (Any (Action state)), [String]) satisfyPrecondition = forall a. (Int -> Gen a) -> Gen a sized forall a b. (a -> b) -> a -> b $ \Int n -> Int -> Int -> [String] -> Gen (Maybe (Any (Action state)), [String]) go Int n (Int 2 forall a. Num a => a -> a -> a * Int n) [] -- idea copied from suchThatMaybe go :: Int -> Int -> [String] -> Gen (Maybe (Any (Action state)), [String]) go Int m Int n [String] rej | Int m forall a. Ord a => a -> a -> Bool > Int n = forall (m :: * -> *) a. Monad m => a -> m a return (forall a. Maybe a Nothing, [String] rej) | Bool otherwise = do Any (Action state) a <- forall a. Int -> Gen a -> Gen a resize Int m forall a b. (a -> b) -> a -> b $ forall state. StateModel state => state -> Gen (Any (Action state)) arbitraryAction state s case Any (Action state) a of Some Action state a act -> if forall state a. StateModel state => state -> Action state a -> Bool precondition state s Action state a act then forall (m :: * -> *) a. Monad m => a -> m a return (forall a. a -> Maybe a Just (forall a (f :: * -> *). (Show a, Typeable a, Eq (f a)) => f a -> Any f Some Action state a act), [String] rej) else Int -> Int -> [String] -> Gen (Maybe (Any (Action state)), [String]) go (Int m forall a. Num a => a -> a -> a + Int 1) Int n (forall state a. StateModel state => Action state a -> String actionName Action state a act forall a. a -> [a] -> [a] : [String] rej) Error String _ -> Int -> Int -> [String] -> Gen (Maybe (Any (Action state)), [String]) go (Int m forall a. Num a => a -> a -> a + Int 1) Int n [String] rej shrink :: Actions state -> [Actions state] shrink (Actions_ [String] rs Smart [Step state] as) = forall a b. (a -> b) -> [a] -> [b] map (forall state. [String] -> Smart [Step state] -> Actions state Actions_ [String] rs) (forall a. (a -> [a]) -> Smart a -> [Smart a] shrinkSmart (forall a b. (a -> b) -> [a] -> [b] map (forall state. StateModel state => [Step state] -> [Step state] prune forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a b. (a -> b) -> [a] -> [b] map forall a b. (a, b) -> a fst) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall a. (a -> [a]) -> [a] -> [[a]] shrinkList forall {b}. StateModel b => (Step b, b) -> [(Step b, b)] shrinker forall b c a. (b -> c) -> (a -> b) -> a -> c . forall state. StateModel state => [Step state] -> [(Step state, state)] withStates) Smart [Step state] as) where shrinker :: (Step b, b) -> [(Step b, b)] shrinker (Var Int i := Action b a act, b s) = [(forall a. Int -> Var a Var Int i forall a state. (Show a, Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state := Action b a act', b s) | Some Action b a act' <- forall state a. (StateModel state, Show a, Typeable a) => state -> Action state a -> [Any (Action state)] shrinkAction b s Action b a act] prune :: StateModel state => [Step state] -> [Step state] prune :: forall state. StateModel state => [Step state] -> [Step state] prune = forall {state}. StateModel state => state -> [Step state] -> [Step state] loop forall state. StateModel state => state initialState where loop :: state -> [Step state] -> [Step state] loop state _s [] = [] loop state s ((Var a var := Action state a act) : [Step state] as) | forall state a. StateModel state => state -> Action state a -> Bool precondition state s Action state a act = (Var a var forall a state. (Show a, Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state := Action state a act) forall a. a -> [a] -> [a] : state -> [Step state] -> [Step state] loop (forall state a. StateModel state => state -> Action state a -> Var a -> state nextState state s Action state a act Var a var) [Step state] as | Bool otherwise = state -> [Step state] -> [Step state] loop state s [Step state] as withStates :: StateModel state => [Step state] -> [(Step state, state)] withStates :: forall state. StateModel state => [Step state] -> [(Step state, state)] withStates = forall {state}. StateModel state => state -> [Step state] -> [(Step state, state)] loop forall state. StateModel state => state initialState where loop :: state -> [Step state] -> [(Step state, state)] loop state _s [] = [] loop state s ((Var a var := Action state a act) : [Step state] as) = (Var a var forall a state. (Show a, Typeable a, Eq (Action state a), Show (Action state a)) => Var a -> Action state a -> Step state := Action state a act, state s) forall a. a -> [a] -> [a] : state -> [Step state] -> [(Step state, state)] loop (forall state a. StateModel state => state -> Action state a -> Var a -> state nextState state s Action state a act Var a var) [Step state] as stateAfter :: StateModel state => Actions state -> state stateAfter :: forall state. StateModel state => Actions state -> state stateAfter (Actions [Step state] actions) = forall {state}. StateModel state => state -> [Step state] -> state loop forall state. StateModel state => state initialState [Step state] actions where loop :: state -> [Step state] -> state loop state s [] = state s loop state s ((Var a var := Action state a act) : [Step state] as) = state -> [Step state] -> state loop (forall state a. StateModel state => state -> Action state a -> Var a -> state nextState state s Action state a act Var a var) [Step state] as runActions :: forall state m. (StateModel state, Monad m) => RunModel state m -> Actions state -> PropertyM m (state, Env) runActions :: forall state (m :: * -> *). (StateModel state, Monad m) => RunModel state m -> Actions state -> PropertyM m (state, [EnvEntry]) runActions = forall state (m :: * -> *). (StateModel state, Monad m) => state -> RunModel state m -> Actions state -> PropertyM m (state, [EnvEntry]) runActionsInState @_ @m forall state. StateModel state => state initialState runActionsInState :: forall state m. (StateModel state, Monad m) => state -> RunModel state m -> Actions state -> PropertyM m (state, Env) runActionsInState :: forall state (m :: * -> *). (StateModel state, Monad m) => state -> RunModel state m -> Actions state -> PropertyM m (state, [EnvEntry]) runActionsInState state state RunModel{forall a. state -> Action state a -> LookUp -> m a perform :: forall a. state -> Action state a -> LookUp -> m a perform :: forall state (m :: * -> *). RunModel state m -> forall a. state -> Action state a -> LookUp -> m a ..} (Actions_ [String] rejected (Smart Int _ [Step state] actions)) = state -> [EnvEntry] -> [Step state] -> PropertyM m (state, [EnvEntry]) loop state state [] [Step state] actions where loop :: state -> [EnvEntry] -> [Step state] -> PropertyM m (state, [EnvEntry]) loop state _s [EnvEntry] env [] = do forall (f :: * -> *). Applicative f => Bool -> f () -> f () unless (forall (t :: * -> *) a. Foldable t => t a -> Bool null [String] rejected) forall a b. (a -> b) -> a -> b $ forall (m :: * -> *). Monad m => (Property -> Property) -> PropertyM m () monitor (forall prop. Testable prop => String -> [String] -> prop -> Property tabulate String "Actions rejected by precondition" [String] rejected) forall (m :: * -> *) a. Monad m => a -> m a return (state _s, forall a. [a] -> [a] reverse [EnvEntry] env) loop state s [EnvEntry] env ((Var Int n := Action state a act) : [Step state] as) = do forall (m :: * -> *). Monad m => Bool -> PropertyM m () pre forall a b. (a -> b) -> a -> b $ forall state a. StateModel state => state -> Action state a -> Bool precondition state s Action state a act a ret <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a run (forall a. state -> Action state a -> LookUp -> m a perform state s Action state a act (forall a. Typeable a => [EnvEntry] -> Var a -> a lookUpVar [EnvEntry] env)) let name :: String name = forall state a. StateModel state => Action state a -> String actionName Action state a act forall (m :: * -> *). Monad m => (Property -> Property) -> PropertyM m () monitor (forall prop. Testable prop => String -> [String] -> prop -> Property tabulate String "Actions" [String name]) let s' :: state s' = forall state a. StateModel state => state -> Action state a -> Var a -> state nextState state s Action state a act (forall a. Int -> Var a Var Int n) env' :: [EnvEntry] env' = (forall a. Int -> Var a Var Int n forall a. (Show a, Typeable a) => Var a -> a -> EnvEntry :== a ret) forall a. a -> [a] -> [a] : [EnvEntry] env forall (m :: * -> *). Monad m => (Property -> Property) -> PropertyM m () monitor (forall state a. (StateModel state, Show a) => (state, state) -> Action state a -> LookUp -> a -> Property -> Property monitoring (state s, state s') Action state a act (forall a. Typeable a => [EnvEntry] -> Var a -> a lookUpVar [EnvEntry] env') a ret) forall (m :: * -> *). Monad m => Bool -> PropertyM m () assert forall a b. (a -> b) -> a -> b $ forall state a. StateModel state => state -> Action state a -> LookUp -> a -> Bool postcondition state s Action state a act (forall a. Typeable a => [EnvEntry] -> Var a -> a lookUpVar [EnvEntry] env) a ret state -> [EnvEntry] -> [Step state] -> PropertyM m (state, [EnvEntry]) loop state s' [EnvEntry] env' [Step state] as