{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
module Hedgehog.Internal.State (
  -- * Variables
    Var(..)
  , concrete
  , opaque

  , Concrete(..)
  , Symbolic(..)
  , Name(..)

  -- * Environment
  , Environment(..)
  , EnvironmentError(..)
  , emptyEnvironment
  , insertConcrete
  , reifyDynamic
  , reifyEnvironment
  , reify

  -- * Commands
  , Command(..)
  , Callback(..)
  , commandGenOK

  -- * Actions
  , Action(..)
  , Sequential(..)
  , Parallel(..)
  , takeVariables
  , variablesOK
  , dropInvalid
  , action
  , sequential
  , parallel
  , executeSequential
  , executeParallel
  ) where

import qualified Control.Concurrent.Async.Lifted as Async
import           Control.Monad (foldM, foldM_)
import           Control.Monad.Catch (MonadCatch)
import           Control.Monad.State.Class (MonadState, get, put, modify)
import           Control.Monad.Morph (MFunctor(..))
import           Control.Monad.Trans.Class (lift)
import           Control.Monad.Trans.Control (MonadBaseControl)
import           Control.Monad.Trans.State (State, runState, execState)
import           Control.Monad.Trans.State (StateT(..), evalStateT, runStateT)

import           Data.Dynamic (Dynamic, toDyn, fromDynamic, dynTypeRep)
import           Data.Foldable (traverse_)
import           Data.Functor.Classes (Eq1(..), Ord1(..), Show1(..))
import           Data.Functor.Classes (eq1, compare1, showsPrec1)
import           Data.Kind (Type)
import           Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Maybe as Maybe
import           Data.Typeable (Typeable, TypeRep, Proxy(..), typeRep)

import           Hedgehog.Internal.Barbie (FunctorB(..), TraversableB(..))
import           Hedgehog.Internal.Distributive (distributeT)
import           Hedgehog.Internal.Gen (MonadGen, GenT, GenBase)
import qualified Hedgehog.Internal.Gen as Gen
import           Hedgehog.Internal.Opaque (Opaque(..))
import           Hedgehog.Internal.Property (MonadTest(..), Test, evalEither, evalM, success, runTest, failWith, annotate)
import           Hedgehog.Internal.Range (Range)
import           Hedgehog.Internal.Show (showPretty)
import           Hedgehog.Internal.Source (HasCallStack, withFrozenCallStack)


-- | Symbolic variable names.
--
newtype Name =
  Name Int
  deriving (Name -> Name -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq, Eq Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
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
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
Ord, Integer -> Name
Name -> Name
Name -> Name -> Name
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Name
$cfromInteger :: Integer -> Name
signum :: Name -> Name
$csignum :: Name -> Name
abs :: Name -> Name
$cabs :: Name -> Name
negate :: Name -> Name
$cnegate :: Name -> Name
* :: Name -> Name -> Name
$c* :: Name -> Name -> Name
- :: Name -> Name -> Name
$c- :: Name -> Name -> Name
+ :: Name -> Name -> Name
$c+ :: Name -> Name -> Name
Num)

instance Show Name where
  showsPrec :: Int -> Name -> ShowS
showsPrec Int
p (Name Int
x) =
    forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Int
x

-- | Symbolic values: Because hedgehog generates actions in a separate phase
--   before execution, you will sometimes need to refer to the result of a
--   previous action in a generator without knowing the value of the result
--   (e.g., to get the ID of a previously-created user).
--
--   Symbolic variables provide a token to stand in for the actual variables at
--   generation time (and in 'Require'/'Update' callbacks). At execution time,
--   real values are available, so your execute actions work on 'Concrete'
--   variables.
--
--   See also: 'Command', 'Var'
--
data Symbolic a where
  Symbolic :: Typeable a => Name -> Symbolic a

deriving instance Eq (Symbolic a)
deriving instance Ord (Symbolic a)

instance Show (Symbolic a) where
  showsPrec :: Int -> Symbolic a -> ShowS
showsPrec Int
p (Symbolic Name
x) =
    forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Name
x

instance Show1 Symbolic where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Symbolic a -> ShowS
liftShowsPrec Int -> a -> ShowS
_ [a] -> ShowS
_ Int
p (Symbolic Name
x) =
    forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Name
x

instance Eq1 Symbolic where
  liftEq :: forall a b. (a -> b -> Bool) -> Symbolic a -> Symbolic b -> Bool
liftEq a -> b -> Bool
_ (Symbolic Name
x) (Symbolic Name
y) =
    Name
x forall a. Eq a => a -> a -> Bool
== Name
y

instance Ord1 Symbolic where
  liftCompare :: forall a b.
(a -> b -> Ordering) -> Symbolic a -> Symbolic b -> Ordering
liftCompare a -> b -> Ordering
_ (Symbolic Name
x) (Symbolic Name
y) =
    forall a. Ord a => a -> a -> Ordering
compare Name
x Name
y

-- | Concrete values: At test-execution time, 'Symbolic' values from generation
--   are replaced with 'Concrete' values from performing actions. This type
--   gives us something of the same kind as 'Symbolic' to pass as a type
--   argument to 'Var'.
--
newtype Concrete a where
  Concrete :: a -> Concrete a
  deriving (Concrete a -> Concrete a -> Bool
forall a. Eq a => Concrete a -> Concrete a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Concrete a -> Concrete a -> Bool
$c/= :: forall a. Eq a => Concrete a -> Concrete a -> Bool
== :: Concrete a -> Concrete a -> Bool
$c== :: forall a. Eq a => Concrete a -> Concrete a -> Bool
Eq, Concrete a -> Concrete a -> Bool
Concrete a -> Concrete a -> Ordering
Concrete a -> Concrete a -> Concrete 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}. Ord a => Eq (Concrete a)
forall a. Ord a => Concrete a -> Concrete a -> Bool
forall a. Ord a => Concrete a -> Concrete a -> Ordering
forall a. Ord a => Concrete a -> Concrete a -> Concrete a
min :: Concrete a -> Concrete a -> Concrete a
$cmin :: forall a. Ord a => Concrete a -> Concrete a -> Concrete a
max :: Concrete a -> Concrete a -> Concrete a
$cmax :: forall a. Ord a => Concrete a -> Concrete a -> Concrete a
>= :: Concrete a -> Concrete a -> Bool
$c>= :: forall a. Ord a => Concrete a -> Concrete a -> Bool
> :: Concrete a -> Concrete a -> Bool
$c> :: forall a. Ord a => Concrete a -> Concrete a -> Bool
<= :: Concrete a -> Concrete a -> Bool
$c<= :: forall a. Ord a => Concrete a -> Concrete a -> Bool
< :: Concrete a -> Concrete a -> Bool
$c< :: forall a. Ord a => Concrete a -> Concrete a -> Bool
compare :: Concrete a -> Concrete a -> Ordering
$ccompare :: forall a. Ord a => Concrete a -> Concrete a -> Ordering
Ord, forall a b. a -> Concrete b -> Concrete a
forall a b. (a -> b) -> Concrete a -> Concrete b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Concrete b -> Concrete a
$c<$ :: forall a b. a -> Concrete b -> Concrete a
fmap :: forall a b. (a -> b) -> Concrete a -> Concrete b
$cfmap :: forall a b. (a -> b) -> Concrete a -> Concrete b
Functor, forall a. Eq a => a -> Concrete a -> Bool
forall a. Num a => Concrete a -> a
forall a. Ord a => Concrete a -> a
forall m. Monoid m => Concrete m -> m
forall a. Concrete a -> Bool
forall a. Concrete a -> Int
forall a. Concrete a -> [a]
forall a. (a -> a -> a) -> Concrete a -> a
forall m a. Monoid m => (a -> m) -> Concrete a -> m
forall b a. (b -> a -> b) -> b -> Concrete a -> b
forall a b. (a -> b -> b) -> b -> Concrete a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Concrete a -> a
$cproduct :: forall a. Num a => Concrete a -> a
sum :: forall a. Num a => Concrete a -> a
$csum :: forall a. Num a => Concrete a -> a
minimum :: forall a. Ord a => Concrete a -> a
$cminimum :: forall a. Ord a => Concrete a -> a
maximum :: forall a. Ord a => Concrete a -> a
$cmaximum :: forall a. Ord a => Concrete a -> a
elem :: forall a. Eq a => a -> Concrete a -> Bool
$celem :: forall a. Eq a => a -> Concrete a -> Bool
length :: forall a. Concrete a -> Int
$clength :: forall a. Concrete a -> Int
null :: forall a. Concrete a -> Bool
$cnull :: forall a. Concrete a -> Bool
toList :: forall a. Concrete a -> [a]
$ctoList :: forall a. Concrete a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Concrete a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Concrete a -> a
foldr1 :: forall a. (a -> a -> a) -> Concrete a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Concrete a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Concrete a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Concrete a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Concrete a -> m
fold :: forall m. Monoid m => Concrete m -> m
$cfold :: forall m. Monoid m => Concrete m -> m
Foldable, Functor Concrete
Foldable Concrete
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
forall (f :: * -> *) a.
Applicative f =>
Concrete (f a) -> f (Concrete a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concrete a -> m (Concrete b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concrete a -> f (Concrete b)
sequence :: forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
$csequence :: forall (m :: * -> *) a. Monad m => Concrete (m a) -> m (Concrete a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concrete a -> m (Concrete b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Concrete a -> m (Concrete b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Concrete (f a) -> f (Concrete a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Concrete (f a) -> f (Concrete a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concrete a -> f (Concrete b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Concrete a -> f (Concrete b)
Traversable)

instance Show a => Show (Concrete a) where
  showsPrec :: Int -> Concrete a -> ShowS
showsPrec =
    forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1

instance Show1 Concrete where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Concrete a -> ShowS
liftShowsPrec Int -> a -> ShowS
sp [a] -> ShowS
_ Int
p (Concrete a
x) =
    Int -> a -> ShowS
sp Int
p a
x

instance Eq1 Concrete where
  liftEq :: forall a b. (a -> b -> Bool) -> Concrete a -> Concrete b -> Bool
liftEq a -> b -> Bool
eq (Concrete a
x) (Concrete b
y) =
    a -> b -> Bool
eq a
x b
y

instance Ord1 Concrete where
  liftCompare :: forall a b.
(a -> b -> Ordering) -> Concrete a -> Concrete b -> Ordering
liftCompare a -> b -> Ordering
comp (Concrete a
x) (Concrete b
y) =
    a -> b -> Ordering
comp a
x b
y

------------------------------------------------------------------------

-- | Variables are the potential or actual result of executing an action. They
--   are parameterised by either `Symbolic` or `Concrete` depending on the
--   phase of the test.
--
--   `Symbolic` variables are the potential results of actions. These are used
--   when generating the sequence of actions to execute. They allow actions
--   which occur later in the sequence to make use of the result of an action
--   which came earlier in the sequence.
--
--   `Concrete` variables are the actual results of actions. These are used
--   during test execution. They provide access to the actual runtime value of
--   a variable.
--
--   The state update `Callback` for a command needs to be polymorphic in the
--   type of variable because it is used in both the generation and the
--   execution phase.
--
--   The order of arguments makes 'Var' 'HTraverable', which is how 'Symbolic'
--   values are turned into 'Concrete' ones.
--
newtype Var a v =
  Var (v a)

-- | Take the value from a concrete variable.
--
concrete :: Var a Concrete -> a
concrete :: forall a. Var a Concrete -> a
concrete (Var (Concrete a
x)) =
  a
x

-- | Take the value from an opaque concrete variable.
--
opaque :: Var (Opaque a) Concrete -> a
opaque :: forall a. Var (Opaque a) Concrete -> a
opaque (Var (Concrete (Opaque a
x))) =
  a
x

instance (Eq a, Eq1 v) => Eq (Var a v) where
  == :: Var a v -> Var a v -> Bool
(==) (Var v a
x) (Var v a
y) =
    forall (f :: * -> *) a. (Eq1 f, Eq a) => f a -> f a -> Bool
eq1 v a
x v a
y

instance (Ord a, Ord1 v) => Ord (Var a v) where
  compare :: Var a v -> Var a v -> Ordering
compare (Var v a
x) (Var v a
y) =
    forall (f :: * -> *) a. (Ord1 f, Ord a) => f a -> f a -> Ordering
compare1 v a
x v a
y

instance (Show a, Show1 v) => Show (Var a v) where
  showsPrec :: Int -> Var a v -> ShowS
showsPrec Int
p (Var v a
x) =
    Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
>= Int
11) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"Var " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS
showsPrec1 Int
11 v a
x

instance FunctorB (Var a) where
  bmap :: forall (f :: * -> *) (g :: * -> *).
(forall a. f a -> g a) -> Var a f -> Var a g
bmap forall a. f a -> g a
f (Var f a
v) =
    forall a (v :: * -> *). v a -> Var a v
Var (forall a. f a -> g a
f f a
v)

instance TraversableB (Var a) where
  btraverse :: forall (e :: * -> *) (f :: * -> *) (g :: * -> *).
Applicative e =>
(forall a. f a -> e (g a)) -> Var a f -> e (Var a g)
btraverse forall a. f a -> e (g a)
f (Var f a
v) =
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a (v :: * -> *). v a -> Var a v
Var (forall a. f a -> e (g a)
f f a
v)

------------------------------------------------------------------------
-- Symbolic Environment

-- | A mapping of symbolic values to concrete values.
--
newtype Environment =
  Environment {
      Environment -> Map Name Dynamic
unEnvironment :: Map Name Dynamic
    } deriving (Int -> Environment -> ShowS
[Environment] -> ShowS
Environment -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Environment] -> ShowS
$cshowList :: [Environment] -> ShowS
show :: Environment -> String
$cshow :: Environment -> String
showsPrec :: Int -> Environment -> ShowS
$cshowsPrec :: Int -> Environment -> ShowS
Show)

-- | Environment errors.
--
data EnvironmentError =
    EnvironmentValueNotFound !Name
  | EnvironmentTypeError !TypeRep !TypeRep
    deriving (EnvironmentError -> EnvironmentError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EnvironmentError -> EnvironmentError -> Bool
$c/= :: EnvironmentError -> EnvironmentError -> Bool
== :: EnvironmentError -> EnvironmentError -> Bool
$c== :: EnvironmentError -> EnvironmentError -> Bool
Eq, Eq EnvironmentError
EnvironmentError -> EnvironmentError -> Bool
EnvironmentError -> EnvironmentError -> Ordering
EnvironmentError -> EnvironmentError -> EnvironmentError
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
min :: EnvironmentError -> EnvironmentError -> EnvironmentError
$cmin :: EnvironmentError -> EnvironmentError -> EnvironmentError
max :: EnvironmentError -> EnvironmentError -> EnvironmentError
$cmax :: EnvironmentError -> EnvironmentError -> EnvironmentError
>= :: EnvironmentError -> EnvironmentError -> Bool
$c>= :: EnvironmentError -> EnvironmentError -> Bool
> :: EnvironmentError -> EnvironmentError -> Bool
$c> :: EnvironmentError -> EnvironmentError -> Bool
<= :: EnvironmentError -> EnvironmentError -> Bool
$c<= :: EnvironmentError -> EnvironmentError -> Bool
< :: EnvironmentError -> EnvironmentError -> Bool
$c< :: EnvironmentError -> EnvironmentError -> Bool
compare :: EnvironmentError -> EnvironmentError -> Ordering
$ccompare :: EnvironmentError -> EnvironmentError -> Ordering
Ord, Int -> EnvironmentError -> ShowS
[EnvironmentError] -> ShowS
EnvironmentError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EnvironmentError] -> ShowS
$cshowList :: [EnvironmentError] -> ShowS
show :: EnvironmentError -> String
$cshow :: EnvironmentError -> String
showsPrec :: Int -> EnvironmentError -> ShowS
$cshowsPrec :: Int -> EnvironmentError -> ShowS
Show)

-- | Create an empty environment.
--
emptyEnvironment :: Environment
emptyEnvironment :: Environment
emptyEnvironment =
  Map Name Dynamic -> Environment
Environment forall k a. Map k a
Map.empty

unionsEnvironment :: [Environment] -> Environment
unionsEnvironment :: [Environment] -> Environment
unionsEnvironment =
  Map Name Dynamic -> Environment
Environment forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Environment -> Map Name Dynamic
unEnvironment

-- | Insert a symbolic / concrete pairing in to the environment.
--
insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete :: forall a. Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete (Symbolic Name
k) (Concrete a
v) =
  Map Name Dynamic -> Environment
Environment forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
k (forall a. Typeable a => a -> Dynamic
toDyn a
v) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Environment -> Map Name Dynamic
unEnvironment

-- | Cast a 'Dynamic' in to a concrete value.
--
reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic :: forall a.
Typeable a =>
Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic Dynamic
dyn =
  case forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn of
    Maybe a
Nothing ->
      forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ TypeRep -> TypeRep -> EnvironmentError
EnvironmentTypeError (forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a)) (Dynamic -> TypeRep
dynTypeRep Dynamic
dyn)
    Just a
x ->
      forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. a -> Concrete a
Concrete a
x

-- | Turns an environment in to a function for looking up a concrete value from
--   a symbolic one.
--
reifyEnvironment :: Environment -> (forall a. Symbolic a -> Either EnvironmentError (Concrete a))
reifyEnvironment :: Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment (Environment Map Name Dynamic
vars) (Symbolic Name
n) =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name Dynamic
vars of
    Maybe Dynamic
Nothing ->
      forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Name -> EnvironmentError
EnvironmentValueNotFound Name
n
    Just Dynamic
dyn ->
      forall a.
Typeable a =>
Dynamic -> Either EnvironmentError (Concrete a)
reifyDynamic Dynamic
dyn

-- | Convert a symbolic structure to a concrete one, using the provided environment.
--
reify :: TraversableB t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify :: forall (t :: (* -> *) -> *).
TraversableB t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
vars =
  forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
       (g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
btraverse (Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment Environment
vars)

------------------------------------------------------------------------
-- Callbacks

-- | Optional command configuration.
--
data Callback input output state =
  -- | A pre-condition for a command that must be verified before the command
  --   can be executed. This is mainly used during shrinking to ensure that it
  --   is still OK to run a command despite the fact that some previously
  --   executed commands may have been removed from the sequence.
  --
    Require (state Symbolic -> input Symbolic -> Bool)

  -- | Updates the model state, given the input and output of the command. Note
  --   that this function is polymorphic in the type of values. This is because
  --   it must work over 'Symbolic' values when we are generating actions, and
  --   'Concrete' values when we are executing them.
  --
  | Update (forall v. Ord1 v => state v -> input v -> Var output v -> state v)

  -- | A post-condition for a command that must be verified for the command to
  --   be considered a success.
  --
  --   This callback receives the state prior to execution as the first
  --   argument, and the state after execution as the second argument.
  --
  | Ensure (state Concrete -> state Concrete -> input Concrete -> output -> Test ())

callbackRequire1 ::
     state Symbolic
  -> input Symbolic
  -> Callback input output state
  -> Bool
callbackRequire1 :: forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
state Symbolic
-> input Symbolic -> Callback input output state -> Bool
callbackRequire1 state Symbolic
s input Symbolic
i = \case
  Require state Symbolic -> input Symbolic -> Bool
f ->
    state Symbolic -> input Symbolic -> Bool
f state Symbolic
s input Symbolic
i
  Update forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ ->
    Bool
True
  Ensure state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_ ->
    Bool
True

callbackUpdate1 ::
     Ord1 v
  => state v
  -> input v
  -> Var output v
  -> Callback input output state
  -> state v
callbackUpdate1 :: forall (v :: * -> *) (state :: (* -> *) -> *)
       (input :: (* -> *) -> *) output.
Ord1 v =>
state v
-> input v
-> Var output v
-> Callback input output state
-> state v
callbackUpdate1 state v
s input v
i Var output v
o = \case
  Require state Symbolic -> input Symbolic -> Bool
_ ->
    state v
s
  Update forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
f ->
    forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
f state v
s input v
i Var output v
o
  Ensure state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_ ->
    state v
s

callbackEnsure1 ::
     state Concrete
  -> state Concrete
  -> input Concrete
  -> output
  -> Callback input output state
  -> Test ()
callbackEnsure1 :: forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
state Concrete
-> state Concrete
-> input Concrete
-> output
-> Callback input output state
-> Test ()
callbackEnsure1 state Concrete
s0 state Concrete
s input Concrete
i output
o = \case
  Require state Symbolic -> input Symbolic -> Bool
_ ->
    forall (m :: * -> *). MonadTest m => m ()
success
  Update forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ ->
    forall (m :: * -> *). MonadTest m => m ()
success
  Ensure state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
f ->
    state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
f state Concrete
s0 state Concrete
s input Concrete
i output
o

callbackRequire ::
     [Callback input output state]
  -> state Symbolic
  -> input Symbolic
  -> Bool
callbackRequire :: forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
callbackRequire [Callback input output state]
callbacks state Symbolic
s input Symbolic
i =
  forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
state Symbolic
-> input Symbolic -> Callback input output state -> Bool
callbackRequire1 state Symbolic
s input Symbolic
i) [Callback input output state]
callbacks

callbackUpdate ::
     Ord1 v
  => [Callback input output state]
  -> state v
  -> input v
  -> Var output v
  -> state v
callbackUpdate :: forall (v :: * -> *) (input :: (* -> *) -> *) output
       (state :: (* -> *) -> *).
Ord1 v =>
[Callback input output state]
-> state v -> input v -> Var output v -> state v
callbackUpdate [Callback input output state]
callbacks state v
s0 input v
i Var output v
o =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\state v
s -> forall (v :: * -> *) (state :: (* -> *) -> *)
       (input :: (* -> *) -> *) output.
Ord1 v =>
state v
-> input v
-> Var output v
-> Callback input output state
-> state v
callbackUpdate1 state v
s input v
i Var output v
o) state v
s0 [Callback input output state]
callbacks

callbackEnsure ::
     [Callback input output state]
  -> state Concrete
  -> state Concrete
  -> input Concrete
  -> output
  -> Test ()
callbackEnsure :: forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Concrete
-> state Concrete
-> input Concrete
-> output
-> Test ()
callbackEnsure [Callback input output state]
callbacks state Concrete
s0 state Concrete
s input Concrete
i output
o =
  forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (state :: (* -> *) -> *) (input :: (* -> *) -> *) output.
state Concrete
-> state Concrete
-> input Concrete
-> output
-> Callback input output state
-> Test ()
callbackEnsure1 state Concrete
s0 state Concrete
s input Concrete
i output
o) [Callback input output state]
callbacks

------------------------------------------------------------------------

-- | The specification for the expected behaviour of an
-- 'Action'. These are used to generate sequences of actions to test.
--
-- This is the main type you will use when writing state machine
-- tests. @gen@ is usually an instance of 'MonadGen', and @m@ is usually
-- an instance of 'MonadTest'. These constraints appear when you pass
-- your 'Command' list to 'sequential' or 'parallel'.
--
data Command gen m (state :: (Type -> Type) -> Type) =
  forall input output.
  (TraversableB input, Show (input Symbolic), Show output, Typeable output) =>
  Command {
    -- | A generator which provides random arguments for a command. If the
    --   command cannot be executed in the current state, it should return
    --   'Nothing'.
    --
      ()
commandGen ::
        state Symbolic -> Maybe (gen (input Symbolic))

    -- | Executes a command using the arguments generated by 'commandGen'.
    --
    , ()
commandExecute ::
        input Concrete -> m output

    -- | A set of callbacks which provide optional command configuration such
    --   as pre-condtions, post-conditions and state updates.
    --
    , ()
commandCallbacks ::
        [Callback input output state]
    }

-- | Checks that input for a command can be executed in the given state.
--
commandGenOK :: Command gen m state -> state Symbolic -> Bool
commandGenOK :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
Command gen m state -> state Symbolic -> Bool
commandGenOK (Command state Symbolic -> Maybe (gen (input Symbolic))
inputGen input Concrete -> m output
_ [Callback input output state]
_) state Symbolic
state =
  forall a. Maybe a -> Bool
Maybe.isJust (state Symbolic -> Maybe (gen (input Symbolic))
inputGen state Symbolic
state)

-- | An instantiation of a 'Command' which can be executed, and its effect
--   evaluated.
--
data Action m (state :: (Type -> Type) -> Type) =
  forall input output.
  (TraversableB input, Show (input Symbolic), Show output) =>
  Action {
      ()
actionInput ::
        input Symbolic

    , ()
actionOutput ::
        Symbolic output

    , ()
actionExecute ::
        input Concrete -> m output

    , ()
actionRequire ::
        state Symbolic -> input Symbolic -> Bool

    , ()
actionUpdate ::
        forall v. Ord1 v => state v -> input v -> Var output v -> state v

    , ()
actionEnsure ::
        state Concrete -> state Concrete -> input Concrete -> output -> Test ()
    }

instance Show (Action m state) where
  showsPrec :: Int -> Action m state -> ShowS
showsPrec Int
p (Action input Symbolic
input (Symbolic (Name Int
output)) input Concrete -> m output
_ state Symbolic -> input Symbolic -> Bool
_ forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_) =
    Bool -> ShowS -> ShowS
showParen (Int
p forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"Var " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 Int
output forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      String -> ShowS
showString String
" :<- " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 input Symbolic
input

-- | Extract the variable name and the type from a symbolic value.
--
takeSymbolic :: forall a. Symbolic a -> (Name, TypeRep)
takeSymbolic :: forall a. Symbolic a -> (Name, TypeRep)
takeSymbolic (Symbolic Name
name) =
  (Name
name, forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {k} (t :: k). Proxy t
Proxy :: Proxy a))

-- | Insert a symbolic variable in to a map of variables to types.
--
insertSymbolic :: Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic :: forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic a
s =
  let
    (Name
name, TypeRep
typ) =
      forall a. Symbolic a -> (Name, TypeRep)
takeSymbolic Symbolic a
s
  in
    forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
name TypeRep
typ

-- | Collects all the symbolic values in a data structure and produces a set of
--   all the variables they refer to.
--
takeVariables :: forall t. TraversableB t => t Symbolic -> Map Name TypeRep
takeVariables :: forall (t :: (* -> *) -> *).
TraversableB t =>
t Symbolic -> Map Name TypeRep
takeVariables t Symbolic
xs =
  let
    go :: Symbolic a -> m (Symbolic a)
go Symbolic a
x = do
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic a
x)
      forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbolic a
x
  in
    forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> s
execState forall k a. Map k a
Map.empty forall a b. (a -> b) -> a -> b
$ forall k (b :: (k -> *) -> *) (e :: * -> *) (f :: k -> *)
       (g :: k -> *).
(TraversableB b, Applicative e) =>
(forall (a :: k). f a -> e (g a)) -> b f -> e (b g)
btraverse forall {m :: * -> *} {a}.
MonadState (Map Name TypeRep) m =>
Symbolic a -> m (Symbolic a)
go t Symbolic
xs

-- | Checks that the symbolic values in the data structure refer only to the
--   variables in the provided set, and that they are of the correct type.
--
variablesOK :: TraversableB t => t Symbolic -> Map Name TypeRep -> Bool
variablesOK :: forall (t :: (* -> *) -> *).
TraversableB t =>
t Symbolic -> Map Name TypeRep -> Bool
variablesOK t Symbolic
xs Map Name TypeRep
allowed =
  let
    vars :: Map Name TypeRep
vars =
      forall (t :: (* -> *) -> *).
TraversableB t =>
t Symbolic -> Map Name TypeRep
takeVariables t Symbolic
xs
  in
    forall k a. Map k a -> Bool
Map.null (Map Name TypeRep
vars forall k a b. Ord k => Map k a -> Map k b -> Map k a
`Map.difference` Map Name TypeRep
allowed) Bool -> Bool -> Bool
&&
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith forall a. Eq a => a -> a -> Bool
(==) Map Name TypeRep
vars Map Name TypeRep
allowed)

