{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE UndecidableInstances #-}

-- | 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 (..),
  Polarity (..),
  ActionWithPolarity (..),
  LookUp,
  Actions (..),
  pattern Actions,
  EnvEntry (..),
  pattern (:=?),
  Env,
  Generic,
  IsPerformResult,
  Options (..),
  monitorPost,
  counterexamplePost,
  stateAfter,
  runActions,
  lookUpVar,
  lookUpVarMaybe,
  viewAtType,
  initialAnnotatedState,
  computeNextState,
  computePrecondition,
  computeArbitraryAction,
  computeShrinkAction,
  generateActionsWithOptions,
  shrinkActionsWithOptions,
  defaultOptions,
  moreActions,
) where

import Control.Monad
import Control.Monad.Reader
import Control.Monad.Writer (WriterT, runWriterT, tell)
import Data.Data
import Data.Kind
import Data.List
import Data.Monoid (Endo (..))
import Data.Set qualified as Set
import Data.Void
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,
--  * `validFailingAction`: Specifies when an action that fails it's `precondition` can still run as what is
--    called a _negative_ action. This means that the action is (1) expected to fail and (2) not expected to
--    change the model state. This is very useful for testing the checks and failure conditions in the SUT
--    are implemented correctly. Should it be necessary to update the model state with e.g. book-keeping for
--    a negative action one can define `failureNextState` - but it is generally recommended to let this be
--    as simple an action as possible.
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 ()
  --     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. HasCallStack => [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`.
  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

  -- | Transition function for negative actions. Note that most negative testing applications
  -- should not require an implementation of this function!
  failureNextState :: Typeable a => state -> Action state a -> state
  failureNextState state
s Action state 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

  -- | Precondition for filtering an `Action` that can meaningfully run but is supposed to fail.
  -- An action will run as a _negative_ action if the `precondition` fails and `validFailingAction` succeeds.
  -- A negative action should have _no effect_ on the model state. This may not be desierable in all
  -- situations - in which case one can override this semantics for book-keeping in `failureNextState`.
  validFailingAction :: state -> Action state a -> Bool
  validFailingAction state
_ Action state a
_ = Bool
False

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

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 -> b) -> PostconditionM m a -> PostconditionM m b)
-> (forall a b. a -> PostconditionM m b -> PostconditionM m a)
-> Functor (PostconditionM m)
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
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> PostconditionM m a -> PostconditionM m b
fmap :: forall a b. (a -> b) -> PostconditionM m a -> PostconditionM m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> PostconditionM m b -> PostconditionM m a
<$ :: forall a b. a -> PostconditionM m b -> PostconditionM m a
Functor, Functor (PostconditionM m)
Functor (PostconditionM m) =>
(forall a. a -> PostconditionM m a)
-> (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 a b.
    PostconditionM m a -> PostconditionM m b -> PostconditionM m b)
-> (forall a b.
    PostconditionM m a -> PostconditionM m b -> PostconditionM m a)
-> Applicative (PostconditionM m)
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
$cpure :: forall (m :: * -> *) a. Applicative m => a -> PostconditionM m a
pure :: forall a. a -> PostconditionM m a
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
<*> :: forall a b.
PostconditionM m (a -> b)
-> PostconditionM m a -> PostconditionM m b
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
liftA2 :: forall a b c.
(a -> b -> c)
-> PostconditionM m a -> PostconditionM m b -> PostconditionM m c
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
*> :: 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 a
<* :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m a
Applicative, Applicative (PostconditionM m)
Applicative (PostconditionM m) =>
(forall a b.
 PostconditionM m a
 -> (a -> PostconditionM m b) -> PostconditionM m b)
-> (forall a b.
    PostconditionM m a -> PostconditionM m b -> PostconditionM m b)
-> (forall a. a -> PostconditionM m a)
-> Monad (PostconditionM m)
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
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
PostconditionM m a
-> (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 -> PostconditionM m b -> PostconditionM m b
>> :: forall a b.
PostconditionM m a -> PostconditionM m b -> PostconditionM m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> PostconditionM m a
return :: forall a. a -> PostconditionM m a
Monad)

instance MonadTrans PostconditionM where
  lift :: forall (m :: * -> *) a. Monad m => m a -> PostconditionM m a
lift = WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM (WriterT (Endo Property, Endo Property) m a -> PostconditionM m a)
-> (m a -> WriterT (Endo Property, Endo Property) m a)
-> m a
-> PostconditionM m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> WriterT (Endo Property, Endo Property) m a
forall (m :: * -> *) a.
Monad m =>
m a -> WriterT (Endo Property, Endo Property) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
evaluatePostCondition :: forall (m :: * -> *).
Monad m =>
PostconditionM m Bool -> PropertyM m ()
evaluatePostCondition PostconditionM m Bool
post = do
  (Bool
b, (Endo Property -> Property
mon, Endo Property -> Property
onFail)) <- m (Bool, (Endo Property, Endo Property))
-> PropertyM m (Bool, (Endo Property, Endo Property))
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m (Bool, (Endo Property, Endo Property))
 -> PropertyM m (Bool, (Endo Property, Endo Property)))
-> (PostconditionM m Bool
    -> m (Bool, (Endo Property, Endo Property)))
-> PostconditionM m Bool
-> PropertyM m (Bool, (Endo Property, Endo Property))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT (Endo Property, Endo Property) m Bool
-> m (Bool, (Endo Property, Endo Property))
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT (Endo Property, Endo Property) m Bool
 -> m (Bool, (Endo Property, Endo Property)))
-> (PostconditionM m Bool
    -> WriterT (Endo Property, Endo Property) m Bool)
-> PostconditionM m Bool
-> m (Bool, (Endo Property, Endo Property))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PostconditionM m Bool
-> WriterT (Endo Property, Endo Property) m Bool
forall (m :: * -> *) a.
PostconditionM m a -> WriterT (Endo Property, Endo Property) m a
runPost (PostconditionM m Bool
 -> PropertyM m (Bool, (Endo Property, Endo Property)))
-> PostconditionM m Bool
-> PropertyM m (Bool, (Endo Property, Endo Property))
forall a b. (a -> b) -> a -> b
$ PostconditionM m Bool
post
  (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor Property -> Property
mon
  Bool -> PropertyM m () -> PropertyM m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (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 Property -> Property
onFail
  Bool -> PropertyM m ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
b

-- | 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 = WriterT (Endo Property, Endo Property) m () -> PostconditionM m ()
forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM (WriterT (Endo Property, Endo Property) m ()
 -> PostconditionM m ())
-> WriterT (Endo Property, Endo Property) m ()
-> PostconditionM m ()
forall a b. (a -> b) -> a -> b
$ (Endo Property, Endo Property)
-> WriterT (Endo Property, Endo Property) m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ((Property -> Property) -> Endo Property
forall a. (a -> a) -> Endo a
Endo Property -> Property
m, Endo Property
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 = WriterT (Endo Property, Endo Property) m () -> PostconditionM m ()
forall (m :: * -> *) a.
WriterT (Endo Property, Endo Property) m a -> PostconditionM m a
PostconditionM (WriterT (Endo Property, Endo Property) m ()
 -> PostconditionM m ())
-> WriterT (Endo Property, Endo Property) m ()
-> PostconditionM m ()
forall a b. (a -> b) -> a -> b
$ (Endo Property, Endo Property)
-> WriterT (Endo Property, Endo Property) m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Endo Property
forall a. Monoid a => a
mempty, (Property -> Property) -> Endo Property
forall a. (a -> a) -> Endo a
Endo ((Property -> Property) -> Endo Property)
-> (Property -> Property) -> Endo Property
forall a b. (a -> b) -> a -> b
$ String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
c)

-- | The result required of `perform` depending on the `Error` type.
-- If there are no errors, `Error state = Void`, and
-- so we don't need to specify if the action failed or not.
type family PerformResult state (m :: Type -> Type) a where
  PerformResult state m a = EitherIsh (Error state m) a

type family EitherIsh e a where
  EitherIsh Void a = a
  EitherIsh e a = Either e a

class IsPerformResult e a where
  performResultToEither :: EitherIsh e a -> Either e a

instance {-# OVERLAPPING #-} IsPerformResult Void a where
  performResultToEither :: EitherIsh Void a -> Either Void a
performResultToEither = a -> Either Void a
EitherIsh Void a -> Either Void a
forall a b. b -> Either a b
Right

instance {-# OVERLAPPABLE #-} (EitherIsh e a ~ Either e a) => IsPerformResult e a where
  performResultToEither :: EitherIsh e a -> Either e a
performResultToEither = Either e a -> Either e a
EitherIsh e a -> Either e a
forall a. a -> a
id

class (forall a. Show (Action state a), Monad m) => RunModel state m where
  -- | The type of errors that actions can throw. If this is defined as anything
  -- other than `Void` `perform` is required to return `Either (Error state) a`
  -- instead of `a`.
  type Error state m

  type Error state m = Void

  -- | Perform an `Action` in some `state` in the `Monad` `m`.  This
  -- is the function that's used to exercise the actual stateful
  -- implementation, usually through various side-effects as permitted
  -- 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 :: Typeable a => state -> Action state a -> LookUp -> m (PerformResult state m a)

  -- | Postcondition on the `a` value produced at some step.
  -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
  -- to check the implementation produces expected values.
  postcondition :: (state, state) -> Action state a -> LookUp -> a -> PostconditionM m Bool
  postcondition (state, state)
_ Action state a
_ LookUp
_ a
_ = Bool -> PostconditionM m Bool
forall a. a -> PostconditionM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

  -- | Postcondition on the result of running a _negative_ `Action`.
  -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
  -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't
  -- been updated during the execution of the negative action.
  postconditionOnFailure :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> PostconditionM m Bool
  postconditionOnFailure (state, state)
_ Action state a
_ LookUp
_ Either (Error state m) a
_ = Bool -> PostconditionM m Bool
forall a. a -> PostconditionM 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 :: (state, state) -> Action state a -> LookUp -> Either (Error state m) a -> Property -> Property
  monitoring (state, state)
_ Action state a
_ LookUp
_ Either (Error state m) a
_ Property
prop = Property
prop

  -- | Allows the user to attach additional information to the `Property` if a positive action fails.
  monitoringFailure :: state -> Action state a -> LookUp -> Error state m -> Property -> Property
  monitoringFailure state
_ Action state a
_ LookUp
_ Error state m
_ Property
prop = Property
prop

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

type Env = [EnvEntry]

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

infix 5 :==

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

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

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

lookUpVar :: Typeable a => Env -> Var a -> a
lookUpVar :: forall a. Typeable a => Env -> Var a -> a
lookUpVar Env
env Var a
v = case Env -> Var a -> Maybe a
forall a. Typeable a => Env -> Var a -> Maybe a
lookUpVarMaybe Env
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 at type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep -> String
forall a. Show a => a -> String
show (Var a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Var a
v) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!"
  Just a
a -> a
a

data WithUsedVars a = WithUsedVars VarContext a

data Polarity
  = PosPolarity
  | NegPolarity
  deriving (Eq Polarity
Eq Polarity =>
(Polarity -> Polarity -> Ordering)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Polarity)
-> (Polarity -> Polarity -> Polarity)
-> Ord Polarity
Polarity -> Polarity -> Bool
Polarity -> Polarity -> Ordering
Polarity -> Polarity -> Polarity
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
$ccompare :: Polarity -> Polarity -> Ordering
compare :: Polarity -> Polarity -> Ordering
$c< :: Polarity -> Polarity -> Bool
< :: Polarity -> Polarity -> Bool
$c<= :: Polarity -> Polarity -> Bool
<= :: Polarity -> Polarity -> Bool
$c> :: Polarity -> Polarity -> Bool
> :: Polarity -> Polarity -> Bool
$c>= :: Polarity -> Polarity -> Bool
>= :: Polarity -> Polarity -> Bool
$cmax :: Polarity -> Polarity -> Polarity
max :: Polarity -> Polarity -> Polarity
$cmin :: Polarity -> Polarity -> Polarity
min :: Polarity -> Polarity -> Polarity
Ord, Polarity -> Polarity -> Bool
(Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool) -> Eq Polarity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
/= :: Polarity -> Polarity -> Bool
Eq)

instance Show Polarity where
  show :: Polarity -> String
show Polarity
PosPolarity = String
"+"
  show Polarity
NegPolarity = String
"-"

data ActionWithPolarity state a = Eq (Action state a) =>
  ActionWithPolarity
  { forall state a. ActionWithPolarity state a -> Action state a
polarAction :: Action state a
  , forall state a. ActionWithPolarity state a -> Polarity
polarity :: Polarity
  }

instance HasVariables (Action state a) => HasVariables (ActionWithPolarity state a) where
  getAllVariables :: ActionWithPolarity state a -> Set (Any Var)
getAllVariables = Action state a -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables (Action state a -> Set (Any Var))
-> (ActionWithPolarity state a -> Action state a)
-> ActionWithPolarity state a
-> Set (Any Var)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction

deriving instance Eq (Action state a) => Eq (ActionWithPolarity state a)

data Step state where
  (:=)
    :: (Typeable a, Eq (Action state a), Show (Action state a))
    => Var a
    -> ActionWithPolarity 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 := ActionWithPolarity state a
act) = Any Var -> Set (Any Var) -> Set (Any Var)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Var a -> Any Var
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Var a
var) (Set (Any Var) -> Set (Any Var)) -> Set (Any Var) -> Set (Any Var)
forall a b. (a -> b) -> a -> b
$ Action state a -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables (ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)

funName :: Polarity -> String
funName :: Polarity -> String
funName Polarity
PosPolarity = String
"action"
funName Polarity
_ = String
"failingAction"

instance Show (Step state) where
  show :: Step state -> String
show (Var a
var := ActionWithPolarity state a
act) = Var a -> String
forall a. Show a => a -> String
show Var a
var String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Polarity -> String
funName (ActionWithPolarity state a -> Polarity
forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" $ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Action state a -> String
forall a. Show a => a -> String
show (ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)

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

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

pattern Actions :: [Step state] -> Actions state
pattern $mActions :: forall {r} {state}.
Actions state -> ([Step state] -> r) -> ((# #) -> r) -> r
$bActions :: forall state. [Step state] -> Actions state
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 StateModel state => Show (Actions state) where
  show :: Actions state -> String
show (Actions [Step state]
as) =
    let as' :: [WithUsedVars (Step state)]
as' = VarContext -> Step state -> WithUsedVars (Step state)
forall a. VarContext -> a -> WithUsedVars a
WithUsedVars (Actions state -> VarContext
forall state. StateModel state => Actions state -> VarContext
usedVariables ([Step state] -> Actions state
forall state. [Step state] -> Actions state
Actions [Step state]
as)) (Step state -> WithUsedVars (Step state))
-> [Step state] -> [WithUsedVars (Step state)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Step state]
as
     in String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> ShowS) -> [String] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> ShowS
forall a. [a] -> [a] -> [a]
(++) (String
"do " String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
forall a. a -> [a]
repeat String
"   ") ((WithUsedVars (Step state) -> String)
-> [WithUsedVars (Step state)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map WithUsedVars (Step state) -> String
forall a. Show a => a -> String
show [WithUsedVars (Step state)]
as' [String] -> [String] -> [String]
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 Annotated state
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 [] = state -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
aState)
    go Annotated state
aState ((Var a
var := ActionWithPolarity state a
act) : [Step state]
steps) =
      Action state a -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables (ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act)
        VarContext -> VarContext -> VarContext
forall a. Semigroup a => a -> a -> a
<> state -> VarContext
forall a. HasVariables a => a -> VarContext
allVariables (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
aState)
        VarContext -> VarContext -> VarContext
forall a. Semigroup a => a -> a -> a
<> Annotated state -> [Step state] -> VarContext
go (Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
aState ActionWithPolarity state a
act Var a
var) [Step state]
steps

instance forall state. StateModel state => Arbitrary (Actions state) where
  arbitrary :: Gen (Actions state)
arbitrary = Options state -> Gen (Actions state)
forall state.
StateModel state =>
Options state -> Gen (Actions state)
generateActionsWithOptions Options state
forall state. Options state
defaultOptions
  shrink :: Actions state -> [Actions state]
shrink = Options state -> Actions state -> [Actions state]
forall state.
StateModel state =>
Options state -> Actions state -> [Actions state]
shrinkActionsWithOptions Options state
forall state. Options state
defaultOptions

data QCDProperty state = QCDProperty
  { forall state. QCDProperty state -> Actions state -> Property
runQCDProperty :: Actions state -> Property
  , forall state. QCDProperty state -> Options state
qcdPropertyOptions :: Options state
  }

instance StateModel state => Testable (QCDProperty state) where
  property :: QCDProperty state -> Property
property QCDProperty{Options state
Actions state -> Property
runQCDProperty :: forall state. QCDProperty state -> Actions state -> Property
qcdPropertyOptions :: forall state. QCDProperty state -> Options state
runQCDProperty :: Actions state -> Property
qcdPropertyOptions :: Options state
..} =
    Gen (Actions state)
-> (Actions state -> [Actions state])
-> (Actions state -> Property)
-> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrink
      (Options state -> Gen (Actions state)
forall state.
StateModel state =>
Options state -> Gen (Actions state)
generateActionsWithOptions Options state
qcdPropertyOptions)
      (Options state -> Actions state -> [Actions state]
forall state.
StateModel state =>
Options state -> Actions state -> [Actions state]
shrinkActionsWithOptions Options state
qcdPropertyOptions)
      Actions state -> Property
runQCDProperty

class QCDProp state p | p -> state where
  qcdProperty :: p -> QCDProperty state

instance QCDProp state (QCDProperty state) where
  qcdProperty :: QCDProperty state -> QCDProperty state
qcdProperty = QCDProperty state -> QCDProperty state
forall a. a -> a
id

instance Testable p => QCDProp state (Actions state -> p) where
  qcdProperty :: (Actions state -> p) -> QCDProperty state
qcdProperty Actions state -> p
p = (Actions state -> Property) -> Options state -> QCDProperty state
forall state.
(Actions state -> Property) -> Options state -> QCDProperty state
QCDProperty (p -> Property
forall prop. Testable prop => prop -> Property
property (p -> Property)
-> (Actions state -> p) -> Actions state -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Actions state -> p
p) Options state
forall state. Options state
defaultOptions

modifyOptions :: QCDProperty state -> (Options state -> Options state) -> QCDProperty state
modifyOptions :: forall state.
QCDProperty state
-> (Options state -> Options state) -> QCDProperty state
modifyOptions QCDProperty state
p Options state -> Options state
f =
  let opts :: Options state
opts = QCDProperty state -> Options state
forall state. QCDProperty state -> Options state
qcdPropertyOptions QCDProperty state
p
   in QCDProperty state
p{qcdPropertyOptions = f opts}

moreActions :: QCDProp state p => Rational -> p -> QCDProperty state
moreActions :: forall state p.
QCDProp state p =>
Rational -> p -> QCDProperty state
moreActions Rational
r p
p =
  QCDProperty state
-> (Options state -> Options state) -> QCDProperty state
forall state.
QCDProperty state
-> (Options state -> Options state) -> QCDProperty state
modifyOptions (p -> QCDProperty state
forall state p. QCDProp state p => p -> QCDProperty state
qcdProperty p
p) ((Options state -> Options state) -> QCDProperty state)
-> (Options state -> Options state) -> QCDProperty state
forall a b. (a -> b) -> a -> b
$ \Options state
opts -> Options state
opts{actionLengthMultiplier = actionLengthMultiplier opts * r}

-- NOTE: indexed on state for forwards compatibility, e.g. when we
-- want to give an explicit initial state
data Options state = Options {forall state. Options state -> Rational
actionLengthMultiplier :: Rational}

defaultOptions :: Options state
defaultOptions :: forall state. Options state
defaultOptions = Options{actionLengthMultiplier :: Rational
actionLengthMultiplier = Rational
1}

-- | Generate arbitrary actions with the `GenActionsOptions`. More flexible than using the type-based
-- modifiers.
generateActionsWithOptions :: forall state. StateModel state => Options state -> Gen (Actions state)
generateActionsWithOptions :: forall state.
StateModel state =>
Options state -> Gen (Actions state)
generateActionsWithOptions Options{Rational
actionLengthMultiplier :: forall state. Options state -> Rational
actionLengthMultiplier :: Rational
..} = do
  ([Step state]
as, [String]
rejected) <- [Step state]
-> [String]
-> Annotated state
-> Int
-> Gen ([Step state], [String])
arbActions [] [] Annotated state
forall state. StateModel state => Annotated state
initialAnnotatedState Int
1
  Actions state -> Gen (Actions state)
forall a. a -> Gen a
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 :: [Step state] -> [String] -> Annotated state -> Int -> Gen ([Step state], [String])
    arbActions :: [Step state]
-> [String]
-> Annotated state
-> Int
-> Gen ([Step state], [String])
arbActions [Step state]
steps [String]
rejected Annotated 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 -> do
      let w :: Int
w = Rational -> Int
forall b. Integral b => Rational -> b
forall a b. (RealFrac a, Integral b) => a -> b
round (Rational
actionLengthMultiplier Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Int -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral 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
      Bool
continue <- [(Int, Gen Bool)] -> Gen Bool
forall a. [(Int, Gen a)] -> Gen a
frequency [(Int
1, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False), (Int
w, Bool -> Gen Bool
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)]
      if Bool
continue
        then do
          (Maybe (Any (ActionWithPolarity state))
mact, [String]
rej) <- Gen (Maybe (Any (ActionWithPolarity state)), [String])
satisfyPrecondition
          case Maybe (Any (ActionWithPolarity state))
mact of
            Just (Some act :: ActionWithPolarity state a
act@ActionWithPolarity{}) -> do
              let var :: Var a
var = Int -> Var a
forall a. Int -> Var a
mkVar Int
step
              [Step state]
-> [String]
-> Annotated state
-> Int
-> Gen ([Step state], [String])
arbActions
                ((Var a
var Var a -> ActionWithPolarity state a -> Step state
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act) Step state -> [Step state] -> [Step state]
forall a. a -> [a] -> [a]
: [Step state]
steps)
                ([String]
rej [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
rejected)
                (Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
act Var a
var)
                (Int
step Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            Maybe (Any (ActionWithPolarity state))
Nothing ->
              ([Step state], [String]) -> Gen ([Step state], [String])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Step state] -> [Step state]
forall a. [a] -> [a]
reverse [Step state]
steps, [String]
rejected)
        else ([Step state], [String]) -> Gen ([Step state], [String])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Step state] -> [Step state]
forall a. [a] -> [a]
reverse [Step state]
steps, [String]
rejected)
      where
        satisfyPrecondition :: Gen (Maybe (Any (ActionWithPolarity state)), [String])
satisfyPrecondition = (Int -> Gen (Maybe (Any (ActionWithPolarity state)), [String]))
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (Maybe (Any (ActionWithPolarity state)), [String]))
 -> Gen (Maybe (Any (ActionWithPolarity state)), [String]))
-> (Int -> Gen (Maybe (Any (ActionWithPolarity state)), [String]))
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
forall a b. (a -> b) -> a -> b
$ \Int
n -> Int
-> Int
-> [String]
-> Gen (Maybe (Any (ActionWithPolarity 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 (ActionWithPolarity 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 (ActionWithPolarity state)), [String])
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Any (ActionWithPolarity state))
forall a. Maybe a
Nothing, [String]
rej)
          | Bool
otherwise = do
              Any (ActionWithPolarity state)
a <- Int
-> Gen (Any (ActionWithPolarity state))
-> Gen (Any (ActionWithPolarity state))
forall a. Int -> Gen a -> Gen a
resize Int
m (Gen (Any (ActionWithPolarity state))
 -> Gen (Any (ActionWithPolarity state)))
-> Gen (Any (ActionWithPolarity state))
-> Gen (Any (ActionWithPolarity state))
forall a b. (a -> b) -> a -> b
$ Annotated state -> Gen (Any (ActionWithPolarity state))
forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated state
s
              case Any (ActionWithPolarity state)
a of
                Some ActionWithPolarity state a
act ->
                  if Annotated state -> ActionWithPolarity state a -> Bool
forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated state
s ActionWithPolarity state a
act
                    then (Maybe (Any (ActionWithPolarity state)), [String])
-> Gen (Maybe (Any (ActionWithPolarity state)), [String])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Any (ActionWithPolarity state)
-> Maybe (Any (ActionWithPolarity state))
forall a. a -> Maybe a
Just (ActionWithPolarity state a -> Any (ActionWithPolarity state)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some ActionWithPolarity state a
act), [String]
rej)
                    else Int
-> Int
-> [String]
-> Gen (Maybe (Any (ActionWithPolarity 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
forall a. Action state a -> String
actionName (ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
rej)

shrinkActionsWithOptions :: forall state. StateModel state => Options state -> Actions state -> [Actions state]
shrinkActionsWithOptions :: forall state.
StateModel state =>
Options state -> Actions state -> [Actions state]
shrinkActionsWithOptions Options state
_ (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, Annotated state)] -> [Step state])
-> [[(Step state, Annotated 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, Annotated state)] -> [Step state])
-> [(Step state, Annotated state)]
-> [Step state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Step state, Annotated state) -> Step state)
-> [(Step state, Annotated state)] -> [Step state]
forall a b. (a -> b) -> [a] -> [b]
map (Step state, Annotated state) -> Step state
forall a b. (a, b) -> a
fst) ([[(Step state, Annotated state)]] -> [[Step state]])
-> ([Step state] -> [[(Step state, Annotated state)]])
-> [Step state]
-> [[Step state]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Step state, Annotated state)]
 -> [[(Step state, Annotated state)]])
-> [[(Step state, Annotated state)]]
-> [[(Step state, Annotated state)]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
customActionsShrinker ([[(Step state, Annotated state)]]
 -> [[(Step state, Annotated state)]])
-> ([Step state] -> [[(Step state, Annotated state)]])
-> [Step state]
-> [[(Step state, Annotated state)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Step state, Annotated state) -> [(Step state, Annotated state)])
-> [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker ([(Step state, Annotated state)]
 -> [[(Step state, Annotated state)]])
-> ([Step state] -> [(Step state, Annotated state)])
-> [Step state]
-> [[(Step state, Annotated state)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Step state] -> [(Step state, Annotated state)]
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 :: (Step state, Annotated state) -> [(Step state, Annotated state)]
shrinker (Var a
v := ActionWithPolarity state a
act, Annotated state
s) = [(Var a -> Var a
forall a b. Var a -> Var b
unsafeCoerceVar Var a
v Var a -> ActionWithPolarity state a -> Step state
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act', Annotated state
s) | Some act' :: ActionWithPolarity state a
act'@ActionWithPolarity{} <- Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
forall state a.
(Typeable a, StateModel state) =>
Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
computeShrinkAction Annotated state
s ActionWithPolarity state a
act]

    customActionsShrinker :: [(Step state, Annotated state)] -> [[(Step state, Annotated state)]]
    customActionsShrinker :: [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
customActionsShrinker [(Step state, Annotated state)]
acts =
      let usedVars :: Set (Any Var)
usedVars = [Set (Any Var)] -> Set (Any Var)
forall a. Monoid a => [a] -> a
mconcat [ActionWithPolarity state a -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables ActionWithPolarity state a
a Set (Any Var) -> Set (Any Var) -> Set (Any Var)
forall a. Semigroup a => a -> a -> a
<> state -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) | (Var a
_ := ActionWithPolarity state a
a, Annotated state
s) <- [(Step state, Annotated state)]
acts]
          binding :: (Step state, Annotated state) -> Bool
binding (Var a
v := ActionWithPolarity state a
_, Annotated state
_) = Var a -> Any Var
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some Var a
v Any Var -> Set (Any Var) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Any Var)
usedVars
          -- Remove at most one non-binding action
          go :: [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [] = [[]]
          go ((Step state, Annotated state)
p : [(Step state, Annotated state)]
ps)
            | (Step state, Annotated state) -> Bool
binding (Step state, Annotated state)
p = ([(Step state, Annotated state)]
 -> [(Step state, Annotated state)])
-> [[(Step state, Annotated state)]]
-> [[(Step state, Annotated state)]]
forall a b. (a -> b) -> [a] -> [b]
map ((Step state, Annotated state)
p (Step state, Annotated state)
-> [(Step state, Annotated state)]
-> [(Step state, Annotated state)]
forall a. a -> [a] -> [a]
:) ([(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [(Step state, Annotated state)]
ps)
            | Bool
otherwise = [(Step state, Annotated state)]
ps [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
-> [[(Step state, Annotated state)]]
forall a. a -> [a] -> [a]
: ([(Step state, Annotated state)]
 -> [(Step state, Annotated state)])
-> [[(Step state, Annotated state)]]
-> [[(Step state, Annotated state)]]
forall a b. (a -> b) -> [a] -> [b]
map ((Step state, Annotated state)
p (Step state, Annotated state)
-> [(Step state, Annotated state)]
-> [(Step state, Annotated state)]
forall a. a -> [a] -> [a]
:) ([(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [(Step state, Annotated state)]
ps)
       in [(Step state, Annotated state)]
-> [[(Step state, Annotated state)]]
go [(Step state, Annotated state)]
acts

-- 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) = VarContext -> String
forall a. Show a => a -> String
show VarContext
ctx String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" |- " String -> ShowS
forall a. [a] -> [a] -> [a]
++ state -> String
forall a. Show a => a -> String
show state
s

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

actionWithPolarity :: (StateModel state, Eq (Action state a)) => Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity :: forall state a.
(StateModel state, Eq (Action state a)) =>
Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity Annotated state
s Action state a
a =
  let p :: Polarity
p
        | state -> Action state a -> Bool
forall a. state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a = Polarity
PosPolarity
        | state -> Action state a -> Bool
forall a. state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
validFailingAction (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a = Polarity
NegPolarity
        | Bool
otherwise = Polarity
PosPolarity
   in Action state a -> Polarity -> ActionWithPolarity state a
forall state a.
Eq (Action state a) =>
Action state a -> Polarity -> ActionWithPolarity state a
ActionWithPolarity Action state a
a Polarity
p

computePrecondition :: StateModel state => Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition :: forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated state
s (ActionWithPolarity Action state a
a Polarity
p) =
  let polarPrecondition :: Bool
polarPrecondition
        | Polarity
p Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = state -> Action state a -> Bool
forall a. state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a
        | Bool
otherwise = state -> Action state a -> Bool
forall a. state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
validFailingAction (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a Bool -> Bool -> Bool
&& Bool -> Bool
not (state -> Action state a -> Bool
forall a. state -> Action state a -> Bool
forall state a. StateModel state => state -> Action state a -> Bool
precondition (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a)
   in (Any Var -> Bool) -> Set (Any Var) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Some Var a
v) -> Var a
v Var a -> VarContext -> Bool
forall a. Typeable a => Var a -> VarContext -> Bool
`isWellTyped` Annotated state -> VarContext
forall state. Annotated state -> VarContext
vars Annotated state
s) (Action state a -> Set (Any Var)
forall a. HasVariables a => a -> Set (Any Var)
getAllVariables Action state a
a)
        Bool -> Bool -> Bool
&& Bool
polarPrecondition

computeNextState
  :: (StateModel state, Typeable a)
  => Annotated state
  -> ActionWithPolarity state a
  -> Var a
  -> Annotated state
computeNextState :: forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
a Var a
v
  | ActionWithPolarity state a -> Polarity
forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
a Polarity -> Polarity -> Bool
forall a. Eq a => a -> a -> Bool
== Polarity
PosPolarity = VarContext -> state -> Annotated state
forall state. VarContext -> state -> Annotated state
Metadata (VarContext -> Var a -> VarContext
forall a. Typeable a => VarContext -> Var a -> VarContext
extendContext (Annotated state -> VarContext
forall state. Annotated state -> VarContext
vars Annotated state
s) Var a
v) (state -> Action state a -> Var a -> state
forall a. Typeable a => state -> Action state a -> Var a -> state
forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> Var a -> state
nextState (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) (ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
a) Var a
v)
  | Bool
otherwise = VarContext -> state -> Annotated state
forall state. VarContext -> state -> Annotated state
Metadata (Annotated state -> VarContext
forall state. Annotated state -> VarContext
vars Annotated state
s) (state -> Action state a -> state
forall a. Typeable a => state -> Action state a -> state
forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> state
failureNextState (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) (ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
a))

computeArbitraryAction
  :: StateModel state
  => Annotated state
  -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction :: forall state.
StateModel state =>
Annotated state -> Gen (Any (ActionWithPolarity state))
computeArbitraryAction Annotated state
s = do
  Some Action state a
a <- VarContext -> state -> Gen (Any (Action state))
forall state.
StateModel state =>
VarContext -> state -> Gen (Any (Action state))
arbitraryAction (Annotated state -> VarContext
forall state. Annotated state -> VarContext
vars Annotated state
s) (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s)
  Any (ActionWithPolarity state)
-> Gen (Any (ActionWithPolarity state))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (ActionWithPolarity state)
 -> Gen (Any (ActionWithPolarity state)))
-> Any (ActionWithPolarity state)
-> Gen (Any (ActionWithPolarity state))
forall a b. (a -> b) -> a -> b
$ ActionWithPolarity state a -> Any (ActionWithPolarity state)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (ActionWithPolarity state a -> Any (ActionWithPolarity state))
-> ActionWithPolarity state a -> Any (ActionWithPolarity state)
forall a b. (a -> b) -> a -> b
$ Annotated state -> Action state a -> ActionWithPolarity state a
forall state a.
(StateModel state, Eq (Action state a)) =>
Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity Annotated state
s Action state a
a

computeShrinkAction
  :: forall state a
   . (Typeable a, StateModel state)
  => Annotated state
  -> ActionWithPolarity state a
  -> [Any (ActionWithPolarity state)]
computeShrinkAction :: forall state a.
(Typeable a, StateModel state) =>
Annotated state
-> ActionWithPolarity state a -> [Any (ActionWithPolarity state)]
computeShrinkAction Annotated state
s (ActionWithPolarity Action state a
a Polarity
_) =
  [ActionWithPolarity state a -> Any (ActionWithPolarity state)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Annotated state -> Action state a -> ActionWithPolarity state a
forall state a.
(StateModel state, Eq (Action state a)) =>
Annotated state -> Action state a -> ActionWithPolarity state a
actionWithPolarity Annotated state
s Action state a
a') | Some Action state a
a' <- VarContext -> state -> Action state a -> [Any (Action state)]
forall a.
Typeable a =>
VarContext -> state -> Action state a -> [Any (Action state)]
forall state a.
(StateModel state, Typeable a) =>
VarContext -> state -> Action state a -> [Any (Action state)]
shrinkAction (Annotated state -> VarContext
forall state. Annotated state -> VarContext
vars Annotated state
s) (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
a]

prune :: forall state. StateModel state => [Step state] -> [Step state]
prune :: forall state. StateModel state => [Step state] -> [Step state]
prune = Annotated state -> [Step state] -> [Step state]
loop Annotated state
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 := ActionWithPolarity state a
act) : [Step state]
as)
      | forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition @state Annotated state
s ActionWithPolarity state a
act =
          (Var a
var Var a -> ActionWithPolarity state a -> Step state
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act) Step state -> [Step state] -> [Step state]
forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [Step state]
loop (Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity 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 :: forall state. StateModel state => [Step state] -> [(Step state, Annotated state)]
withStates :: forall state.
StateModel state =>
[Step state] -> [(Step state, Annotated state)]
withStates = Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop Annotated state
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 := ActionWithPolarity state a
act) : [Step state]
as) =
      (Var a
var Var a -> ActionWithPolarity state a -> Step state
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
:= ActionWithPolarity state a
act, Annotated state
s) (Step state, Annotated state)
-> [(Step state, Annotated state)]
-> [(Step state, Annotated state)]
forall a. a -> [a] -> [a]
: Annotated state -> [Step state] -> [(Step state, Annotated state)]
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState @state Annotated state
s ActionWithPolarity state a
act Var a
var) [Step state]
as

stateAfter :: forall state. StateModel state => Actions state -> Annotated state
stateAfter :: forall state. StateModel state => Actions state -> Annotated state
stateAfter (Actions [Step state]
actions) = Annotated state -> [Step state] -> Annotated state
loop Annotated state
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 := ActionWithPolarity state a
act) : [Step state]
as) = Annotated state -> [Step state] -> Annotated state
loop (forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState @state Annotated state
s ActionWithPolarity state a
act Var a
var) [Step state]
as

runActions
  :: forall state m e
   . ( StateModel state
     , RunModel state m
     , e ~ Error state m
     , forall a. IsPerformResult e a
     )
  => Actions state
  -> PropertyM m (Annotated state, Env)
runActions :: forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env)
runActions (Actions_ [String]
rejected (Smart Int
_ [Step state]
actions)) = do
  let bucket :: Int -> String
bucket = \Int
n -> let (Int
a, Int
b) = Int -> (Int, Int)
forall {t}. Integral t => t -> (t, t)
go Int
n in Int -> String
forall a. Show a => a -> String
show Int
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
b
        where
          go :: t -> (t, t)
go t
n
            | t
n t -> t -> Bool
forall a. Ord a => a -> a -> Bool
< t
100 = (t
d t -> t -> t
forall a. Num a => a -> a -> a
* t
10, t
d t -> t -> t
forall a. Num a => a -> a -> a
* t
10 t -> t -> t
forall a. Num a => a -> a -> a
+ t
9)
            | Bool
otherwise = let (t
a, t
b) = t -> (t, t)
go t
d in (t
a t -> t -> t
forall a. Num a => a -> a -> a
* t
10, t
b t -> t -> t
forall a. Num a => a -> a -> a
* t
10 t -> t -> t
forall a. Num a => a -> a -> a
+ t
9)
            where
              d :: t
d = t -> t -> t
forall a. Integral a => a -> a -> a
div t
n t
10
  (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((Property -> Property) -> PropertyM m ())
-> (Property -> Property) -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"# of actions" [ShowS
forall a. Show a => a -> String
show ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> String
bucket (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [Step state] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step state]
actions]
  (Annotated state
finalState, Env
env, [String]
names, [Polarity]
polars) <- Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
runSteps Annotated state
forall state. StateModel state => Annotated state
initialAnnotatedState [] [Step state]
actions
  (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((Property -> Property) -> PropertyM m ())
-> (Property -> Property) -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions" [String]
names
  (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((Property -> Property) -> PropertyM m ())
-> (Property -> Property) -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Action polarity" ([String] -> Property -> Property)
-> [String] -> Property -> Property
forall a b. (a -> b) -> a -> b
$ (Polarity -> String) -> [Polarity] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Polarity -> String
forall a. Show a => a -> String
show [Polarity]
polars
  Bool -> PropertyM m () -> PropertyM m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall a. [a] -> 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 ((Property -> Property) -> PropertyM m ())
-> (Property -> Property) -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$
      String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Actions rejected by precondition" [String]
rejected
  (Annotated state, Env) -> PropertyM m (Annotated state, Env)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Annotated state
finalState, Env
env)

-- | Core function to execute a sequence of `Step` given some initial `Env`ironment and `Annotated`
-- state. Return the list of action names and polarities to work around
-- https://github.com/nick8325/quickcheck/issues/416 causing repeated calls to tabulate being slow.
runSteps
  :: forall state m e
   . ( StateModel state
     , RunModel state m
     , e ~ Error state m
     , forall a. IsPerformResult e a
     )
  => Annotated state
  -> Env
  -> [Step state]
  -> PropertyM m (Annotated state, Env, [String], [Polarity])
runSteps :: forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
runSteps Annotated state
s Env
env [] = (Annotated state, Env, [String], [Polarity])
-> PropertyM m (Annotated state, Env, [String], [Polarity])
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Annotated state
s, Env -> Env
forall a. [a] -> [a]
reverse Env
env, [], [])
runSteps Annotated state
s Env
env ((Var a
v := ActionWithPolarity 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
$ Annotated state -> ActionWithPolarity state a -> Bool
forall state a.
StateModel state =>
Annotated state -> ActionWithPolarity state a -> Bool
computePrecondition Annotated state
s ActionWithPolarity state a
act
  Either e a
ret <- m (Either e a) -> PropertyM m (Either e a)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m (Either e a) -> PropertyM m (Either e a))
-> m (Either e a) -> PropertyM m (Either e a)
forall a b. (a -> b) -> a -> b
$ EitherIsh e a -> Either e a
forall e a. IsPerformResult e a => EitherIsh e a -> Either e a
performResultToEither (EitherIsh e a -> Either e a)
-> m (EitherIsh e a) -> m (Either e a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> state -> Action state a -> LookUp -> m (PerformResult state m a)
forall a.
Typeable a =>
state -> Action state a -> LookUp -> m (PerformResult state m a)
forall state (m :: * -> *) a.
(RunModel state m, Typeable a) =>
state -> Action state a -> LookUp -> m (PerformResult state m a)
perform (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s) Action state a
action (Env -> Var a -> a
forall a. Typeable a => Env -> Var a -> a
lookUpVar Env
env)
  let name :: String
name = Polarity -> String
forall a. Show a => a -> String
show Polarity
polar String -> ShowS
forall a. [a] -> [a] -> [a]
++ Action state a -> String
forall state a. StateModel state => Action state a -> String
forall a. Action state a -> String
actionName Action state a
action
  case (Polarity
polar, Either e a
ret) of
    (Polarity
PosPolarity, Left e
err) ->
      e -> PropertyM m (Annotated state, Env, [String], [Polarity])
positiveActionFailed e
err
    (Polarity
PosPolarity, Right a
val) -> do
      (Annotated state
s', Env
env') <- Either e a -> a -> PropertyM m (Annotated state, Env)
positiveActionSucceeded Either e a
ret a
val
      (Annotated state
s'', Env
env'', [String]
names, [Polarity]
polars) <- Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
runSteps Annotated state
s' Env
env' [Step state]
as
      (Annotated state, Env, [String], [Polarity])
-> PropertyM m (Annotated state, Env, [String], [Polarity])
forall a. a -> PropertyM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Annotated state
s'', Env
env'', String
name String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
names, Polarity
polar Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
: [Polarity]
polars)
    (Polarity
NegPolarity, Either e a
_) -> do
      (Annotated state
s', Env
env') <- Either e a -> PropertyM m (Annotated state, Env)
negativeActionResult Either e a
ret
      (Annotated state
s'', Env
env'', [String]
names, [Polarity]
polars) <- Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Annotated state
-> Env
-> [Step state]
-> PropertyM m (Annotated state, Env, [String], [Polarity])
runSteps Annotated state
s' Env
env' [Step state]
as
      (Annotated state, Env, [String], [Polarity])
-> PropertyM m (Annotated state, Env, [String], [Polarity])
forall a. a -> PropertyM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Annotated state
s'', Env
env'', String
name String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
names, Polarity
polar Polarity -> [Polarity] -> [Polarity]
forall a. a -> [a] -> [a]
: [Polarity]
polars)
  where
    polar :: Polarity
polar = ActionWithPolarity state a -> Polarity
forall state a. ActionWithPolarity state a -> Polarity
polarity ActionWithPolarity state a
act

    action :: Action state a
action = ActionWithPolarity state a -> Action state a
forall state a. ActionWithPolarity state a -> Action state a
polarAction ActionWithPolarity state a
act

    positiveActionFailed :: e -> PropertyM m (Annotated state, Env, [String], [Polarity])
positiveActionFailed e
err = do
      (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((Property -> Property) -> PropertyM m ())
-> (Property -> Property) -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$
        forall state (m :: * -> *) a.
RunModel state m =>
state
-> Action state a
-> LookUp
-> Error state m
-> Property
-> Property
monitoringFailure @state @m
          (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s)
          Action state a
action
          (Env -> Var a -> a
forall a. Typeable a => Env -> Var a -> a
lookUpVar Env
env)
          e
Error state m
err
      Bool -> PropertyM m (Annotated state, Env, [String], [Polarity])
forall prop (m :: * -> *) a.
(Testable prop, Monad m) =>
prop -> PropertyM m a
stop Bool
False

    positiveActionSucceeded :: Either e a -> a -> PropertyM m (Annotated state, Env)
positiveActionSucceeded Either e a
ret a
val = do
      (Annotated state
s', Env
env', (state, state)
stateTransition) <- Either e a -> PropertyM m (Annotated state, Env, (state, state))
computeNewState Either e a
ret
      PostconditionM m Bool -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
PostconditionM m Bool -> PropertyM m ()
evaluatePostCondition (PostconditionM m Bool -> PropertyM m ())
-> PostconditionM m Bool -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$
        (state, state)
-> Action state a -> LookUp -> a -> PostconditionM m Bool
forall a.
(state, state)
-> Action state a -> LookUp -> a -> PostconditionM m Bool
forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a -> LookUp -> a -> PostconditionM m Bool
postcondition
          (state, state)
stateTransition
          Action state a
action
          (Env -> Var a -> a
forall a. Typeable a => Env -> Var a -> a
lookUpVar Env
env)
          a
val
      (Annotated state, Env) -> PropertyM m (Annotated state, Env)
forall a. a -> PropertyM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Annotated state
s', Env
env')

    negativeActionResult :: Either e a -> PropertyM m (Annotated state, Env)
negativeActionResult Either e a
ret = do
      (Annotated state
s', Env
env', (state, state)
stateTransition) <- Either e a -> PropertyM m (Annotated state, Env, (state, state))
computeNewState Either e a
ret
      PostconditionM m Bool -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
PostconditionM m Bool -> PropertyM m ()
evaluatePostCondition (PostconditionM m Bool -> PropertyM m ())
-> PostconditionM m Bool -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$
        (state, state)
-> Action state a
-> LookUp
-> Either (Error state m) a
-> PostconditionM m Bool
forall a.
(state, state)
-> Action state a
-> LookUp
-> Either (Error state m) a
-> PostconditionM m Bool
forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp
-> Either (Error state m) a
-> PostconditionM m Bool
postconditionOnFailure
          (state, state)
stateTransition
          Action state a
action
          (Env -> Var a -> a
forall a. Typeable a => Env -> Var a -> a
lookUpVar Env
env)
          Either e a
Either (Error state m) a
ret
      (Annotated state, Env) -> PropertyM m (Annotated state, Env)
forall a. a -> PropertyM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Annotated state
s', Env
env')

    computeNewState :: Either e a -> PropertyM m (Annotated state, Env, (state, state))
computeNewState Either e a
ret = do
      let var :: Var a
var = Var a -> Var a
forall a b. Var a -> Var b
unsafeCoerceVar Var a
v
          s' :: Annotated state
s' = Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
forall state a.
(StateModel state, Typeable a) =>
Annotated state
-> ActionWithPolarity state a -> Var a -> Annotated state
computeNextState Annotated state
s ActionWithPolarity state a
act Var a
var
          env' :: Env
env'
            | Right a
val <- Either e a
ret = (Var a
var Var a -> a -> EnvEntry
forall a. Typeable a => Var a -> a -> EnvEntry
:== a
val) EnvEntry -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env
            | Bool
otherwise = Env
env
          stateTransition :: (state, state)
stateTransition = (Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s, Annotated state -> state
forall state. Annotated state -> state
underlyingState Annotated state
s')
      (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor ((Property -> Property) -> PropertyM m ())
-> (Property -> Property) -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ forall state (m :: * -> *) a.
RunModel state m =>
(state, state)
-> Action state a
-> LookUp
-> Either (Error state m) a
-> Property
-> Property
monitoring @state @m (state, state)
stateTransition Action state a
action (Env -> Var a -> a
forall a. Typeable a => Env -> Var a -> a
lookUpVar Env
env') Either e a
Either (Error state m) a
ret
      (Annotated state, Env, (state, state))
-> PropertyM m (Annotated state, Env, (state, state))
forall a. a -> PropertyM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Annotated state
s', Env
env', (state, state)
stateTransition)