-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Test monadic programs using state machine based models
--   
--   See README at
--   <a>https://github.com/advancedtelematic/quickcheck-state-machine#readme</a>
@package quickcheck-state-machine
@version 0.2.0


-- | This module contains Z-inspried combinators for working with
--   relations. The idea is that they can be used to define concise and
--   showable models. This module is an experiment and will likely change
--   or move to its own package.
module Test.StateMachine.Z
union :: Eq a => [a] -> [a] -> [a]
intersect :: Eq a => [a] -> [a] -> [a]
isSubsetOf :: Eq a => [a] -> [a] -> Bool
(~=) :: Eq a => [a] -> [a] -> Bool

-- | Relations.
type Rel a b = [(a, b)]

-- | (Partial) functions.
type Fun a b = Rel a b
empty :: Rel a b
identity :: [a] -> Rel a a
singleton :: a -> b -> Rel a b
domain :: Rel a b -> [a]
codomain :: Rel a b -> [b]
compose :: Eq b => Rel b c -> Rel a b -> Rel a c
fcompose :: Eq b => Rel a b -> Rel b c -> Rel a c
inverse :: Rel a b -> Rel b a
lookupDom :: Eq a => a -> Rel a b -> [b]
lookupCod :: Eq b => b -> Rel a b -> [a]

-- | Domain restriction.
--   
--   <pre>
--   &gt;&gt;&gt; ['a'] &lt;| [ ('a', "apa"), ('b', "bepa") ]
--   [('a',"apa")]
--   </pre>
(<|) :: Eq a => [a] -> Rel a b -> Rel a b

-- | Codomain restriction.
--   
--   <pre>
--   &gt;&gt;&gt; [ ('a', "apa"), ('b', "bepa") ] |&gt; ["apa"]
--   [('a',"apa")]
--   </pre>
(|>) :: Eq b => Rel a b -> [b] -> Rel a b

-- | Domain substraction.
--   
--   <pre>
--   &gt;&gt;&gt; ['a'] &lt;-| [ ('a', "apa"), ('b', "bepa") ]
--   [('b',"bepa")]
--   </pre>
(<-|) :: Eq a => [a] -> Rel a b -> Rel a b

-- | Codomain substraction.
--   
--   <pre>
--   &gt;&gt;&gt; [ ('a', "apa"), ('b', "bepa") ] |-&gt; ["apa"]
--   [('b',"bepa")]
--   </pre>
(|->) :: Eq b => Rel a b -> [b] -> Rel a b

-- | The image of a relation.
image :: Eq a => Rel a b -> [a] -> [b]