data Context state =
  Context {
      forall (state :: (* -> *) -> *). Context state -> state Symbolic
contextState :: state Symbolic
    , forall (state :: (* -> *) -> *). Context state -> Map Name TypeRep
_contextVars :: Map Name TypeRep
    }

mkContext :: state Symbolic -> Context state
mkContext :: forall (state :: (* -> *) -> *). state Symbolic -> Context state
mkContext state Symbolic
initial =
  forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
initial forall k a. Map k a
Map.empty

contextUpdate :: MonadState (Context state) m => state Symbolic -> m ()
contextUpdate :: forall (state :: (* -> *) -> *) (m :: * -> *).
MonadState (Context state) m =>
state Symbolic -> m ()
contextUpdate state Symbolic
state = do
  Context state Symbolic
_ Map Name TypeRep
vars <- forall s (m :: * -> *). MonadState s m => m s
get
  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
state Map Name TypeRep
vars

contextNewVar :: (MonadState (Context state) m, Typeable a) => m (Symbolic a)
contextNewVar :: forall (state :: (* -> *) -> *) (m :: * -> *) a.
(MonadState (Context state) m, Typeable a) =>
m (Symbolic a)
contextNewVar = do
  Context state Symbolic
state Map Name TypeRep
vars <- forall s (m :: * -> *). MonadState s m => m s
get

  let
    var :: Symbolic a
