{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RecordWildCards #-}

-- | 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 = [String] -> String
forall a. [a] -> a
head ([String] -> String)
-> (Action state a -> [String]) -> Action state a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words (String -> [String])
-> (Action state a -> String) -> Action state a -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action state a -> String
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 :: (state, state) -> Action state a -> LookUp -> a -> Property -> Property
  monitoring (state, state)
_ Action state a
_ LookUp
_ a
_ = Property -> Property
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 {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 :: [EnvEntry] -> Var a -> Maybe a
lookUpVarMaybe [] Var a
_ = Maybe a
forall a. Maybe a
Nothing
lookUpVarMaybe ((Var a
v' :== a
a) : [EnvEntry]
env) Var a
v =
  case (Var a, a) -> Maybe (Var a, a)
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 Var a -> Var a -> Bool
forall a. Eq a => a -> a -> Bool
== Var a
v'' -> a -> Maybe a
forall a. a -> Maybe a
Just a
a'
    Maybe (Var a, a)
_ -> [EnvEntry] -> Var a -> Maybe a
forall a. Typeable a => [EnvEntry] -> Var a -> Maybe a
lookUpVarMaybe [EnvEntry]
env Var a
v

lookUpVar :: Typeable a => Env -> Var a -> a
lookUpVar :: [EnvEntry] -> Var a -> a
lookUpVar [EnvEntry]
env Var a
v = case [EnvEntry] -> Var a -> Maybe a
forall a. Typeable a => [EnvEntry] -> Var a -> Maybe a
lookUpVarMaybe [EnvEntry]
env Var a
v of
  Maybe a
Nothing -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Variable " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Var a -> String
forall a. Show a => a -> String
show Var a
v String -> ShowS
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 :: [EnvEntry] -> a -> Maybe (Var a)
invertLookupVarMaybe [] a
_ = Maybe (Var a)
forall a. Maybe a
Nothing
invertLookupVarMaybe ((Var a
v :== a
a) : [EnvEntry]
env) a
a' =
  case (Var a, a) -> Maybe (Var a, a)
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' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
a'' -> Var a -> Maybe (Var a)
forall a. a -> Maybe a
Just Var a
v'
    Maybe (Var a, a)
_ -> [EnvEntry] -> a -> Maybe (Var 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 (Typeable a, Typeable a) => Maybe (a :~: a)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT @a @b of
      Just a :~: a
Refl -> f a
a f a -> f a -> Bool
forall a. Eq a => a -> a -> Bool
== f a
f a
b
      Maybe (a :~: a)
Nothing -> Bool
False
  Error String
s == Error String
s' = String
s String -> String -> Bool
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
(Var a -> Var a -> Bool) -> (Var a -> Var a -> Bool) -> Eq (Var a)
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, Eq (Var a)
Eq (Var a)
-> (Var a -> Var a -> Ordering)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Bool)
-> (Var a -> Var a -> Var a)
-> (Var a -> Var a -> Var a)
-> Ord (Var a)
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
$cp1Ord :: forall a. Eq (Var a)
Ord, Int -> Var a -> ShowS
[Var a] -> ShowS
Var a -> String
(Int -> Var a -> ShowS)
-> (Var a -> String) -> ([Var a] -> ShowS) -> Show (Var a)
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, Typeable (Var a)
DataType
Constr
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Var a))
-> (Var a -> Constr)
-> (Var a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Var a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a)))
-> ((forall b. Data b => b -> b) -> Var a -> Var a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Var a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Var a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Var a -> m (Var a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Var a -> m (Var a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Var a -> m (Var a))
-> Data (Var a)
Var a -> DataType
Var a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Var a))
(forall b. Data b => b -> b) -> Var a -> Var a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Var a -> c (Var a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Var a)
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 u. Int -> (forall d. Data d => d -> u) -> Var a -> u
forall u. (forall d. Data d => d -> u) -> Var a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Var a -> m (Var a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Var a -> m (Var 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var a))
$cVar :: Constr
$tVar :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> Var a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Var a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j Bool -> Bool -> Bool
&& Action state a -> Any (Action state)
forall a (f :: * -> *).
(Show a, Typeable a, Eq (f a)) =>
f a -> Any f
Some Action state a
act Any (Action state) -> Any (Action state) -> Bool
forall a. Eq a => a -> a -> Bool
== Action state a -> Any (Action state)
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 :: [Step state] -> Actions state
$mActions :: forall r state.
Actions state -> ([Step state] -> r) -> (Void# -> r) -> r
Actions as <-
  Actions_ _ (Smart _ as)
  where
    Actions [Step state]
as = [String] -> Smart [Step state] -> Actions state
forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [] (Int -> [Step state] -> Smart [Step state]
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') = [String] -> Smart [Step state] -> Actions state
forall state. [String] -> Smart [Step state] -> Actions state
Actions_ ([String]
rs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
rs') (Int -> [Step state] -> Smart [Step state]
forall a. Int -> a -> Smart a
Smart Int
k ([Step state]
as [Step state] -> [Step state] -> [Step state]
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 [Step state] -> [Step state] -> Bool
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10 = (String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions state -> ShowS
forall a. Show a => a -> ShowS
shows ([Step state] -> Actions state
forall state. [Step state] -> Actions state
Actions [Step state]
as) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
")" String -> ShowS
forall a. [a] -> [a] -> [a]
++)
    | [Step state] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Step state]
as = (String
"Actions []" String -> ShowS
forall a. [a] -> [a] -> [a]
++)
    | Bool
otherwise =
      (String
"Actions \n [" String -> ShowS
forall a. [a] -> [a] -> [a]
++)
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
          (Step state -> ShowS
forall a. Show a => a -> ShowS
shows ([Step state] -> Step state
forall a. [a] -> a
last [Step state]
as) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"]" String -> ShowS
forall a. [a] -> [a] -> [a]
++))
          [Step state -> ShowS
forall a. Show a => a -> ShowS
shows Step state
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
",\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) | Step state
a <- [Step state] -> [Step state]
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 state
forall state. StateModel state => state
initialState Int
1
    Actions state -> Gen (Actions state)
forall (m :: * -> *) a. Monad m => a -> m a
return (Actions state -> Gen (Actions state))
-> Actions state -> Gen (Actions state)
forall a b. (a -> b) -> a -> b
$ [String] -> Smart [Step state] -> Actions state
forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [String]
rejected (Int -> [Step state] -> Smart [Step state]
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 = (Int -> Gen ([Step state], [String]))
-> Gen ([Step state], [String])
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen ([Step state], [String]))
 -> Gen ([Step state], [String]))
-> (Int -> Gen ([Step state], [String]))
-> Gen ([Step state], [String])
forall a b. (a -> b) -> a -> b
$ \Int
n ->
      let w :: Int
w = Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
       in [(Int, Gen ([Step state], [String]))]
-> Gen ([Step state], [String])
forall a. [(Int, Gen a)] -> Gen a
frequency
            [ (Int
1, ([Step state], [String]) -> Gen ([Step state], [String])
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 (state -> Action state a -> Var a -> state
forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState state
s Action state a
act (Int -> Var a
forall a. Int -> Var a
Var Int
step)) (Int
step Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                      ([Step state], [String]) -> Gen ([Step state], [String])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int -> Var a
forall a. Int -> Var a
Var Int
step Var a -> Action state a -> Step state
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) Step state -> [Step state] -> [Step state]
forall a. a -> [a] -> [a]
: [Step state]
as, [String]
rej [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
rejected)
                    Just Error{} -> String -> Gen ([Step state], [String])
forall a. HasCallStack => String -> a
error String
"impossible"
                    Maybe (Any (Action state))
Nothing ->
                      ([Step state], [String]) -> Gen ([Step state], [String])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [])
              )
            ]
     where
      satisfyPrecondition :: Gen (Maybe (Any (Action state)), [String])
satisfyPrecondition = (Int -> Gen (Maybe (Any (Action state)), [String]))
-> Gen (Maybe (Any (Action state)), [String])
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (Maybe (Any (Action state)), [String]))
 -> Gen (Maybe (Any (Action state)), [String]))