-- | Overriding.
--   
--   <pre>
--   &gt;&gt;&gt; [('a', "apa")] &lt;+ [('a', "bepa")]
--   [('a',"bepa")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; [('a', "apa")] &lt;+ [('b', "bepa")]
--   [('a',"apa"),('b',"bepa")]
--   </pre>
(<+) :: (Eq a, Eq b) => Rel a b -> Rel a b -> Rel a b

-- | Direct product.
(<**>) :: Eq a => Rel a b -> Rel a c -> Rel a (b, c)

-- | Parallel product.
(<||>) :: Rel a c -> Rel b d -> Rel (a, b) (c, d)
isTotalRel :: Eq a => Rel a b -> [a] -> Bool
isSurjRel :: Eq b => Rel a b -> [b] -> Bool
isTotalSurjRel :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool
isPartialFun :: (Eq a, Eq b) => Rel a b -> Bool
isTotalFun :: (Eq a, Eq b) => Rel a b -> [a] -> Bool
isPartialInj :: (Eq a, Eq b) => Rel a b -> Bool
isTotalInj :: (Eq a, Eq b) => Rel a b -> [a] -> Bool
isPartialSurj :: (Eq a, Eq b) => Rel a b -> [b] -> Bool
isTotalSurj :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool
isBijection :: (Eq a, Eq b) => Rel a b -> [a] -> [b] -> Bool

-- | Application.
(!) :: Eq a => Rel a b -> a -> Maybe b
(.!) :: Rel a b -> a -> (Rel a b, a)

-- | Assignment.
--   
--   <pre>
--   &gt;&gt;&gt; singleton 'a' "apa" .! 'a' .= "bepa"
--   [('a',"bepa")]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; singleton 'a' "apa" .! 'b' .= "bepa"
--   [('a',"apa"),('b',"bepa")]
--   </pre>
(.=) :: (Eq a, Eq b) => (Rel a b, a) -> b -> Rel a b


-- | This module exports a higher-order version of functors, foldable
--   functors, and traversable functors.
module Test.StateMachine.Types.HFunctor

-- | Higher-order functors.
class HFunctor (f :: (* -> *) -> * -> *) where hfmap f = runIdentity . htraverse (Identity . f)

-- | Higher-order version of <a>fmap</a>.
hfmap :: HFunctor f => (forall a. g a -> h a) -> f g b -> f h b

-- | Higher-order version of <a>fmap</a>.
hfmap :: (HFunctor f, HTraversable f) => (forall a. g a -> h a) -> f g b -> f h b

-- | Higher-order version of <a>fmap</a>.
hfmap :: HFunctor f => (forall a. g a -> h a) -> f g b -> f h b

-- | Higher-order foldable functors.
class HFunctor t => HFoldable (t :: (* -> *) -> * -> *) where hfoldMap f = getConst . htraverse (Const . f)

-- | Higher-order version of <a>foldMap</a>.
hfoldMap :: (HFoldable t, Monoid m) => (forall a. v a -> m) -> t v b -> m

-- | Higher-order version of <a>foldMap</a>.
hfoldMap :: (HFoldable t, HTraversable t, Monoid m) => (forall a. v a -> m) -> t v b -> m

-- | Higher-order version of <a>foldMap</a>.
hfoldMap :: (HFoldable t, Monoid m) => (forall a. v a -> m) -> t v b -> m

-- | Higher-order traversable functors.
class (HFunctor t, HFoldable t) => HTraversable (t :: (* -> *) -> * -> *)

-- | Higher-order version of <a>traverse</a>.
htraverse :: (HTraversable t, Applicative f) => (forall a. g a -> f (h a)) -> t g b -> f (t h b)

-- | Higher-order version of <a>traverse</a>.
htraverse :: (HTraversable t, Applicative f) => (forall a. g a -> f (h a)) -> t g b -> f (t h b)


-- | This module contains reference related types. It's taken almost
--   verbatim from the Hedgehog <a>library</a>.
module Test.StateMachine.Types.References

-- | References are the potential or actual result of executing an action.
--   They are parameterised by either <a>Symbolic</a> or <a>Concrete</a>
--   depending on the phase of the test.
--   
--   <a>Symbolic</a> 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.
--   
--   <a>Concrete</a> variables are the actual results of actions. These are
--   used during test execution. They provide access to the actual runtime
--   value of a variable.
newtype Reference v a
Reference :: (v a) -> Reference v a

-- | Take the value from a concrete variable.
concrete :: Reference Concrete a -> a

-- | Take the value from an opaque concrete variable.
opaque :: Reference Concrete (Opaque a) -> a

-- | Opaque values.
--   
--   Useful if you want to put something without a <a>Show</a> instance
--   inside something which you'd like to be able to display.
newtype Opaque a
Opaque :: a -> Opaque a
[unOpaque] :: Opaque a -> a

-- | Symbolic values.
data Symbolic a
[Symbolic] :: Typeable a => Var -> Symbolic a

-- | Concrete values.
newtype Concrete a
[Concrete] :: a -> Concrete a

-- | Symbolic variable names.
newtype Var
Var :: Int -> Var
instance Data.Traversable.Traversable Test.StateMachine.Types.References.Concrete
instance Data.Foldable.Foldable Test.StateMachine.Types.References.Concrete
instance GHC.Base.Functor Test.StateMachine.Types.References.Concrete
instance GHC.Read.Read a => GHC.Read.Read (Test.StateMachine.Types.References.Concrete a)
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.References.Concrete a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Concrete a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Concrete a)
instance GHC.Read.Read Test.StateMachine.Types.References.Var
instance GHC.Num.Num Test.StateMachine.Types.References.Var
instance GHC.Show.Show Test.StateMachine.Types.References.Var
instance GHC.Classes.Ord Test.StateMachine.Types.References.Var
instance GHC.Classes.Eq Test.StateMachine.Types.References.Var
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Opaque a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Opaque a)
instance GHC.Read.Read (v a) => GHC.Read.Read (Test.StateMachine.Types.References.Reference v a)
instance GHC.Classes.Eq (Test.StateMachine.Types.References.Symbolic a)
instance GHC.Classes.Ord (Test.StateMachine.Types.References.Symbolic a)
instance GHC.Show.Show (Test.StateMachine.Types.References.Symbolic a)
instance Data.Typeable.Internal.Typeable a => GHC.Read.Read (Test.StateMachine.Types.References.Symbolic a)
instance Data.Foldable.Foldable Test.StateMachine.Types.References.Symbolic
instance (Data.Functor.Classes.Eq1 v, GHC.Classes.Eq a) => GHC.Classes.Eq (Test.StateMachine.Types.References.Reference v a)
instance (Data.Functor.Classes.Ord1 v, GHC.Classes.Ord a) => GHC.Classes.Ord (Test.StateMachine.Types.References.Reference v a)
instance (Data.Functor.Classes.Show1 v, GHC.Show.Show a) => GHC.Show.Show (Test.StateMachine.Types.References.Reference v a)
instance Test.StateMachine.Types.HFunctor.HTraversable Test.StateMachine.Types.References.Reference
instance Test.StateMachine.Types.HFunctor.HFunctor Test.StateMachine.Types.References.Reference
instance Test.StateMachine.Types.HFunctor.HFoldable Test.StateMachine.Types.References.Reference
instance GHC.Show.Show (Test.StateMachine.Types.References.Opaque a)
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Symbolic
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Symbolic
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Symbolic
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Concrete