var =
      case forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.maxViewWithKey Map Name TypeRep
vars of
        Maybe ((Name, TypeRep), Map Name TypeRep)
Nothing ->
          forall a. Typeable a => Name -> Symbolic a
Symbolic Name
0
        Just ((Name
name, TypeRep
_), Map Name TypeRep
_) ->
          forall a. Typeable a => Name -> Symbolic a
Symbolic (Name
name forall a. Num a => a -> a -> a
+ Name
1)

  forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
state (forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic a
var Map Name TypeRep
vars)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Symbolic a
var

-- | Drops invalid actions from the sequence.
--
dropInvalid :: [Action m state] -> State (Context state) [Action m state]
dropInvalid :: forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state] -> State (Context state) [Action m state]
dropInvalid =
  let
    loop :: Action m state -> m (Maybe (Action m state))
loop step :: Action m state
step@(Action input Symbolic
input Symbolic output
output input Concrete -> m output
_execute state Symbolic -> input Symbolic -> Bool
require forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_ensure) = do
      Context state Symbolic
state0 Map Name TypeRep
vars0 <- forall s (m :: * -> *). MonadState s m => m s
get

      if state Symbolic -> input Symbolic -> Bool
require state Symbolic
state0 input Symbolic
input Bool -> Bool -> Bool
&& forall (t :: (* -> *) -> *).
TraversableB t =>
t Symbolic -> Map Name TypeRep -> Bool
variablesOK input Symbolic
input Map Name TypeRep
vars0 then do
        let
          state :: state Symbolic