-> (Int -> Gen (Maybe (Any (Action state)), [String]))
-> Gen (Maybe (Any (Action state)), [String])
forall a b. (a -> b) -> a -> b
$ \Int
n -> Int
-> Int -> [String] -> Gen (Maybe (Any (Action state)), [String])
go Int
n (Int
2 Int -> Int -> Int
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = (Maybe (Any (Action state)), [String])
-> Gen (Maybe (Any (Action state)), [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Any (Action state))
forall a. Maybe a
Nothing, [String]
rej)
        | Bool
otherwise = do
          Any (Action state)
a <- Int -> Gen (Any (Action state)) -> Gen (Any (Action state))
forall a. Int -> Gen a -> Gen a
resize Int
m (Gen (Any (Action state)) -> Gen (Any (Action state)))
-> Gen (Any (Action state)) -> Gen (Any (Action state))
forall a b. (a -> b) -> a -> b
$ state -> Gen (Any (Action state))
forall state. StateModel state => state -> Gen (Any (Action state))
arbitraryAction state
s
          case Any (Action state)
a of
            Some Action state a
act ->
              if state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition state
s Action state a
act
                then (Maybe (Any (Action state)), [String])
-> Gen (Maybe (Any (Action state)), [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (Any (Action state) -> Maybe (Any (Action state))
forall a. a -> Maybe a
Just (Action state a -> Any (Action state)
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
n (Action state a -> String
forall state a. StateModel state => Action state a -> String
actionName Action state a
act String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
rej)
            Error String
_ ->
              Int
-> Int -> [String] -> Gen (Maybe (Any (Action state)), [String])
go (Int
m Int -> Int -> Int
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) =
    (Smart [Step state] -> Actions state)
-> [Smart [Step state]] -> [Actions state]
forall a b. (a -> b) -> [a] -> [b]
map ([String] -> Smart [Step state] -> Actions state
forall state. [String] -> Smart [Step state] -> Actions state
Actions_ [String]
rs) (([Step state] -> [[Step state]])
-> Smart [Step state] -> [Smart [Step state]]
forall a. (a -> [a]) -> Smart a -> [Smart a]
shrinkSmart (([(Step state, state)] -> [Step state])
-> [[(Step state, state)]] -> [[Step state]]
forall a b. (a -> b) -> [a] -> [b]
map ([Step state] -> [Step state]
forall state. StateModel state => [Step state] -> [Step state]
prune ([Step state] -> [Step state])
-> ([(Step state, state)] -> [Step state])
-> [(Step state, state)]
-> [Step state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Step state, state) -> Step state)
-> [(Step state, state)] -> [Step state]
forall a b. (a -> b) -> [a] -> [b]
map (Step state, state) -> Step state
forall a b. (a, b) -> a
fst) ([[(Step state, state)]] -> [[Step state]])
-> ([Step state] -> [[(Step state, state)]])
-> [Step state]
-> [[Step state]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Step state, state) -> [(Step state, state)])
-> [(Step state, state)] -> [[(Step state, state)]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Step state, state) -> [(Step state, state)]
forall b. StateModel b => (Step b, b) -> [(Step b, b)]
shrinker ([(Step state, state)] -> [[(Step state, state)]])
-> ([Step state] -> [(Step state, state)])
-> [Step state]
-> [[(Step state, state)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Step state] -> [(Step state, state)]
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) = [(Int -> Var a
forall a. Int -> Var a
Var Int
i Var a -> Action b a -> Step b
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' <- b -> Action b a -> [Any (Action b)]
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 :: [Step state] -> [Step state]
prune = state -> [Step state] -> [Step state]
forall state.
StateModel state =>
state -> [Step state] -> [Step state]
loop state
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)
    | state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition state
s Action state a
act =
      (Var a
var Var a -> Action state a -> Step state
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) Step state -> [Step state] -> [Step state]
forall a. a -> [a] -> [a]
: state -> [Step state] -> [Step state]
loop (state -> Action state a -> Var a -> state
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 :: [Step state] -> [(Step state, state)]
withStates = state -> [Step state] -> [(Step state, state)]
forall state.
StateModel state =>
state -> [Step state] -> [(Step state, state)]
loop state
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 Var a -> Action state a -> Step state
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) (Step state, state)
-> [(Step state, state)] -> [(Step state, state)]
forall a. a -> [a] -> [a]
: state -> [Step state] -> [(Step state, state)]
loop (state -> Action state a -> Var a -> state
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 :: Actions state -> state
stateAfter (Actions [Step state]
actions) = state -> [Step state] -> state
forall state. StateModel state => state -> [Step state] -> state
loop state
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 (state -> Action state a -> Var a -> state
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 :: RunModel state m
-> Actions state -> PropertyM m (state, [EnvEntry])
runActions = state
-> RunModel state m
-> Actions state
-> PropertyM m (state, [EnvEntry])
forall state (m :: * -> *).
(StateModel state, Monad m) =>
state
-> RunModel state m
-> Actions state
-> PropertyM m (state, [EnvEntry])
runActionsInState @_ @m state
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 :: 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
    Bool -> PropertyM m () -> PropertyM m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
rejected) (PropertyM m () -> PropertyM m ())
-> PropertyM m () -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$
      (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions rejected by precondition" [String]
rejected)
    (state, [EnvEntry]) -> PropertyM m (state, [EnvEntry])
forall (m :: * -> *) a. Monad m => a -> m a
return (state
_s, [EnvEntry] -> [EnvEntry]
forall a. [a] -> [a]
reverse [EnvEntry]
env)
  loop state
s [EnvEntry]
env ((Var Int
n := Action state a
act) : [Step state]
as) = do
    Bool -> PropertyM m ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
pre (Bool -> PropertyM m ()) -> Bool -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition state
s Action state a
act
    a
ret <- m a -> PropertyM m a
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (state -> Action state a -> LookUp -> m a
forall a. state -> Action state a -> LookUp -> m a
perform state
s Action state a
act ([EnvEntry] -> Var a -> a
forall a. Typeable a => [EnvEntry] -> Var a -> a
lookUpVar [EnvEntry]
env))
    let name :: String
name = Action state a -> String
forall state a. StateModel state => Action state a -> String
actionName Action state a
act
    (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions" [String
name])
    let s' :: state
s' = state -> Action state a -> Var a -> state
forall state a.
StateModel state =>
state -> Action state a -> Var a -> state
nextState state
s Action state a
act (Int -> Var a
forall a. Int -> Var a
Var Int
n)
        env' :: [EnvEntry]
env' = (Int -> Var a
forall a. Int -> Var a
Var Int
n Var a -> a -> EnvEntry
forall a. (Show a, Typeable a) => Var a -> a -> EnvEntry
:== a
ret) EnvEntry -> [EnvEntry] -> [EnvEntry]
forall a. a -> [a] -> [a]
: [EnvEntry]
env
    (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((state, state)
-> Action state a -> LookUp -> a -> Property -> Property
forall state a.
StateModel state =>
(state, state)
-> Action state a -> LookUp -> a -> Property -> Property
monitoring (state
s, state
s') Action state a
act ([EnvEntry] -> Var a -> a
forall a. Typeable a => [EnvEntry] -> Var a -> a
lookUpVar [EnvEntry]
env') a
ret)
    Bool -> PropertyM m ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert (Bool -> PropertyM m ()) -> Bool -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ state -> Action state a -> LookUp -> a -> Bool
forall state a.
StateModel state =>
state -> Action state a -> LookUp -> a -> Bool
postcondition state
s Action state a
act ([EnvEntry] -> Var a -> a
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