-- | Datatype-generic utilities.
module Test.StateMachine.Types.Generics

-- | A constructor name is a string.
newtype Constructor
Constructor :: String -> Constructor

-- | Extracting constructors from actions.
class Constructors (act :: (* -> *) -> * -> *)

-- | Constructor of a given action.
constructor :: Constructors act => act v a -> Constructor

-- | Total number of constructors in the action type.
nConstructors :: Constructors act => proxy act -> Int
instance GHC.Classes.Ord Test.StateMachine.Types.Generics.Constructor
instance GHC.Classes.Eq Test.StateMachine.Types.Generics.Constructor
instance GHC.Show.Show Test.StateMachine.Types.Generics.Constructor


-- | This module contains the main types exposed to the user. The module is
--   perhaps best read indirectly, on a per need basis, via the main module
--   <a>Test.StateMachine</a>.
module Test.StateMachine.Types

-- | An untyped action is an action where the response type is hidden away
--   using an existential type.
--   
--   We need to hide the response type when generating actions, because in
--   general the actions we want to generate will have different response
--   types; and thus we can only type the generating function if we hide
--   the response type.
data Untyped (act :: (* -> *) -> * -> *)
[Untyped] :: (Show resp, Typeable resp) => act Symbolic resp -> Untyped act

-- | A (non-failing) state machine record bundles up all functionality
--   needed to perform our tests.
type StateMachine model act m = StateMachine' model act Void m

-- | Helper for lifting non-failing semantics to a possibly failing state
--   machine record.
stateMachine :: Functor m => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> (forall resp. act Concrete resp -> m resp) -> Runner m -> StateMachine' model act Void m