state =
            forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Symbolic
state0 input Symbolic
input (forall a (v :: * -> *). v a -> Var a v
Var Symbolic output
output)

          vars :: Map Name TypeRep
vars =
            forall a. Symbolic a -> Map Name TypeRep -> Map Name TypeRep
insertSymbolic Symbolic output
output Map Name TypeRep
vars0

        forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall (state :: (* -> *) -> *).
state Symbolic -> Map Name TypeRep -> Context state
Context state Symbolic
state Map Name TypeRep
vars
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Action m state
step
      else
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
  in
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [Maybe a] -> [a]
Maybe.catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {m :: * -> *} {state :: (* -> *) -> *} {m :: * -> *}.
MonadState (Context state) m =>
Action m state -> m (Maybe (Action m state))
loop

-- | Generates a single action from a set of possible commands.
--
action ::
     (MonadGen gen, MonadTest m)
  => [Command gen m state]
  -> GenT (StateT (Context state) (GenBase gen)) (Action m state)
action :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
[Command gen m state]
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
action [Command gen m state]
commands =
  forall (m :: * -> *) a. MonadGen m => m (Maybe a) -> m a
Gen.justT forall a b. (a -> b) -> a -> b
$ do
    Context state Symbolic
state0 Map Name TypeRep
_ <- forall s (m :: * -> *). MonadState s m => m s
get

    Command state Symbolic -> Maybe (gen (input Symbolic))
