-- 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.3.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, Show a, Show b) => Fun a b -> a -> b
(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a 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 m Void

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

-- | Same as above, but with possibly failing semantics.
data StateMachine' model act m err
StateMachine :: Generator model act -> Shrinker act -> Precondition model act -> Transition' model act err -> Postcondition' model act err -> InitialModel model -> Semantics' act m err -> Runner m -> StateMachine' model act m err
[generator'] :: StateMachine' model act m err -> Generator model act
[shrinker'] :: StateMachine' model act m err -> Shrinker act
[precondition'] :: StateMachine' model act m err -> Precondition model act
[transition'] :: StateMachine' model act m err -> Transition' model act err
[postcondition'] :: StateMachine' model act m err -> Postcondition' model act err
[model'] :: StateMachine' model act m err -> InitialModel model
[semantics'] :: StateMachine' model act m err -> Semantics' act m err
[runner'] :: StateMachine' model act m err -> 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, Show1 v) => model v -> act v resp -> v resp -> model v
type Transition' model act err = forall resp v. (Ord1 v, Show1 v) => model v -> act v resp -> Result err (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 -> Bool
type Postcondition' model act err = forall resp. model Concrete -> act Concrete resp -> Result err resp -> Bool

-- | 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 err resp
Success :: resp -> Result err resp
Fail :: err -> Result err resp
ppResult :: (Show err, Show resp) => Result err resp -> String

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

-- | How to run the monad used by the semantics.
type Runner m = m Property -> IO Property
data Reason
Ok :: Reason
PreconditionFailed :: Reason
PostconditionFailed :: Reason
instance GHC.Show.Show Test.StateMachine.Types.Reason
instance GHC.Classes.Eq Test.StateMachine.Types.Reason
instance GHC.Base.Functor (Test.StateMachine.Types.Result err)


-- | This module provides a propositional logic which gives counterexamples
--   when the proposition is false.
module Test.StateMachine.Logic
data Logic
Bot :: Logic
Top :: Logic
(:&&) :: Logic -> Logic -> Logic
(:||) :: Logic -> Logic -> Logic
(:=>) :: Logic -> Logic -> Logic
Not :: Logic -> Logic
Predicate :: Predicate -> Logic
Annotate :: String -> Logic -> Logic
data Predicate
(:==) :: a -> a -> Predicate
(:/=) :: a -> a -> Predicate
(:<) :: a -> a -> Predicate
(:<=) :: a -> a -> Predicate
(:>) :: a -> a -> Predicate
(:>=) :: a -> a -> Predicate
Elem :: a -> [a] -> Predicate
NotElem :: a -> [a] -> Predicate
dual :: Predicate -> Predicate
strongNeg :: Logic -> Logic
data Counterexample
BotC :: Counterexample
Fst :: Counterexample -> Counterexample
Snd :: Counterexample -> Counterexample
EitherC :: Counterexample -> Counterexample -> Counterexample
ImpliesC :: Counterexample -> Counterexample
NotC :: Counterexample -> Counterexample
PredicateC :: Predicate -> Counterexample
AnnotateC :: String -> Counterexample -> Counterexample
data Value
VFalse :: Counterexample -> Value
VTrue :: Value
logic :: Logic -> Value
predicate :: Predicate -> Value
instance GHC.Show.Show Test.StateMachine.Logic.Value
instance GHC.Show.Show Test.StateMachine.Logic.Counterexample
instance GHC.Show.Show Test.StateMachine.Logic.Logic
instance GHC.Show.Show Test.StateMachine.Logic.Predicate


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

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

-- | A variant of <a>forAllShrink</a> with an explicit show function.
forAllShrinkShow :: Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShowC :: Testable prop => Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> PropertyOf (a :&: Counterexample prop)

-- | 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
getChanContents :: TChan a -> IO [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>, and <a>Show1</a>
--   <tt>(Action Symbolic)</tt>. See <a>deriveShow</a>,
--   <a>deriveShowUntyped</a>, and <a>deriveShow1</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>, and <a>Show1</a>
--   <tt>(Action Symbolic)</tt>. See <a>deriveShow</a>,
--   <a>deriveShowUntyped</a>, and <a>deriveShow1</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
data ParallelProgram act
ParallelProgram :: (Program act) -> [(Program act, Program act)] -> ParallelProgram act
parallelProgramLength :: ParallelProgram act -> Int
parallelProgramToList :: [(Program act, Program act)] -> [Program act]
parallelProgramFromList :: [Program act] -> [(Program act, Program act)]
parallelProgramAsList :: ([Program act] -> [Program act]) -> [(Program act, Program act)] -> [(Program act, Program act)]
flattenParallelProgram :: ParallelProgram act -> Program act

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

-- | 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.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.Classes.Eq (Test.StateMachine.Types.Untyped act) => GHC.Classes.Eq (Test.StateMachine.Internal.Types.ParallelProgram 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
data Fork a
Fork :: a -> a -> a -> Fork a

-- | Given a history, and output from processes generate Doc with boxes
exec :: [(EventType, Pid)] -> Fork [String] -> Doc
instance GHC.Base.Functor Test.StateMachine.Internal.Utils.BoxDrawer.Fork
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 :: forall model act err. Show (model Concrete) => Show err => model Concrete -> Transition' model act err -> 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 err Dynamic) -> 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 err resp) -> String -> 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 err. Generator model act -> Precondition model act -> Transition' model act err -> Int -> StateT (model Symbolic) Gen (Program act)
generateProgram' :: Generator model act -> Precondition model act -> Transition' model act err -> 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 err -> 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])
validProgram :: forall act model err. HFoldable act => Precondition model act -> Transition' model act err -> model Symbolic -> Program act -> Bool

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

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


-- | 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 err -> model Symbolic -> Gen (ParallelProgram act)

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

-- | 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 => Show1 (act Symbolic) => Semantics' act m err -> 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 err -> Postcondition' model act err -> 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


-- | 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 <tt>forAllShrink</tt> for sequential programs.
forAllProgram :: HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition' model act err -> 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 => HFoldable act => Testable a => StateMachine' model act m err -> (Program act -> PropertyM m a) -> Property

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

-- | Takes the output of running a program and pretty prints a
--   counterexample if the run failed.
prettyProgram :: MonadIO m => Show (model Concrete) => Show err => StateMachine' model act m err -> History act err -> 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
data ParallelProgram act

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

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

-- | Testable property of parallel programs derived from a
--   <a>StateMachine</a> specification.
runParallelProgram :: MonadBaseControl IO m => Show1 (act Symbolic) => HTraversable act => StateMachine' model act m err -> ParallelProgram act -> PropertyM m [(History act err, Property)]
runParallelProgram' :: MonadBaseControl IO m => Show1 (act Symbolic) => HTraversable act => Int -> StateMachine' model act m err -> 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 => Show (Untyped 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 :: HFoldable act => Generator model act -> Shrinker act -> Precondition model act -> Transition' model act err -> InitialModel model -> (Program act -> PropertyOf a) -> PropertyOf (Program act :&: a)

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

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

-- | Tests a property and prints the results to <tt>stdout</tt>.
--   
--   By default up to 100 tests are performed, which may not be enough to
--   find all bugs. To run more tests, use <a>withMaxSuccess</a>.
quickCheck :: Testable prop => prop -> IO ()