-- | Same as above, but with possibly failing semantics.
data StateMachine' model act err m
StateMachine :: Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> Semantics act err m -> Runner m -> StateMachine' model act err m
[generator'] :: StateMachine' model act err m -> Generator model act
[shrinker'] :: StateMachine' model act err m -> Shrinker act
[precondition'] :: StateMachine' model act err m -> Precondition model act
[transition'] :: StateMachine' model act err m -> Transition model act
[postcondition'] :: StateMachine' model act err m -> Postcondition model act
[model'] :: StateMachine' model act err m -> InitialModel model
[semantics'] :: StateMachine' model act err m -> Semantics act err m
[runner'] :: StateMachine' model act err m -> Runner m

-- | When generating actions we have access to a model containing symbolic
--   references.
type Generator model act = model Symbolic -> Gen (Untyped act)

-- | Shrinking should preserve the response type of the action.
type Shrinker act = forall (v :: * -> *) resp. act v resp -> [act v resp]

-- | Pre-conditions are checked while generating, at this stage we do not
--   yet have access to concrete references.
type Precondition model act = forall resp. model Symbolic -> act Symbolic resp -> Bool

-- | The transition function must be polymorphic in the type of variables
--   used, as it is used both while generating and executing.
type Transition model act = forall resp v. Ord1 v => model v -> act v resp -> v resp -> model v

-- | Post-conditions are checked after the actions have been executed and
--   we got a response.
type Postcondition model act = forall resp. model Concrete -> act Concrete resp -> resp -> Property

-- | The initial model is polymorphic in the type of references it uses, so
--   that it can be used both in the pre- and the post-condition check.
type InitialModel m = forall (v :: * -> *). m v

-- | The result of executing an action.
data Result resp err
Ok :: resp -> Result resp err
Fail :: err -> Result resp err

-- | When we execute our actions we have access to concrete references.
type Semantics act err m = forall resp. act Concrete resp -> m (Result resp err)

-- | How to run the monad used by the semantics.
type Runner m = m Property -> IO Property


module Test.StateMachine.Internal.Utils

-- | Lifts <a>any</a> to properties.
anyP :: (a -> Property) -> [a] -> Property

-- | Lifts a plain property into a monadic property.
liftProperty :: Monad m => Property -> PropertyM m ()

-- | Lifts <a>whenFail</a> to <a>PropertyM</a>.
whenFailM :: Monad m => IO () -> Property -> PropertyM m ()

-- | A property that tests <tt>prop</tt> repeatedly <tt>n</tt> times,
--   failing as soon as any of the tests of <tt>prop</tt> fails.
alwaysP :: Int -> Property -> Property

-- | Write a metaproperty on the output of QuickChecking a property using a
--   boolean predicate on the output.
shrinkPropertyHelperC :: Show a => PropertyOf a -> (a -> Bool) -> Property

-- | Same as above, but using a property predicate.
shrinkPropertyHelperC' :: Show a => PropertyOf a -> (a -> Property) -> Property

-- | Given shrinkers for the components of a pair we can shrink the pair.
shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])

-- | Same above, but for homogeneous pairs.
shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])

-- | Remove duplicate elements from a list.
nub :: Ord a => [a] -> [a]

-- | Drop last <tt>n</tt> elements of a list.
dropLast :: Int -> [a] -> [a]

-- | Indexing starting from the back of a list.
toLast :: Int -> [a] -> a


-- | Template Haskell functions to derive some general-purpose
--   functionalities.
module Test.StateMachine.Types.Generics.TH

-- | Given a name <tt>''Action</tt>, derive <a>Show</a> for <tt>(Action v
--   a)</tt> and <tt>(<a>Untyped</a> Action)</tt>. See <a>deriveShow</a>
--   and <a>deriveShowUntyped</a>.
deriveShows :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveShow</a> ''Action
--   ===&gt;
--   deriving instance <a>Show1</a> v =&gt; <a>Show</a> (Action v a)@.
--   </pre>
deriveShow :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveShowUntyped</a> ''Action
--   ===&gt;
--   deriving instance <a>Show</a> (<a>Untyped</a> Action)
--   </pre>
deriveShowUntyped :: Name -> Q [Dec]

-- | <tt>$(<a>mkShrinker</a> ''Action)</tt> creates a generic shrinker of
--   type <tt>(Action v a -&gt; [Action v a])</tt> which ignores
--   <a>Reference</a> fields.
mkShrinker :: Name -> Q Exp

-- | <pre>
--   <a>deriveConstructors</a> ''Action
--   ===&gt;
--   instance <a>Constructors</a> Action where ...
--   </pre>
deriveConstructors :: Name -> Q [Dec]


-- | Template Haskell functions to derive higher-order structures.
module Test.StateMachine.Types.HFunctor.TH

-- | Derive <a>HFunctor</a>, <a>HFoldable</a>, <a>HTraversable</a>.
deriveHClasses :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveHTraversable</a> ''Action
--   ===&gt;
--   instance <a>HTraversable</a> Action where ...
--   </pre>
deriveHTraversable :: Name -> Q [Dec]

-- | Derive the body of <a>htraverse</a>.
mkhtraverse :: Name -> Q Exp

-- | <pre>
--   <a>deriveHFoldable</a> ''Action
--   ===&gt;
--   instance <a>HFoldable</a> Action where ...
--   </pre>
deriveHFoldable :: Name -> Q [Dec]

-- | Derive the body of <a>hfoldMap</a>.
mkhfoldMap :: Name -> Q Exp

-- | <pre>
--   <a>deriveHFunctor</a> ''Action
--   ===&gt;
--   instance <a>HFunctor</a> Action where ...
--   </pre>
deriveHFunctor :: Name -> Q [Dec]

-- | Derive the body of <a>hfmap</a>.
mkhfmap :: Name -> Q Exp


-- | Template Haskell functions to derive common type classes for testing
--   with quickcheck-state-machine.
module Test.StateMachine.TH

-- | Derive instances of <a>HFunctor</a>, <a>HFoldable</a>,
--   <a>HTraversable</a>, <a>Constructor</a>.
deriveTestClasses :: Name -> Q [Dec]

-- | Derive <a>HFunctor</a>, <a>HFoldable</a>, <a>HTraversable</a>.
deriveHClasses :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveHFunctor</a> ''Action
--   ===&gt;
--   instance <a>HFunctor</a> Action where ...
--   </pre>
deriveHFunctor :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveHFoldable</a> ''Action
--   ===&gt;
--   instance <a>HFoldable</a> Action where ...
--   </pre>
deriveHFoldable :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveHTraversable</a> ''Action
--   ===&gt;
--   instance <a>HTraversable</a> Action where ...
--   </pre>
deriveHTraversable :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveConstructors</a> ''Action
--   ===&gt;
--   instance <a>Constructors</a> Action where ...
--   </pre>
deriveConstructors :: Name -> Q [Dec]

-- | Given a name <tt>''Action</tt>, derive <a>Show</a> for <tt>(Action v
--   a)</tt> and <tt>(<a>Untyped</a> Action)</tt>. See <a>deriveShow</a>
--   and <a>deriveShowUntyped</a>.
deriveShows :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveShow</a> ''Action
--   ===&gt;
--   deriving instance <a>Show1</a> v =&gt; <a>Show</a> (Action v a)@.
--   </pre>
deriveShow :: Name -> Q [Dec]

-- | <pre>
--   <a>deriveShowUntyped</a> ''Action
--   ===&gt;
--   deriving instance <a>Show</a> (<a>Untyped</a> Action)
--   </pre>
deriveShowUntyped :: Name -> Q [Dec]

-- | <tt>$(<a>mkShrinker</a> ''Action)</tt> creates a generic shrinker of
--   type <tt>(Action v a -&gt; [Action v a])</tt> which ignores
--   <a>Reference</a> fields.
mkShrinker :: Name -> Q Exp


-- | This module contains environments that are used to translate between
--   symbolic and concrete references. It's taken verbatim from the
--   Hedgehog <a>library</a>.
module Test.StateMachine.Internal.Types.Environment

-- | A mapping of symbolic values to concrete values.
newtype Environment
Environment :: Map Var Dynamic -> Environment
[unEnvironment] :: Environment -> Map Var Dynamic

-- | Environment errors.
data EnvironmentError
EnvironmentValueNotFound :: !Var -> EnvironmentError
EnvironmentTypeError :: !TypeRep -> !TypeRep -> EnvironmentError

-- | Create an empty environment.
emptyEnvironment :: Environment

-- | Insert a symbolic / concrete pairing in to the environment.
insertConcrete :: Symbolic a -> Concrete a -> Environment -> Environment

-- | Cast a <a>Dynamic</a> in to a concrete value.
reifyDynamic :: forall a. Typeable a => Dynamic -> Either EnvironmentError (Concrete a)

-- | 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))

-- | Convert a symbolic structure to a concrete one, using the provided
--   environment.
reify :: HTraversable t => Environment -> t Symbolic b -> Either EnvironmentError (t Concrete b)
instance GHC.Show.Show Test.StateMachine.Internal.Types.Environment.EnvironmentError
instance GHC.Classes.Ord Test.StateMachine.Internal.Types.Environment.EnvironmentError
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.Environment.EnvironmentError
instance GHC.Show.Show Test.StateMachine.Internal.Types.Environment.Environment


-- | This module exports some types that are used internally by the
--   library.
module Test.StateMachine.Internal.Types

-- | A (sequential) program is an abstract datatype representing a list of
--   actions.
--   
--   The idea is that the user shows how to generate, shrink, execute and
--   modelcheck individual actions, and then the below combinators lift
--   those things to whole programs.
newtype Program act
Program :: [Internal act] -> Program act
[unProgram] :: Program act -> [Internal act]

-- | Returns the number of actions in a program.
programLength :: Program act -> Int

-- | A parallel program is an abstract datatype that represents three
--   sequences of actions; a sequential prefix and two parallel suffixes.
--   Analogous to the sequential case, the user shows how to generate,
--   shrink, execute and modelcheck individual actions, and then the below
--   combinators lift those things to whole parallel programs.
newtype ParallelProgram act
ParallelProgram :: Fork (Program act) -> ParallelProgram act
[unParallelProgram] :: ParallelProgram act -> Fork (Program act)

-- | A process id.
newtype Pid
Pid :: Int -> Pid

-- | Forks are used to represent parallel programs.
data Fork a
Fork :: a -> a -> a -> Fork a

-- | An internal action is an action together with the symbolic variable
--   that will hold its result.
data Internal (act :: (* -> *) -> * -> *)
[Internal] :: (Show resp, Typeable resp) => act Symbolic resp -> Symbolic resp -> Internal act
instance GHC.Show.Show Test.StateMachine.Internal.Types.Pid
instance GHC.Classes.Eq Test.StateMachine.Internal.Types.Pid
instance GHC.Read.Read a => GHC.Read.Read (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Base.Functor Test.StateMachine.Internal.Types.Fork
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Internal.Types.Fork a)
instance GHC.Show.Show (Test.StateMachine.Types.Untyped act) => GHC.Show.Show (Test.StateMachine.Internal.Types.Program act)
instance GHC.Read.Read (Test.StateMachine.Types.Untyped act) => GHC.Read.Read (Test.StateMachine.Internal.Types.Program act)
instance GHC.Show.Show (Test.StateMachine.Types.Untyped act) => GHC.Show.Show (Test.StateMachine.Internal.Types.ParallelProgram act)
instance GHC.Read.Read (Test.StateMachine.Types.Untyped act) => GHC.Read.Read (Test.StateMachine.Internal.Types.ParallelProgram act)
instance GHC.Classes.Eq (Test.StateMachine.Internal.Types.Internal act) => GHC.Classes.Eq (Test.StateMachine.Internal.Types.Program act)
instance GHC.Base.Monoid (Test.StateMachine.Internal.Types.Program act)
instance GHC.Classes.Eq (Test.StateMachine.Types.Untyped act) => GHC.Classes.Eq (Test.StateMachine.Internal.Types.Internal act)
instance GHC.Show.Show (Test.StateMachine.Types.Untyped act) => GHC.Show.Show (Test.StateMachine.Internal.Types.Internal act)
instance GHC.Read.Read (Test.StateMachine.Types.Untyped act) => GHC.Read.Read (Test.StateMachine.Internal.Types.Internal act)


-- | This module contains functions for visualing a history of a parallel
--   execution.
module Test.StateMachine.Internal.Utils.BoxDrawer

-- | Event invocation or response.
data EventType
Open :: EventType
Close :: EventType

-- | Given a history, and output from processes generate Doc with boxes
exec :: [(EventType, Pid)] -> Fork [String] -> Doc
instance GHC.Show.Show Test.StateMachine.Internal.Utils.BoxDrawer.EventType


-- | This module contains the notion of a history of an execution of a
--   (parallel) program.
module Test.StateMachine.Types.History

-- | A history is a trace of a program execution.
newtype History act err
History :: History' act err -> History act err
[unHistory] :: History act err -> History' act err

-- | A trace is a list of events.
type History' act err = [HistoryEvent (UntypedConcrete act) err]

-- | Pretty print a history.
ppHistory :: History act err -> String

-- | An event is either an invocation or a response.
data HistoryEvent act err
InvocationEvent :: act -> String -> Var -> Pid -> HistoryEvent act err
ResponseEvent :: (Result Dynamic err) -> String -> Pid -> HistoryEvent act err

-- | Get the process id of an event.
getProcessIdEvent :: HistoryEvent act err -> Pid

-- | Untyped concrete actions.
data UntypedConcrete (act :: (* -> *) -> * -> *)
[UntypedConcrete] :: (Show resp, Typeable resp) => act Concrete resp -> UntypedConcrete act

-- | An operation packs up an invocation event with its corresponding
--   response event.
data Operation act err
Operation :: (act Concrete resp) -> String -> (Result (Concrete resp) err) -> Pid -> Operation act err

-- | Given a history, return all possible interleavings of invocations and
--   corresponding response events.
linearTree :: History' act err -> [Tree (Operation act err)]
instance GHC.Base.Monoid (Test.StateMachine.Types.History.History act err)


-- | This module contains helpers for generating, shrinking, and checking
--   sequential programs.
module Test.StateMachine.Internal.Sequential

-- | Generate programs whose actions all respect their pre-conditions.
generateProgram :: forall model act. Generator model act -> Precondition model act -> Transition model act -> Int -> StateT (model Symbolic) Gen (Program act)

-- | Filter out invalid actions from a program. An action is invalid if
--   either its pre-condition doesn't hold, or it uses references that are
--   not in scope.
filterInvalid :: HFoldable act => Precondition model act -> Transition model act -> Program act -> State (model Symbolic, Set Var) (Program act)

-- | Returns the set of references an action uses.
getUsedVars :: HFoldable act => act Symbolic a -> Set Var

-- | Given a shrinker of typed actions we can lift it to a shrinker of
--   internal actions.
liftShrinkInternal :: Shrinker act -> (Internal act -> [Internal act])

-- | Shrink a program in a pre-condition and scope respecting way.
shrinkProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> Program act -> [Program act]

-- | Execute a program and return a history, the final model and a property
--   which contains the information of whether the execution respects the
--   state machine model or not.
executeProgram :: forall m act err model. Monad m => Show (Untyped act) => HTraversable act => StateMachine' model act err m -> Program act -> m (History act err, model Concrete, Property)


-- | This module provides scope-checking for internal actions. This
--   functionality isn't used anywhere in the library, but can be useful
--   for writing <a>metaproperties</a>.
module Test.StateMachine.Internal.ScopeCheck

-- | Scope-check a program, i.e. make sure that no action uses a reference
--   that doesn't exist.
scopeCheck :: forall act. HFoldable act => Program act -> Bool

-- | Same as above, but for parallel programs.
scopeCheckParallel :: HFoldable act => ParallelProgram act -> Bool


-- | This module contains helpers for generating, shrinking, and checking
--   parallel programs.
module Test.StateMachine.Internal.Parallel

-- | Generate a parallel program whose actions all respect their
--   pre-conditions.
generateParallelProgram :: Generator model act -> Precondition model act -> Transition model act -> model Symbolic -> Gen (ParallelProgram act)

-- | Shrink a parallel program in a pre-condition and scope respecting way.
shrinkParallelProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> (ParallelProgram act -> [ParallelProgram act])

-- | Run a parallel program, by first executing the prefix sequentially and
--   then the suffixes in parallel, and return the history (or trace) of
--   the execution.
executeParallelProgram :: forall m act err. MonadBaseControl IO m => HTraversable act => Show (Untyped act) => Semantics act err m -> ParallelProgram act -> m (History act err)

-- | Try to linearise a history of a parallel program execution using a
--   sequential model. See the *Linearizability: a correctness condition
--   for concurrent objects* paper linked to from the README for more info.
linearise :: forall model act err. Transition model act -> Postcondition model act -> InitialModel model -> History act err -> Property

-- | Draw an ASCII diagram of the history of a parallel program. Useful for
--   seeing how a race condition might have occured.
toBoxDrawings :: HFoldable act => ParallelProgram act -> History act err -> Doc


-- | This module provides &lt;math&gt;-equality for internal actions. This
--   functionality isn't used anywhere in the library, but can be useful
--   for writing <a>metaproperties</a>.
module Test.StateMachine.Internal.AlphaEquality

-- | Check if two lists of actions are equal modulo
--   &lt;math&gt;-conversion.
alphaEq :: (HFunctor act, Eq (Program act)) => Program act -> Program act -> Bool

-- | Check if two forks of actions are equal modulo
--   &lt;math&gt;-conversion.
alphaEqFork :: (HFunctor act, Eq (Program act)) => Fork (Program act) -> Fork (Program act) -> Bool


-- | The main module for state machine based testing, it contains
--   combinators that help you build sequential and parallel properties.
module Test.StateMachine

-- | A (sequential) program is an abstract datatype representing a list of
--   actions.
--   
--   The idea is that the user shows how to generate, shrink, execute and
--   modelcheck individual actions, and then the below combinators lift
--   those things to whole programs.
data Program act

-- | Returns the number of actions in a program.
programLength :: Program act -> Int

-- | This function is like a <a>forAllShrink</a> for sequential programs.
forAllProgram :: Show (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> InitialModel model -> (Program act -> Property) -> Property

-- | Wrapper around <a>forAllProgram</a> using the <a>StateMachine</a>
--   specification to generate and shrink sequential programs.
monadicSequential :: Monad m => Show (Untyped act) => HFoldable act => StateMachine' model act err m -> (Program act -> PropertyM m a) -> Property

-- | Testable property of sequential programs derived from a
--   <a>StateMachine</a> specification.
runProgram :: forall m act err model. Monad m => Show (Untyped act) => HTraversable act => StateMachine' model act err m -> Program act -> PropertyM m (History act err, model Concrete, Property)

-- | Takes the output of running a program and pretty prints a
--   counterexample if the run failed.
prettyProgram :: MonadIO m => Program act -> History act err -> model Concrete -> Property -> PropertyM m ()

-- | Returns the frequency of actions in a program.
actionNames :: forall act. Constructors act => Program act -> [(Constructor, Int)]

-- | Print distribution of actions and fail if some actions have not been
--   executed.
checkActionNames :: Constructors act => Program act -> Property -> Property

-- | A parallel program is an abstract datatype that represents three
--   sequences of actions; a sequential prefix and two parallel suffixes.
--   Analogous to the sequential case, the user shows how to generate,
--   shrink, execute and modelcheck individual actions, and then the below
--   combinators lift those things to whole parallel programs.
data ParallelProgram act

-- | This function is like a <a>forAllShrink</a> for parallel programs.
forAllParallelProgram :: Show (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> InitialModel model -> (ParallelProgram act -> Property) -> Property

-- | A history is a trace of a program execution.
data History act err

-- | Wrapper around <a>forAllParallelProgram</a> using the
--   <a>StateMachine</a> specification to generate and shrink parallel
--   programs.
monadicParallel :: MonadBaseControl IO m => Show (Untyped act) => HFoldable act => StateMachine' model act err m -> (ParallelProgram act -> PropertyM m ()) -> Property

-- | Testable property of parallel programs derived from a
--   <a>StateMachine</a> specification.
runParallelProgram :: MonadBaseControl IO m => Show (Untyped act) => HTraversable act => StateMachine' model act err m -> ParallelProgram act -> PropertyM m [(History act err, Property)]

-- | Same as above, but with the ability to choose how many times each
--   parallel program is executed. It can be important to tune this value
--   in order to reveal race conditions. The more runs, the more likely we
--   will find a bug, but it also takes longer.
runParallelProgram' :: MonadBaseControl IO m => Show (Untyped act) => HTraversable act => Int -> StateMachine' model act err m -> ParallelProgram act -> PropertyM m [(History act err, Property)]

-- | Takes the output of a parallel program runs and pretty prints a
--   counter example if any of the runs fail.
prettyParallelProgram :: MonadIO m => HFoldable act => ParallelProgram act -> [(History act err, Property)] -> PropertyM m ()

-- | Variant of <a>forAllProgram</a> which returns the generated and shrunk
--   program if the property fails.
forAllProgramC :: Show (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> InitialModel model -> (Program act -> PropertyOf a) -> PropertyOf (Program act :&: a)

-- | Variant of <a>monadicSequential</a> with counterexamples.
monadicSequentialC :: Monad m => Show (Untyped act) => HFoldable act => StateMachine' model act err m -> (Program act -> PropertyM m a) -> PropertyOf (Program act)

-- | Variant of <a>forAllParallelProgram</a> which returns the generated
--   and shrunk program if the property fails.
forAllParallelProgramC :: Show (Untyped act) => HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> InitialModel model -> (ParallelProgram act -> PropertyOf a) -> PropertyOf (ParallelProgram act :&: a)

-- | Variant of <a>monadicParallel</a> with counterexamples.
monadicParallelC :: MonadBaseControl IO m => Show (Untyped act) => HFoldable act => StateMachine' model act err m -> (ParallelProgram act -> PropertyM m ()) -> PropertyOf (ParallelProgram act)

-- | Tests a property and prints the results to <tt>stdout</tt>.
quickCheck :: Testable prop => prop -> IO ()