mgenInput input Concrete -> m output
exec [Callback input output state]
callbacks <-
      forall (m :: * -> *) a. MonadGen m => [a] -> m a
Gen.element_ forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (\Command gen m state
c -> forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
Command gen m state -> state Symbolic -> Bool
commandGenOK Command gen m state
c state Symbolic
state0) [Command gen m state]
commands

    -- If we shrink the input, we still want to use the same output. Otherwise
    -- any actions using this output as part of their input will be dropped. But
    -- the existing output is still in the context, so `contextNewVar` will
    -- create a new one. To avoid that, we generate the output before the input.
    Symbolic output
output <- forall (state :: (* -> *) -> *) (m :: * -> *) a.
(MonadState (Context state) m, Typeable a) =>
m (Symbolic a)
contextNewVar

    input Symbolic
input <-
      case state Symbolic -> Maybe (gen (input Symbolic))
mgenInput state Symbolic
state0 of
        Maybe (gen (input Symbolic))
Nothing ->
          forall a. HasCallStack => String -> a
error String
"genCommand: internal error, tried to use generator with invalid state."
        Just gen (input Symbolic)
gen ->
          forall {k} (t :: (* -> *) -> k -> *) (m :: * -> *) (n :: * -> *)
       (b :: k).
(MFunctor t, Monad m) =>
(forall a. m a -> n a) -> t m b -> t n b
hoist forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadGen m => m a -> GenT (GenBase m) a
Gen.toGenT gen (input Symbolic)
gen

    if Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
