{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# 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 (
  module Test.QuickCheck.StateModel.Variables,
  StateModel (..),
  RunModel (..),
  PostconditionM (..),
  WithUsedVars (..),
  Annotated (..),
  Step (..),
  LookUp,
  Actions (..),
  pattern Actions,
  EnvEntry (..),
  pattern (:=?),
  Env,
  Realized,
  Generic,
  monitorPost,
  counterexamplePost,
  stateAfter,
  runActions,
  lookUpVar,
  lookUpVarMaybe,
  initialAnnotatedState,
  computeNextState,
  computePrecondition,
  computeArbitraryAction,
  computeShrinkAction,
) where

import Control.Monad
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer (Endo (..), WriterT, runWriterT, tell)
import Data.Data
import Data.Kind
import Data.List
import Data.Set qualified as Set
import GHC.Generics
import Test.QuickCheck as QC
import Test.QuickCheck.DynamicLogic.SmartShrinking
import Test.QuickCheck.Monadic
import Test.QuickCheck.StateModel.Variables

-- | 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,
class
  ( forall a. Show (Action state a)
  , forall a. HasVariables (Action state a)
  , Show state
  , HasVariables 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`.
  arbitraryAction :: VarContext -> 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 :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]
  shrinkAction VarContext
_ 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 :: Typeable a => 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

deriving instance (forall a. Show (Action state a)) => Show (Any (Action state))

-- 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 {forall (m :: * -> *) a.
PostconditionM m a -> WriterT (Endo Property, Endo Property) m a
runPost :: WriterT (Endo Property, Endo Property) m a}
  deriving (forall a b. a -> PostconditionM m b -> PostconditionM m a
forall a b. (a -> b) -> PostconditionM m a -> PostconditionM m b
forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM m b -> PostconditionM m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM m a -> PostconditionM m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> PostconditionM m b -> PostconditionM m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM m b -> PostconditionM m a
fmap :: forall a b. (a -> b) -> PostconditionM m a -> PostconditionM m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM m a -> PostconditionM m b
Functor, forall a. a -> PostconditionM m a
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall a b.
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
forall a b c.
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall {m :: * -> *}. Applicative m => Functor (PostconditionM m)
forall (m :: * -> *) a. Applicative m => a -> PostconditionM m a
forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
<* :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
*> :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
liftA2 :: forall a b c.
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
<*> :: forall a b.
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
pure :: forall a. a -> PostconditionM m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> PostconditionM m a
Applicative, forall a. a -> PostconditionM m a
forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall a b.
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
forall {m :: * -> *}. Monad m => Applicative (PostconditionM m)
forall (m :: * -> *) a. Monad m => a -> PostconditionM m a
forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> PostconditionM m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> PostconditionM m a
>> :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
>>= :: forall a b.
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a
-> (a -> PostconditionM m b) -> PostconditionM m b
Monad, forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
MonadTrans)

-- | Apply the property transformation to the property after evaluating
-- the postcondition. Useful for collecting statistics while avoiding
-- duplication between `monitoring` and `postcondition`.
monitorPost :: Monad m => (Property -> Property) -> PostconditionM m ()
monitorPost :: forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PostconditionM m ()
monitorPost Property -> Property
m = forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a. (a -> a) -> Endo a
Endo Property -> Property
m, forall a. Monoid a => a
mempty)

-- | Acts as `Test.QuickCheck.counterexample` if the postcondition fails.
counterexamplePost :: Monad m => String -> PostconditionM m ()
counterexamplePost :: forall (m :: * -> *). Monad m => String -> PostconditionM m ()
counterexamplePost String
c = forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (forall a. Monoid a => a
mempty, forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => String -> prop -> Property
counterexample String
c)

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 :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool
  postcondition (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
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 :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property
  monitoring (state, state)
_ Action state a
_ LookUp m
_ Realized m a
_ Property
prop = Property
prop

type LookUp m = forall a. Typeable a => Var a -> Realized m a

type Env m = [EnvEntry m]

data EnvEntry m where
  (:==) :: Typeable a => Var a -> Realized m a -> EnvEntry m

infix 5 :==

pattern (:=?) :: forall a m. Typeable a => Var a -> Realized m a -> EnvEntry m
pattern v $m:=? :: forall {r} {a} {m :: * -> *}.
Typeable a =>
EnvEntry m -> (Var a -> Realized m a -> r) -> ((# #) -> r) -> r
:=? val <- (viewAtType -> Just (v, val))

viewAtType :: forall a m. Typeable a => EnvEntry m -> Maybe (Var a, Realized m a)
viewAtType :: forall a (m :: * -> *).
Typeable a =>
EnvEntry m -> Maybe (Var a, Realized m a)
viewAtType ((Var a
v :: Var b) :== Realized m a
val)
  | Just a :~: a
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b = forall a. a -> Maybe a
Just (Var a
v, Realized m a
val)
  | Bool
otherwise = forall a. Maybe a
Nothing

lookUpVarMaybe :: forall a m. Typeable a => Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe :: forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe [] Var a
_ = forall a. Maybe a
Nothing
lookUpVarMaybe (((Var a
v' :: Var b) :== Realized m a
a) : [EnvEntry m]
env) Var a
v =
  case forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b of
    Just a :~: a
Refl | Var a
v forall a. Eq a => a -> a -> Bool
== Var a
v' -> forall a. a -> Maybe a
Just Realized m a
a
    Maybe (a :~: a)
_ -> forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe [EnvEntry m]
env Var a
v

lookUpVar :: Typeable a => Env m -> Var a -> Realized m a
lookUpVar :: forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env Var a
v = case forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Maybe (Realized m a)
lookUpVarMaybe Env m
env Var a
v of
  Maybe (Realized m 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 Realized m a
a -> Realized m a
a

data WithUsedVars a = WithUsedVars VarContext a

data Step state where
  (:=) ::
    (Typeable a, Eq (Action state a), Show (Action state a)) =>
    Var a ->
    Action state a ->
    Step state

infix 5 :=

instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where
  getAllVariables :: Step state -> Set (Any Var)
getAllVariables (Var a
var := Action state a
act) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Var a
var) forall a b. (a -> b) -> a -> b
$ forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Action state a
act

instance Show (Step state) where
  show :: Step state -> String
show (Var a
var := Action state a
act) = forall a. Show a => a -> String
show Var a
var forall a. [a] -> [a] -> [a]
++ String
" <- action $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action state a
act

instance Show (WithUsedVars (Step state)) where
  show :: WithUsedVars (Step state) -> String
show (WithUsedVars VarContext
ctx (Var a
var := Action state a
act)) =
    if forall a. Typeable a => Var a -> VarContext -> Bool
isWellTyped Var a
var VarContext
ctx
      then forall a. Show a => a -> String
show Var a
var forall a. [a] -> [a] -> [a]
++ String
" <- action $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action state a
act
      else String
"action $ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Action state a
act

instance Eq (Step state) where
  (Var a
v := Action state a
act) == :: Step state -> Step state -> Bool
== (Var a
v' := Action state a
act') =
    forall a b. Var a -> Var b
unsafeCoerceVar Var a
v forall a. Eq a => a -> a -> Bool
== Var a
v' Bool -> Bool -> Bool
&& forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Action state a
act forall a. Eq a => a -> a -> Bool
== forall a (f :: * -> *). (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])
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x. Rep (Actions state) x -> Actions state
forall state x. Actions state -> Rep (Actions state) x
$cto :: forall state x. Rep (Actions state) x -> Actions state
$cfrom :: forall state x. Actions state -> Rep (Actions state) x
Generic)

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 StateModel state => Show (Actions state) where
  show :: Actions state -> String
show (Actions [Step state]
as) =
    let as' :: [WithUsedVars (Step state)]
as' = forall a. VarContext -> a -> WithUsedVars a
WithUsedVars (forall state. StateModel state => Actions state -> VarContext
usedVariables (forall state. [Step state] -> Actions state
Actions [Step state]
as)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Step state]
as
     in forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. [a] -> [a] -> [a]
(++) (String
"do " forall a. a -> [a] -> [a]
: forall a. a -> [a]
repeat String
"   ") (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [WithUsedVars (Step state)]
as' forall a. [a] -> [a] -> [a]
++ [String
"pure ()"])

usedVariables :: forall state. StateModel state => Actions state -> VarContext
usedVariables :: forall state. StateModel state => Actions state -> VarContext
usedVariables (Actions [Step state]
as) = Annotated state -> [Step state] -> VarContext
go forall state. StateModel state => Annotated state
initialAnnotatedState [Step state]
as
  where
    go :: Annotated state -> [Step state] -> VarContext
    go :: Annotated state -> [Step state] -> VarContext
go Annotated state
aState [] = forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated state
aState)
    go Annotated state
aState ((Var a
var := Action state a
act) : [Step state]
steps) =
      forall a. HasVariables a => a -> VarContext
allVariables Action state a
act
        forall a. Semigroup a => a -> a -> a
<> forall a. HasVariables a => a -> VarContext
allVariables (forall state. Annotated state -> state
underlyingState Annotated state
aState)
        forall a. Semigroup a => a -> a -> a
<> Annotated state -> [Step state] -> VarContext
go (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
aState Action state a
act Var a
var) [Step state]
steps

instance StateModel state => Arbitrary (Actions state) where
  arbitrary :: Gen (Actions state)
arbitrary = do
    ([Step state]
as, [String]
rejected) <- Annotated state -> Int -> Gen ([Step state], [String])
arbActions forall state. StateModel state => Annotated state
initialAnnotatedState 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 :: Annotated state -> Int -> Gen ([Step state], [String])
      arbActions :: Annotated state -> Int -> Gen ([Step state], [String])
arbActions Annotated 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
                        let var :: Var a
var = forall a. Int -> Var a
mkVar Int
step
                        ([Step state]
as, [String]
rejected) <- Annotated state -> Int -> Gen ([Step state], [String])
arbActions (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) (Int
step forall a. Num a => a -> a -> a
+ Int
1)
                        forall (m :: * -> *) a. Monad m => a -> m a
return ((Var a
var forall a state.
(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)
                      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 =>
Annotated state -> Gen (Any (Action state))
computeArbitraryAction Annotated state
s
                case Any (Action state)
a of
                  Some Action state a
act ->
                    if forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated 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 :: * -> *). (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)

  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 {state}.
StateModel state =>
(Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates) Smart [Step state]
as)
    where
      shrinker :: (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker (Var a
v := Action state a
act, Annotated state
s) = [(forall a b. Var a -> Var b
unsafeCoerceVar Var a
v forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action state a
act', Annotated state
s) | Some Action state a
act' <- forall a state.
(Typeable a, StateModel state) =>
Annotated state -> Action state a -> [Any (Action state)]
computeShrinkAction Annotated state
s Action state a
act]

-- Running state models

data Annotated state = Metadata
  { forall state. Annotated state -> VarContext
vars :: VarContext
  , forall state. Annotated state -> state
underlyingState :: state
  }

instance Show state => Show (Annotated state) where
  show :: Annotated state -> String
show (Metadata VarContext
ctx state
s) = forall a. Show a => a -> String
show VarContext
ctx forall a. [a] -> [a] -> [a]
++ String
" |- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show state
s

initialAnnotatedState :: StateModel state => Annotated state
initialAnnotatedState :: forall state. StateModel state => Annotated state
initialAnnotatedState = forall state. VarContext -> state -> Annotated state
Metadata forall a. Monoid a => a
mempty forall state. StateModel state => state
initialState

computePrecondition :: StateModel state => Annotated state -> Action state a -> Bool
computePrecondition :: forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
a =
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Some Var a
v) -> Var a
v forall a. Typeable a => Var a -> VarContext -> Bool
`isWellTyped` forall state. Annotated state -> VarContext
vars Annotated state
s) (forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Action state a
a)
    Bool -> Bool -> Bool
&& forall state a. StateModel state => state -> Action state a -> Bool
precondition (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a

computeNextState ::
  (StateModel state, Typeable a) =>
  Annotated state ->
  Action state a ->
  Var a ->
  Annotated state
computeNextState :: forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
a Var a
v = forall state. VarContext -> state -> Annotated state
Metadata (forall a. Typeable a => VarContext -> Var a -> VarContext
extendContext (forall state. Annotated state -> VarContext
vars Annotated state
s) Var a
v) (forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> Var a -> state
nextState (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a Var a
v)

computeArbitraryAction ::
  StateModel state =>
  Annotated state ->
  Gen (Any (Action state))
computeArbitraryAction :: forall state.
StateModel state =>
Annotated state -> Gen (Any (Action state))
computeArbitraryAction Annotated state
s = forall state.
StateModel state =>
VarContext -> state -> Gen (Any (Action state))
arbitraryAction (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state. Annotated state -> state
underlyingState Annotated state
s)

computeShrinkAction ::
  (Typeable a, StateModel state) =>
  Annotated state ->
  Action state a ->
  [Any (Action state)]
computeShrinkAction :: forall a state.
(Typeable a, StateModel state) =>
Annotated state -> Action state a -> [Any (Action state)]
computeShrinkAction Annotated state
s = forall state a.
(StateModel state, Typeable a) =>
VarContext -> state -> Action state a -> [Any (Action state)]
shrinkAction (forall state. Annotated state -> VarContext
vars Annotated state
s) (forall state. Annotated state -> state
underlyingState Annotated state
s)

prune :: StateModel state => [Step state] -> [Step state]
prune :: forall state. StateModel state => [Step state] -> [Step state]
prune = forall {state}.
StateModel state =>
Annotated state -> [Step state] -> [Step state]
loop forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    loop :: Annotated state -> [Step state] -> [Step state]
loop Annotated state
_s [] = []
    loop Annotated state
s ((Var a
var := Action state a
act) : [Step state]
as)
      | forall state a.
StateModel state =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
act =
          (Var a
var forall a state.
(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]
: Annotated state -> [Step state] -> [Step state]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) [Step state]
as
      | Bool
otherwise =
          Annotated state -> [Step state] -> [Step state]
loop Annotated state
s [Step state]
as

withStates :: StateModel state => [Step state] -> [(Step state, Annotated state)]
withStates :: forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates = forall {state}.
StateModel state =>
Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop forall state. StateModel state => Annotated state
initialAnnotatedState
  where
    loop :: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop Annotated state
_s [] = []
    loop Annotated state
s ((Var a
var := Action state a
act) : [Step state]
as) =
      (Var a
var forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> Action state a -> Step state
:= Action state a
act, Annotated state
s) forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) [Step state]
as

stateAfter :: StateModel state => Actions state -> Annotated state
stateAfter :: forall state. StateModel state => Actions state -> Annotated state
stateAfter (Actions [Step state]
actions) = forall {state}.
StateModel state =>
Annotated state -> [Step state] -> Annotated state
loop forall state. StateModel state => Annotated state
initialAnnotatedState [Step state]
actions
  where
    loop :: Annotated state -> [Step state] -> Annotated state
loop Annotated state
s [] = Annotated state
s
    loop Annotated state
s ((Var a
var := Action state a
act) : [Step state]
as) = Annotated state -> [Step state] -> Annotated state
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var) [Step state]
as

runActions ::
  forall state m.
  (StateModel state, RunModel state m) =>
  Actions state ->
  PropertyM m (Annotated state, Env m)
runActions :: forall state (m :: * -> *).
(StateModel state, RunModel state m) =>
Actions state -> PropertyM m (Annotated state, Env m)
runActions (Actions_ [String]
rejected (Smart Int
_ [Step state]
actions)) = Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop forall state. StateModel state => Annotated state
initialAnnotatedState [] [Step state]
actions
  where
    loop :: Annotated state -> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
    loop :: Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop Annotated state
_s Env m
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 (Annotated state
_s, forall a. [a] -> [a]
reverse Env m
env)
    loop Annotated state
s Env m
env ((Var a
v := 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 =>
Annotated state -> Action state a -> Bool
computePrecondition Annotated state
s Action state a
act
      Realized m a
ret <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (forall state (m :: * -> *) a.
(RunModel state m, Typeable a) =>
state -> Action state a -> LookUp m -> m (Realized m a)
perform (forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
act (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
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 var :: Var a
var = forall a b. Var a -> Var b
unsafeCoerceVar Var a
v
          s' :: Annotated state
s' = forall state a.
(StateModel state, Typeable a) =>
Annotated state -> Action state a -> Var a -> Annotated state
computeNextState Annotated state
s Action state a
act Var a
var
          env' :: Env m
env' = (Var a
var forall a (m :: * -> *).
Typeable a =>
Var a -> Realized m a -> EnvEntry m
:== Realized m a
ret) forall a. a -> [a] -> [a]
: Env m
env
      forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp m
-> Realized m a
-> Property
-> Property
monitoring @state @m (forall state. Annotated state -> state
underlyingState Annotated state
s, forall state. Annotated state -> state
underlyingState Annotated state
s') Action state a
act (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env') Realized m a
ret)
      (Bool
b, (Endo Property -> Property
mon, Endo Property -> Property
onFail)) <- forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
PostconditionM m a -> WriterT (Endo Property, Endo Property) m a
runPost forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp m
-> Realized m a
-> PostconditionM m Bool
postcondition @state @m (forall state. Annotated state -> state
underlyingState Annotated state
s, forall state. Annotated state -> state
underlyingState Annotated state
s') Action state a
act (forall a (m :: * -> *).
Typeable a =>
Env m -> Var a -> Realized m a
lookUpVar Env m
env) Realized m a
ret
      forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor Property -> Property
mon
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor Property -> Property
onFail
      forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
b
      Annotated state
-> Env m -> [Step state] -> PropertyM m (Annotated state, Env m)
loop Annotated state
s' Env m
env' [Step state]
as