callbackRequire [Callback input output state]
callbacks state Symbolic
state0 input Symbolic
input then
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

    else do
      forall (state :: (* -> *) -> *) (m :: * -> *).
MonadState (Context state) m =>
state Symbolic -> m ()
contextUpdate forall a b. (a -> b) -> a -> b
$
        forall (v :: * -> *) (input :: (* -> *) -> *) output
       (state :: (* -> *) -> *).
Ord1 v =>
[Callback input output state]
-> state v -> input v -> Var output v -> state v
callbackUpdate [Callback input output state]
callbacks state Symbolic
state0 input Symbolic
input (forall a (v :: * -> *). v a -> Var a v
Var Symbolic output
output)

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) (state :: (* -> *) -> *)
       (input :: (* -> *) -> *) output.
(TraversableB input, Show (input Symbolic), Show output) =>
input Symbolic
-> Symbolic output
-> (input Concrete -> m output)
-> (state Symbolic -> input Symbolic -> Bool)
-> (forall (v :: * -> *).
    Ord1 v =>
    state v -> input v -> Var output v -> state v)
-> (state Concrete
    -> state Concrete -> input Concrete -> output -> Test ())
-> Action m state
Action input Symbolic
input Symbolic output
output input Concrete -> m output
exec
          (forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Symbolic -> input Symbolic -> Bool
callbackRequire [Callback input output state]
callbacks)
          (forall (v :: * -> *) (input :: (* -> *) -> *) output
       (state :: (* -> *) -> *).
Ord1 v =>
[Callback input output state]
-> state v -> input v -> Var output v -> state v
callbackUpdate [Callback input output state]
callbacks)
          (forall (input :: (* -> *) -> *) output (state :: (* -> *) -> *).
[Callback input output state]
-> state Concrete
-> state Concrete
-> input Concrete
-> output
-> Test ()
callbackEnsure [Callback input output state]
callbacks)

genActions ::
     (MonadGen gen, MonadTest m)
  => Range Int
  -> [Command gen m state]
  -> Context state
  -> gen ([Action m state], Context state)
genActions :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
range [Command gen m state]
commands Context state
ctx = do
  [Action m state]
xs <- forall (m :: * -> *) a. MonadGen m => GenT (GenBase m) a -> m a
Gen.fromGenT forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
`evalStateT` Context state
ctx) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (g :: (* -> *) -> * -> *) (f :: (* -> *) -> * -> *)
       (m :: * -> *) a.
(MonadTransDistributive g, Transformer f g m) =>
g (f m) a -> f (g m) a
distributeT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadGen m => Range Int -> m a -> m [a]
Gen.list Range Int
range (forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
[Command gen m state]
-> GenT (StateT (Context state) (GenBase gen)) (Action m state)
action [Command gen m state]
commands)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state] -> State (Context state) [Action m state]
dropInvalid [Action m state]
xs forall s a. State s a -> s -> (a, s)
`runState` Context state
ctx

-- | A sequence of actions to execute.
--
newtype Sequential m state =
  Sequential {
      -- | The sequence of actions.
      forall (m :: * -> *) (state :: (* -> *) -> *).
Sequential m state -> [Action m state]
sequentialActions :: [Action m state]
    }

renderAction :: Action m state -> [String]
renderAction :: forall (m :: * -> *) (state :: (* -> *) -> *).
Action m state -> [String]
renderAction (Action input Symbolic
input (Symbolic (Name Int
output)) input Concrete -> m output
_ state Symbolic -> input Symbolic -> Bool
_ forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_) =
  let
    prefix0 :: String
prefix0 =
      String
"Var " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
output forall a. [a] -> [a] -> [a]
++ String
" = "

    prefix :: String
prefix =
      forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
prefix0) Char
' '
  in
    case String -> [String]
lines (forall a. Show a => a -> String
showPretty input Symbolic
input) of
      [] ->
        [String
prefix0 forall a. [a] -> [a] -> [a]
++ String
"?"]
      String
x : [String]
xs ->
        (String
prefix0 forall a. [a] -> [a] -> [a]
++ String
x) forall a. a -> [a] -> [a]
:
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
prefix forall a. [a] -> [a] -> [a]
++) [String]
xs

renderActionResult :: Environment -> Action m state -> [String]
renderActionResult :: forall (m :: * -> *) (state :: (* -> *) -> *).
Environment -> Action m state -> [String]
renderActionResult Environment
env (Action input Symbolic
_ output :: Symbolic output
output@(Symbolic (Name Int
name)) input Concrete -> m output
_ state Symbolic -> input Symbolic -> Bool
_ forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
_ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
_) =
  let
    prefix0 :: String
prefix0 =
      String
"Var " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
name forall a. [a] -> [a] -> [a]
++ String
" = "

    prefix :: String
prefix =
      forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length String
prefix0) Char
' '

    unfound :: EnvironmentError -> String
unfound = \case
      EnvironmentValueNotFound Name
_
        -> String
"<<not found in environment>>"
      EnvironmentTypeError TypeRep
_ TypeRep
_
        -> String
"<<type representation in environment unexpected>>"

    actual :: String
actual =
      forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either EnvironmentError -> String
unfound forall a. Show a => a -> String
showPretty
        forall a b. (a -> b) -> a -> b
$ Environment
-> forall a. Symbolic a -> Either EnvironmentError (Concrete a)
reifyEnvironment Environment
env Symbolic output
output

  in
    case String -> [String]
lines String
actual of
      [] ->
        [String
prefix0 forall a. [a] -> [a] -> [a]
++ String
"?"]
      String
x : [String]
xs ->
        (String
prefix0 forall a. [a] -> [a] -> [a]
++ String
x) forall a. a -> [a] -> [a]
:
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String
prefix forall a. [a] -> [a] -> [a]
++) [String]
xs

-- FIXME we should not abuse Show to get nice output for actions
instance Show (Sequential m state) where
  show :: Sequential m state -> String
show (Sequential [Action m state]
xs) =
    [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall (m :: * -> *) (state :: (* -> *) -> *).
Action m state -> [String]
renderAction [Action m state]
xs

-- | Generates a sequence of actions from an initial model state and set of commands.
--
sequential ::
     (MonadGen gen, MonadTest m)
  => Range Int
  -> (forall v. state v)
  -> [Command gen m state]
  -> gen (Sequential m state)
sequential :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> (forall (v :: * -> *). state v)
-> [Command gen m state]
-> gen (Sequential m state)
sequential Range Int
range forall (v :: * -> *). state v
initial [Command gen m state]
commands =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state] -> Sequential m state
Sequential forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$
    forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
range [Command gen m state]
commands (forall (state :: (* -> *) -> *). state Symbolic -> Context state
mkContext forall (v :: * -> *). state v
initial)

-- | A sequential prefix of actions to execute, with two branches to execute in parallel.
--
data Parallel m state =
  Parallel {
      -- | The sequential prefix.
      forall (m :: * -> *) (state :: (* -> *) -> *).
Parallel m state -> [Action m state]
parallelPrefix :: [Action m state]

      -- | The first branch.
    , forall (m :: * -> *) (state :: (* -> *) -> *).
Parallel m state -> [Action m state]
parallelBranch1 :: [Action m state]

      -- | The second branch.
    , forall (m :: * -> *) (state :: (* -> *) -> *).
Parallel m state -> [Action m state]
parallelBranch2 :: [Action m state]
    }

-- FIXME we should not abuse Show to get nice output for actions
instance Show (Parallel m state) where
  show :: Parallel m state -> String
show =
    forall (m :: * -> *) (state :: (* -> *) -> *).
(Action m state -> [String]) -> Parallel m state -> String
renderParallel forall (m :: * -> *) (state :: (* -> *) -> *).
Action m state -> [String]
renderAction

renderParallel :: (Action m state -> [String]) -> Parallel m state -> String
renderParallel :: forall (m :: * -> *) (state :: (* -> *) -> *).
(Action m state -> [String]) -> Parallel m state -> String
renderParallel Action m state -> [String]
render (Parallel [Action m state]
pre [Action m state]
xs [Action m state]
ys) =
  [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
      [String
"━━━ Prefix ━━━"]
    , forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
render [Action m state]
pre
    , [String
"", String
"━━━ Branch 1 ━━━"]
    , forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
render [Action m state]
xs
    , [String
"", String
"━━━ Branch 2 ━━━"]
    , forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Action m state -> [String]
render [Action m state]
ys
    ]


-- | Given the initial model state and set of commands, generates prefix
--   actions to be run sequentially, followed by two branches to be run in
--   parallel.
--
parallel ::
     (MonadGen gen, MonadTest m)
  => Range Int
  -> Range Int
  -> (forall v. state v)
  -> [Command gen m state]
  -> gen (Parallel m state)
parallel :: forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> Range Int
-> (forall (v :: * -> *). state v)
-> [Command gen m state]
-> gen (Parallel m state)
parallel Range Int
prefixN Range Int
parallelN forall (v :: * -> *). state v
initial [Command gen m state]
commands = do
  ([Action m state]
prefix, Context state
ctx0) <- forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
prefixN [Command gen m state]
commands (forall (state :: (* -> *) -> *). state Symbolic -> Context state
mkContext forall (v :: * -> *). state v
initial)
  ([Action m state]
branch1, Context state
ctx1) <- forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
parallelN [Command gen m state]
commands Context state
ctx0
  ([Action m state]
branch2, Context state
_ctx2) <- forall (gen :: * -> *) (m :: * -> *) (state :: (* -> *) -> *).
(MonadGen gen, MonadTest m) =>
Range Int
-> [Command gen m state]
-> Context state
-> gen ([Action m state], Context state)
genActions Range Int
parallelN [Command gen m state]
commands Context state
ctx1 { contextState :: state Symbolic
contextState = forall (state :: (* -> *) -> *). Context state -> state Symbolic
contextState Context state
ctx0 }

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (state :: (* -> *) -> *).
[Action m state]
-> [Action m state] -> [Action m state] -> Parallel m state
Parallel [Action m state]
prefix [Action m state]
branch1 [Action m state]
branch2

data ActionCheck state =
  ActionCheck {
      forall (state :: (* -> *) -> *).
ActionCheck state -> state Concrete -> state Concrete
checkUpdate :: state Concrete -> state Concrete
    , forall (state :: (* -> *) -> *).
ActionCheck state -> state Concrete -> state Concrete -> Test ()
checkEnsure :: state Concrete -> state Concrete -> Test ()
    }

execute :: (MonadTest m, HasCallStack) => Action m state -> StateT Environment m (ActionCheck state)
execute :: forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
Action m state -> StateT Environment m (ActionCheck state)
execute (Action input Symbolic
sinput Symbolic output
soutput input Concrete -> m output
exec state Symbolic -> input Symbolic -> Bool
_require forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure) =
  forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall a b. (a -> b) -> a -> b
$ do
    Environment
env0 <- forall s (m :: * -> *). MonadState s m => m s
get
    input Concrete
input <- forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> *).
TraversableB t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
env0 input Symbolic
sinput
    output
output <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ input Concrete -> m output
exec input Concrete
input

    let
      coutput :: Concrete output
coutput =
        forall a. a -> Concrete a
Concrete output
output

      env :: Environment
env =
        forall a. Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete Symbolic output
soutput Concrete output
coutput Environment
env0

    forall s (m :: * -> *). MonadState s m => s -> m ()
put Environment
env

    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
      forall (state :: (* -> *) -> *).
(state Concrete -> state Concrete)
-> (state Concrete -> state Concrete -> Test ())
-> ActionCheck state
ActionCheck
        (\state Concrete
s0 -> forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
s0 input Concrete
input (forall a (v :: * -> *). v a -> Var a v
Var Concrete output
coutput))
        (\state Concrete
s0 state Concrete
s -> state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure state Concrete
s0 state Concrete
s input Concrete
input output
output)

-- | Executes a single action in the given evironment.
--
executeUpdateEnsure ::
     (MonadTest m, HasCallStack)
  => (state Concrete, Environment)
  -> Action m state
  -> m (state Concrete, Environment)
executeUpdateEnsure :: forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
(state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
executeUpdateEnsure (state Concrete
state0, Environment
env0) (Action input Symbolic
sinput Symbolic output
soutput input Concrete -> m output
exec state Symbolic -> input Symbolic -> Bool
_require forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure) =
  forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall a b. (a -> b) -> a -> b
$ do
    input Concrete
input <- forall (m :: * -> *) x a.
(MonadTest m, Show x, HasCallStack) =>
Either x a -> m a
evalEither forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> *).
TraversableB t =>
Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
reify Environment
env0 input Symbolic
sinput
    output
output <- input Concrete -> m output
exec input Concrete
input

    let
      coutput :: Concrete output
coutput =
        forall a. a -> Concrete a
Concrete output
output

      state :: state Concrete
state =
        forall (v :: * -> *).
Ord1 v =>
state v -> input v -> Var output v -> state v
update state Concrete
state0 input Concrete
input (forall a (v :: * -> *). v a -> Var a v
Var Concrete output
coutput)

      env :: Environment
env =
        forall a. Symbolic a -> Concrete a -> Environment -> Environment
insertConcrete Symbolic output
soutput Concrete output
coutput Environment
env0

    forall (m :: * -> *) a. MonadTest m => Test a -> m a
liftTest forall a b. (a -> b) -> a -> b
$ state Concrete
-> state Concrete -> input Concrete -> output -> Test ()
ensure state Concrete
state0 state Concrete
state input Concrete
input output
output

    forall (f :: * -> *) a. Applicative f => a -> f a
pure (state Concrete
state, Environment
env)

-- | Executes a list of actions sequentially, verifying that all
--   post-conditions are met and no exceptions are thrown.
--
--   To generate a sequence of actions to execute, see the
--   'Hedgehog.Gen.sequential' combinator in the "Hedgehog.Gen" module.
--
executeSequential ::
     (MonadTest m, MonadCatch m, HasCallStack)
  => (forall v. state v)
  -> Sequential m state
  -> m ()
executeSequential :: forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, MonadCatch m, HasCallStack) =>
(forall (v :: * -> *). state v) -> Sequential m state -> m ()
executeSequential forall (v :: * -> *). state v
initial (Sequential [Action m state]
xs) =
  forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTest m, MonadCatch m, HasCallStack) =>
m a -> m a
evalM forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m ()
foldM_ forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
(state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
executeUpdateEnsure (forall (v :: * -> *). state v
initial, Environment
emptyEnvironment) [Action m state]
xs

successful :: Test () -> Bool
successful :: Test () -> Bool
successful Test ()
x =
  case forall a. Test a -> (Either Failure a, Journal)
runTest Test ()
x of
    (Left Failure
_, Journal
_) ->
      Bool
False
    (Right ()
_, Journal
_) ->
      Bool
True

interleave :: [a] -> [a] -> [[a]]
interleave :: forall a. [a] -> [a] -> [[a]]
interleave [a]
xs00 [a]
ys00 =
  case ([a]
xs00, [a]
ys00) of
    ([], []) ->
      []
    ([a]
xs, []) ->
      [[a]
xs]
    ([], [a]
ys) ->
      [[a]
ys]
    (xs0 :: [a]
xs0@(a
x:[a]
xs), ys0 :: [a]
ys0@(a
y:[a]
ys)) ->
      [ a
x forall a. a -> [a] -> [a]
: [a]
zs | [a]
zs <- forall a. [a] -> [a] -> [[a]]
interleave [a]
xs [a]
ys0 ] forall a. [a] -> [a] -> [a]
++
      [ a
y forall a. a -> [a] -> [a]
: [a]
zs | [a]
zs <- forall a. [a] -> [a] -> [[a]]
interleave [a]
xs0 [a]
ys ]

checkActions :: state Concrete -> [ActionCheck state] -> Test ()
checkActions :: forall (state :: (* -> *) -> *).
state Concrete -> [ActionCheck state] -> Test ()
checkActions state Concrete
s0 = \case
  [] ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  ActionCheck state
x : [ActionCheck state]
xs -> do
    let
      s :: state Concrete
s =
        forall (state :: (* -> *) -> *).
ActionCheck state -> state Concrete -> state Concrete
checkUpdate ActionCheck state
x state Concrete
s0

    forall (state :: (* -> *) -> *).
ActionCheck state -> state Concrete -> state Concrete -> Test ()
checkEnsure ActionCheck state
x state Concrete
s0 state Concrete
s
    forall (state :: (* -> *) -> *).
state Concrete -> [ActionCheck state] -> Test ()
checkActions state Concrete
s [ActionCheck state]
xs

linearize :: MonadTest m => state Concrete -> [ActionCheck state] -> [ActionCheck state] -> m ()
linearize :: forall (m :: * -> *) (state :: (* -> *) -> *).
MonadTest m =>
state Concrete
-> [ActionCheck state] -> [ActionCheck state] -> m ()
linearize state Concrete
initial [ActionCheck state]
branch1 [ActionCheck state]
branch2 =
  forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall a b. (a -> b) -> a -> b
$
    let
      ok :: Bool
ok =
        forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Test () -> Bool
successful forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (state :: (* -> *) -> *).
state Concrete -> [ActionCheck state] -> Test ()
checkActions state Concrete
initial) forall a b. (a -> b) -> a -> b
$
        forall a. [a] -> [a] -> [[a]]
interleave [ActionCheck state]
branch1 [ActionCheck state]
branch2
    in
      if Bool
ok then
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      else
        forall (m :: * -> *) a.
(MonadTest m, HasCallStack) =>
Maybe Diff -> String -> m a
failWith forall a. Maybe a
Nothing String
"no valid interleaving"


-- | Executes the prefix actions sequentially, then executes the two branches
--   in parallel, verifying that no exceptions are thrown and that there is at
--   least one sequential interleaving where all the post-conditions are met.
--
--   To generate parallel actions to execute, see the 'Hedgehog.Gen.parallel'
--   combinator in the "Hedgehog.Gen" module.
--
executeParallel ::
     (MonadTest m, MonadCatch m, MonadBaseControl IO m, HasCallStack)
  => (forall v. state v)
  -> Parallel m state
  -> m ()
executeParallel :: forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, MonadCatch m, MonadBaseControl IO m, HasCallStack) =>
(forall (v :: * -> *). state v) -> Parallel m state -> m ()
executeParallel forall (v :: * -> *). state v
initial p :: Parallel m state
p@(Parallel [Action m state]
prefix [Action m state]
branch1 [Action m state]
branch2) =
  forall a. HasCallStack => (HasCallStack => a) -> a
withFrozenCallStack forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTest m, MonadCatch m, HasCallStack) =>
m a -> m a
evalM forall a b. (a -> b) -> a -> b
$ do
    (state Concrete
s0, Environment
env0) <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
(state Concrete, Environment)
-> Action m state -> m (state Concrete, Environment)
executeUpdateEnsure (forall (v :: * -> *). state v
initial, Environment
emptyEnvironment) [Action m state]
prefix

    (([ActionCheck state]
xs, Environment
env1), ([ActionCheck state]
ys, Environment
env2)) <-
      forall (m :: * -> *) a b.
MonadBaseControl IO m =>
m a -> m b -> m (a, b)
Async.concurrently
        (forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
Action m state -> StateT Environment m (ActionCheck state)
execute [Action m state]
branch1) Environment
env0)
        (forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *) (state :: (* -> *) -> *).
(MonadTest m, HasCallStack) =>
Action m state -> StateT Environment m (ActionCheck state)
execute [Action m state]
branch2) Environment
env0)

    let
      env :: Environment
env = [Environment] -> Environment
unionsEnvironment [Environment
env0, Environment
env1, Environment
env2]

    forall (m :: * -> *). (MonadTest m, HasCallStack) => String -> m ()
annotate forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (state :: (* -> *) -> *).
(Action m state -> [String]) -> Parallel m state -> String
renderParallel (forall (m :: * -> *) (state :: (* -> *) -> *).
Environment -> Action m state -> [String]
renderActionResult Environment
env) Parallel m state
p
    forall (m :: * -> *) (state :: (* -> *) -> *).
MonadTest m =>
state Concrete
-> [ActionCheck state] -> [ActionCheck state] -> m ()
linearize state Concrete
s0 [ActionCheck state]
xs [ActionCheck state]
ys