-- 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/stevana/quickcheck-state-machine#readme</a>
@package quickcheck-state-machine
@version 0.7.3

module Test.StateMachine.Lockstep.Auxiliary
data Elem (xs :: [k]) (a :: k)
[ElemHead] :: Elem (k : ks) k
[ElemTail] :: Elem ks k -> Elem (k' : ks) k
npAt :: NP f xs -> Elem xs a -> f a

-- | N-ary traversable functors
--   
--   TODO: Don't provide Elem explicitly (just instantiate <tt>c</tt>)?
--   TODO: Introduce HTraverse into SOP?
class NTraversable (f :: (k -> Type) -> [k] -> Type)
nctraverse :: (NTraversable f, Applicative m, All c xs) => proxy c -> (forall a. c a => Elem xs a -> g a -> m (h a)) -> f g xs -> m (f h xs)
ntraverse :: (NTraversable f, Applicative m, SListI xs) => (forall a. Elem xs a -> g a -> m (h a)) -> f g xs -> m (f h xs)
ncfmap :: (NTraversable f, All c xs) => proxy c -> (forall a. c a => Elem xs a -> g a -> h a) -> f g xs -> f h xs
nfmap :: (NTraversable f, SListI xs) => (forall a. Elem xs a -> g a -> h a) -> f g xs -> f h xs
ncfoldMap :: forall proxy f g m c xs. (NTraversable f, Monoid m, All c xs) => proxy c -> (forall a. c a => Elem xs a -> g a -> m) -> f g xs -> m
nfoldMap :: (NTraversable f, Monoid m, SListI xs) => (forall a. Elem xs a -> g a -> m) -> f g xs -> m


-- | This module defines a predicate logic-like language and its
--   counterexample semantics.
module Test.StateMachine.Logic
data Logic
Bot :: Logic
Top :: Logic
(:&&) :: Logic -> Logic -> Logic
(:||) :: Logic -> Logic -> Logic
(:=>) :: Logic -> Logic -> Logic
Not :: Logic -> Logic
LogicPredicate :: LogicPredicate -> Logic
Forall :: [a] -> (a -> Logic) -> Logic
Exists :: [a] -> (a -> Logic) -> Logic
Boolean :: Bool -> Logic
Annotate :: String -> Logic -> Logic
data LogicPredicate
(:==) :: a -> a -> LogicPredicate
(:/=) :: a -> a -> LogicPredicate
(:<) :: a -> a -> LogicPredicate
(:<=) :: a -> a -> LogicPredicate
(:>) :: a -> a -> LogicPredicate
(:>=) :: a -> a -> LogicPredicate
Member :: a -> t a -> LogicPredicate
NotMember :: a -> t a -> LogicPredicate
dual :: LogicPredicate -> LogicPredicate
strongNeg :: Logic -> Logic
data Counterexample
BotC :: Counterexample
Fst :: Counterexample -> Counterexample
Snd :: Counterexample -> Counterexample
EitherC :: Counterexample -> Counterexample -> Counterexample
ImpliesC :: Counterexample -> Counterexample
NotC :: Counterexample -> Counterexample
PredicateC :: LogicPredicate -> Counterexample
ForallC :: a -> Counterexample -> Counterexample
ExistsC :: [a] -> [Counterexample] -> Counterexample
BooleanC :: Counterexample
AnnotateC :: String -> Counterexample -> Counterexample
data Value
VFalse :: Counterexample -> Value
VTrue :: Value
boolean :: Logic -> Bool
logic :: Logic -> Value
evalLogicPredicate :: LogicPredicate -> Value

-- | Gather user annotations of a true logic expression.
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations (Top .// "top")
--   ["top"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations ((Bot .// "bot") .|| (Top .// "top"))
--   ["top"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations (Top .// "top1" .&amp;&amp; Top .// "top2")
--   ["top1","top2"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations (Bot .// "bot" .&amp;&amp; Top .// "top")
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations (forall [1,2,3] (\i -&gt; 0 .&lt; i .// "positive"))
--   ["positive","positive","positive"]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations (forall [0,1,2,3] (\i -&gt; 0 .&lt; i .// "positive"))
--   []
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; gatherAnnotations (exists [1,2,3] (\i -&gt; 0 .&lt; i .// "positive"))
--   ["positive"]
--   </pre>
gatherAnnotations :: Logic -> [String]
(.==) :: (Eq a, Show a) => a -> a -> Logic
infix 5 .==
(./=) :: (Eq a, Show a) => a -> a -> Logic
infix 5 ./=
(.<) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .<
(.<=) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .<=
(.>) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .>
(.>=) :: (Ord a, Show a) => a -> a -> Logic
infix 5 .>=
member :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
infix 8 `member`
notMember :: (Foldable t, Eq a, Show a, Show (t a)) => a -> t a -> Logic
infix 8 `notMember`
(.//) :: Logic -> String -> Logic
infixl 4 .//
(.&&) :: Logic -> Logic -> Logic
infixr 3 .&&
(.||) :: Logic -> Logic -> Logic
infixr 2 .||
(.=>) :: Logic -> Logic -> Logic
infixr 1 .=>
forall :: Show a => [a] -> (a -> Logic) -> Logic
exists :: Show a => [a] -> (a -> Logic) -> Logic
instance GHC.Show.Show Test.StateMachine.Logic.Value
instance GHC.Show.Show Test.StateMachine.Logic.LogicPredicate
instance GHC.Show.Show Test.StateMachine.Logic.Counterexample

module Test.StateMachine.Types.Rank2
class Functor (f :: (k -> Type) -> Type)
fmap :: Functor f => (forall x. p x -> q x) -> f p -> f q
gfmap :: (Generic1 f, Functor (Rep1 f)) => (forall a. p a -> q a) -> f p -> f q
(<$>) :: Functor f => (forall x. p x -> q x) -> f p -> f q
class Foldable (f :: (k -> Type) -> Type)
foldMap :: (Foldable f, Monoid m) => (forall x. p x -> m) -> f p -> m
gfoldMap :: (Generic1 f, Foldable (Rep1 f), Monoid m) => (forall a. p a -> m) -> f p -> m
class (Functor t, Foldable t) => Traversable (t :: (k -> Type) -> Type)
traverse :: (Traversable t, Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q)
gtraverse :: (Generic1 t, Traversable (Rep1 t), Applicative f) => (forall a. p a -> f (q a)) -> t p -> f (t q)
instance Test.StateMachine.Types.Rank2.Traversable GHC.Generics.U1
instance Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.K1 i c)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:+: g)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:*: g)
instance forall k (f :: * -> *) (g :: (k -> *) -> *). (Data.Traversable.Traversable f, Test.StateMachine.Types.Rank2.Traversable g) => Test.StateMachine.Types.Rank2.Traversable (f GHC.Generics.:.: g)
instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Traversable f => Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.M1 i c f)
instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Traversable f => Test.StateMachine.Types.Rank2.Traversable (GHC.Generics.Rec1 f)
instance Test.StateMachine.Types.Rank2.Foldable GHC.Generics.U1
instance Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.K1 i c)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:+: g)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:*: g)
instance forall k (f :: * -> *) (g :: (k -> *) -> *). (Data.Foldable.Foldable f, Test.StateMachine.Types.Rank2.Foldable g) => Test.StateMachine.Types.Rank2.Foldable (f GHC.Generics.:.: g)
instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Foldable f => Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.M1 i c f)
instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Foldable f => Test.StateMachine.Types.Rank2.Foldable (GHC.Generics.Rec1 f)
instance Test.StateMachine.Types.Rank2.Functor GHC.Generics.U1
instance Test.StateMachine.Types.Rank2.Functor (GHC.Generics.K1 i c)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:+: g)
instance forall k (f :: (k -> *) -> *) (g :: (k -> *) -> *). (Test.StateMachine.Types.Rank2.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:*: g)
instance forall k (f :: * -> *) (g :: (k -> *) -> *). (GHC.Base.Functor f, Test.StateMachine.Types.Rank2.Functor g) => Test.StateMachine.Types.Rank2.Functor (f GHC.Generics.:.: g)
instance forall k (f :: (k -> *) -> *) i (c :: GHC.Generics.Meta). Test.StateMachine.Types.Rank2.Functor f => Test.StateMachine.Types.Rank2.Functor (GHC.Generics.M1 i c f)
instance forall k (f :: (k -> *) -> *). Test.StateMachine.Types.Rank2.Functor f => Test.StateMachine.Types.Rank2.Functor (GHC.Generics.Rec1 f)


-- | This module contains reference related types. It's taken almost
--   verbatim from the Hedgehog <a>library</a>.
module Test.StateMachine.Types.References
newtype Var
Var :: Int -> Var
data Symbolic a
[Symbolic] :: Typeable a => Var -> Symbolic a
data Concrete a
[Concrete] :: Typeable a => a -> Concrete a
newtype Reference a r
Reference :: r a -> Reference a r
reference :: Typeable a => a -> Reference a Concrete
concrete :: Reference a Concrete -> a
opaque :: Reference (Opaque a) Concrete -> a
newtype Opaque a
Opaque :: a -> Opaque a
unOpaque :: Opaque a -> a
instance Data.TreeDiff.Class.ToExpr Test.StateMachine.Types.References.Var
instance GHC.Read.Read Test.StateMachine.Types.References.Var
instance GHC.Generics.Generic 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.Generics.Generic (Test.StateMachine.Types.References.Reference a r)
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.Show.Show (Test.StateMachine.Types.References.Symbolic a)
instance Data.Typeable.Internal.Typeable a => GHC.Read.Read (Test.StateMachine.Types.References.Symbolic 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 a => GHC.Show.Show (Test.StateMachine.Types.References.Concrete a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.References.Concrete a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.References.Concrete a)
instance Data.Typeable.Internal.Typeable a => GHC.Read.Read (Test.StateMachine.Types.References.Reference a Test.StateMachine.Types.References.Symbolic)
instance GHC.Show.Show (Test.StateMachine.Types.References.Opaque a)
instance Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Opaque a)
instance Data.TreeDiff.Class.ToExpr (r a) => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Reference a r)
instance Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Types.References.Reference a)
instance Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Types.References.Reference a)
instance Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Types.References.Reference a)
instance (GHC.Classes.Eq a, Data.Functor.Classes.Eq1 r) => GHC.Classes.Eq (Test.StateMachine.Types.References.Reference a r)
instance (GHC.Classes.Ord a, Data.Functor.Classes.Ord1 r) => GHC.Classes.Ord (Test.StateMachine.Types.References.Reference a r)
instance (Data.Functor.Classes.Show1 r, GHC.Show.Show a) => GHC.Show.Show (Test.StateMachine.Types.References.Reference a r)
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Concrete
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Concrete
instance Data.TreeDiff.Class.ToExpr a => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Concrete a)
instance Data.Functor.Classes.Show1 Test.StateMachine.Types.References.Symbolic
instance Data.TreeDiff.Class.ToExpr a => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Types.References.Symbolic a)
instance Data.Functor.Classes.Eq1 Test.StateMachine.Types.References.Symbolic
instance Data.Functor.Classes.Ord1 Test.StateMachine.Types.References.Symbolic


-- | This module contains the notion of a history of an execution of a
--   (parallel) program.
module Test.StateMachine.Types.History
newtype History cmd resp
History :: History' cmd resp -> History cmd resp
[unHistory] :: History cmd resp -> History' cmd resp
type History' cmd resp = [(Pid, HistoryEvent cmd resp)]
newtype Pid
Pid :: Int -> Pid
[unPid] :: Pid -> Int
data HistoryEvent cmd resp
Invocation :: !cmd Concrete -> !Set Var -> HistoryEvent cmd resp
Response :: !resp Concrete -> HistoryEvent cmd resp
Exception :: !String -> HistoryEvent cmd resp

-- | An operation packs up an invocation event with its corresponding
--   response event.
data Operation cmd resp
Operation :: cmd Concrete -> resp Concrete -> Pid -> Operation cmd resp
Crash :: cmd Concrete -> String -> Pid -> Operation cmd resp

-- | Given a sequential history, group invocation and response events into
--   operations.
makeOperations :: History' cmd resp -> [Operation cmd resp]

-- | Given a parallel history, return all possible interleavings of
--   invocations and corresponding response events.
interleavings :: History' cmd resp -> Forest (Operation cmd resp)
operationsPath :: Forest (Operation cmd resp) -> [Operation cmd resp]
completeHistory :: (cmd Concrete -> resp Concrete) -> History cmd resp -> History cmd resp
instance GHC.Classes.Ord Test.StateMachine.Types.History.Pid
instance GHC.Show.Show Test.StateMachine.Types.History.Pid
instance GHC.Classes.Eq Test.StateMachine.Types.History.Pid
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Concrete), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Concrete)) => GHC.Classes.Eq (Test.StateMachine.Types.History.History cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.History cmd resp)
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Concrete), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Concrete)) => GHC.Classes.Eq (Test.StateMachine.Types.History.HistoryEvent cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.HistoryEvent cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Concrete), GHC.Show.Show (resp Test.StateMachine.Types.References.Concrete)) => GHC.Show.Show (Test.StateMachine.Types.History.Operation cmd resp)

module Test.StateMachine.DotDrawing
data GraphOptions
GraphOptions :: FilePath -> GraphvizOutput -> GraphOptions
[filePath] :: GraphOptions -> FilePath
[graphvizOutput] :: GraphOptions -> GraphvizOutput

-- | The possible Graphviz output formats (that is, those that actually
--   produce a file).
data GraphvizOutput

-- | Windows Bitmap Format.
Bmp :: GraphvizOutput

-- | Pretty-printed Dot output with no layout performed.
Canon :: GraphvizOutput

-- | Reproduces the input along with layout information.
DotOutput :: GraphvizOutput

-- | As with <a>DotOutput</a>, but provides even more information on how
--   the graph is drawn. The optional <a>Version</a> is the same as
--   specifying the <tt>XDotVersion</tt> attribute.
XDot :: Maybe Version -> GraphvizOutput

-- | Encapsulated PostScript.
Eps :: GraphvizOutput

-- | FIG graphics language.
Fig :: GraphvizOutput

-- | Internal GD library format.
Gd :: GraphvizOutput

-- | Compressed version of <a>Gd</a>.
Gd2 :: GraphvizOutput

-- | Graphics Interchange Format.
Gif :: GraphvizOutput

-- | Icon image file format.
Ico :: GraphvizOutput

-- | Server-side imagemap.
Imap :: GraphvizOutput

-- | Client-side imagemap.
Cmapx :: GraphvizOutput

-- | As for <a>Imap</a>, except only rectangles are used as active areas.
ImapNP :: GraphvizOutput

-- | As for <a>Cmapx</a>, except only rectangles are used as active areas.
CmapxNP :: GraphvizOutput

-- | The JPEG image format.
Jpeg :: GraphvizOutput

-- | Portable Document Format.
Pdf :: GraphvizOutput

-- | Simple text format.
Plain :: GraphvizOutput

-- | As for <a>Plain</a>, but provides port names on head and tail nodes
--   when applicable.
PlainExt :: GraphvizOutput

-- | Portable Network Graphics format.
Png :: GraphvizOutput

-- | PostScript.
Ps :: GraphvizOutput

-- | PostScript for PDF.
Ps2 :: GraphvizOutput

-- | Scalable Vector Graphics format.
Svg :: GraphvizOutput

-- | Compressed SVG format.
SvgZ :: GraphvizOutput

-- | Tagged Image File Format.
Tiff :: GraphvizOutput

-- | Vector Markup Language; <a>Svg</a> is usually preferred.
Vml :: GraphvizOutput

-- | Compressed VML format; <a>SvgZ</a> is usually preferred.
VmlZ :: GraphvizOutput

-- | Virtual Reality Modeling Language format; requires nodes to have a
--   third dimension set via the <tt>Pos</tt> attribute (and with a
--   <tt>Dim</tt> value of at least <tt>3</tt>).
Vrml :: GraphvizOutput

-- | Wireless BitMap format; monochrome format usually used for mobile
--   computing devices.
WBmp :: GraphvizOutput

-- | Google's WebP format; requires Graphviz &gt;= 2.29.0.
WebP :: GraphvizOutput
data Rose a
Rose :: a -> Map Pid a -> Rose a
printDotGraph :: GraphOptions -> Rose [String] -> IO ()
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.DotDrawing.Rose a)
instance GHC.Base.Functor Test.StateMachine.DotDrawing.Rose


module Test.StateMachine.Types.GenSym
data GenSym a
runGenSym :: GenSym a -> Counter -> (a, Counter)
genSym :: Typeable a => GenSym (Reference a Symbolic)
data Counter
newCounter :: Counter
instance GHC.Show.Show Test.StateMachine.Types.GenSym.Counter
instance GHC.Base.Monad Test.StateMachine.Types.GenSym.GenSym
instance GHC.Base.Applicative Test.StateMachine.Types.GenSym.GenSym
instance GHC.Base.Functor Test.StateMachine.Types.GenSym.GenSym


-- | This module contains environments that are used to translate between
--   symbolic and concrete references. It's taken from the Hedgehog
--   <a>library</a>.
module Test.StateMachine.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 :: Var -> Dynamic -> Environment -> Environment
insertConcretes :: [Var] -> [Dynamic] -> 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 :: Traversable t => Environment -> t Symbolic -> Either EnvironmentError (t Concrete)
instance GHC.Base.Monoid Test.StateMachine.Types.Environment.Environment
instance GHC.Base.Semigroup Test.StateMachine.Types.Environment.Environment
instance GHC.Show.Show Test.StateMachine.Types.Environment.Environment
instance GHC.Show.Show Test.StateMachine.Types.Environment.EnvironmentError
instance GHC.Classes.Ord Test.StateMachine.Types.Environment.EnvironmentError
instance GHC.Classes.Eq Test.StateMachine.Types.Environment.EnvironmentError


module Test.StateMachine.Types
data StateMachine model cmd m resp
StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Maybe (Gen (cmd Symbolic))) -> (model Symbolic -> cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> (model Concrete -> m ()) -> StateMachine model cmd m resp
[initModel] :: StateMachine model cmd m resp -> forall r. model r
[transition] :: StateMachine model cmd m resp -> forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r
[precondition] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> Logic
[postcondition] :: StateMachine model cmd m resp -> model Concrete -> cmd Concrete -> resp Concrete -> Logic
[invariant] :: StateMachine model cmd m resp -> Maybe (model Concrete -> Logic)
[generator] :: StateMachine model cmd m resp -> model Symbolic -> Maybe (Gen (cmd Symbolic))
[shrinker] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> [cmd Symbolic]
[semantics] :: StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
[mock] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
[cleanup] :: StateMachine model cmd m resp -> model Concrete -> m ()

-- | Previously symbolically executed command
--   
--   Invariant: the variables must be the variables in the response.
data Command cmd resp
Command :: !cmd Symbolic -> !resp Symbolic -> ![Var] -> Command cmd resp
getCommand :: Command cmd resp -> cmd Symbolic
newtype Commands cmd resp
Commands :: [Command cmd resp] -> Commands cmd resp
[unCommands] :: Commands cmd resp -> [Command cmd resp]
type NParallelCommands = ParallelCommandsF []
lengthCommands :: Commands cmd resp -> Int
data ParallelCommandsF t cmd resp
ParallelCommands :: !Commands cmd resp -> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
[prefix] :: ParallelCommandsF t cmd resp -> !Commands cmd resp
[suffixes] :: ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
type ParallelCommands = ParallelCommandsF Pair
data Pair a
Pair :: !a -> !a -> Pair a
[proj1] :: Pair a -> !a
[proj2] :: Pair a -> !a
fromPair :: Pair a -> (a, a)
toPair :: (a, a) -> Pair a
fromPair' :: ParallelCommandsF Pair cmd resp -> ParallelCommandsF [] cmd resp
toPairUnsafe' :: ParallelCommandsF [] cmd resp -> ParallelCommandsF Pair cmd resp
data Reason
Ok :: Reason
PreconditionFailed :: String -> Reason
PostconditionFailed :: String -> Reason
InvariantBroken :: String -> Reason
ExceptionThrown :: String -> Reason
MockSemanticsMismatch :: String -> Reason
isOK :: Reason -> Bool
noCleanup :: Monad m => model Concrete -> m ()
instance GHC.Base.Monoid (Test.StateMachine.Types.Commands cmd resp)
instance GHC.Base.Semigroup (Test.StateMachine.Types.Commands cmd resp)
instance GHC.Show.Show Test.StateMachine.Types.Reason
instance GHC.Classes.Eq Test.StateMachine.Types.Reason
instance Data.Traversable.Traversable Test.StateMachine.Types.Pair
instance Data.Foldable.Foldable Test.StateMachine.Types.Pair
instance GHC.Base.Functor Test.StateMachine.Types.Pair
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Types.Pair a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Test.StateMachine.Types.Pair a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Types.Pair a)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Show.Show (Test.StateMachine.Types.Command cmd resp)
instance (GHC.Read.Read (cmd Test.StateMachine.Types.References.Symbolic), GHC.Read.Read (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Read.Read (Test.StateMachine.Types.Command cmd resp)
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Classes.Eq (Test.StateMachine.Types.Command cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Show.Show (Test.StateMachine.Types.Commands cmd resp)
instance (GHC.Read.Read (cmd Test.StateMachine.Types.References.Symbolic), GHC.Read.Read (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Read.Read (Test.StateMachine.Types.Commands cmd resp)
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Symbolic)) => GHC.Classes.Eq (Test.StateMachine.Types.Commands cmd resp)
instance (GHC.Classes.Eq (cmd Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (resp Test.StateMachine.Types.References.Symbolic), GHC.Classes.Eq (t (Test.StateMachine.Types.Commands cmd resp))) => GHC.Classes.Eq (Test.StateMachine.Types.ParallelCommandsF t cmd resp)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (resp Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (t (Test.StateMachine.Types.Commands cmd resp))) => GHC.Show.Show (Test.StateMachine.Types.ParallelCommandsF t cmd resp)


-- | This module exports helpers that are useful for labelling properties.
module Test.StateMachine.Labelling
data Predicate a b
Predicate :: (a -> Either b (Predicate a b)) -> Maybe b -> Predicate a b

-- | Given an <tt>a</tt>, either successfully classify as <tt>b</tt> or
--   continue looking
[predApply] :: Predicate a b -> a -> Either b (Predicate a b)

-- | End of the string
--   
--   The predicate is given a final chance to return a value.
[predFinish] :: Predicate a b -> Maybe b

-- | Construct simply predicate that returns <a>Nothing</a> on termination
predicate :: (a -> Either b (Predicate a b)) -> Predicate a b

-- | Maximum value found, if any
maximum :: forall a b. Ord b => (a -> Maybe b) -> Predicate a b

-- | Do a linear scan over the list, returning all successful
--   classifications
classify :: forall a b. [Predicate a b] -> [a] -> [b]
data Event model cmd resp (r :: Type -> Type)
Event :: model r -> cmd r -> model r -> resp r -> Event model cmd resp (r :: Type -> Type)
[eventBefore] :: Event model cmd resp (r :: Type -> Type) -> model r
[eventCmd] :: Event model cmd resp (r :: Type -> Type) -> cmd r
[eventAfter] :: Event model cmd resp (r :: Type -> Type) -> model r
[eventResp] :: Event model cmd resp (r :: Type -> Type) -> resp r

-- | <a>execCmds</a> is just the repeated form of <a>execCmd</a>.
execCmds :: forall model cmd m resp. StateMachine model cmd m resp -> Commands cmd resp -> [Event model cmd resp Symbolic]
execHistory :: forall model cmd m resp. StateMachine model cmd m resp -> History cmd resp -> [Event model cmd resp Concrete]
instance (GHC.Show.Show (model r), GHC.Show.Show (cmd r), GHC.Show.Show (resp r)) => GHC.Show.Show (Test.StateMachine.Labelling.Event model cmd resp r)
instance GHC.Base.Functor (Test.StateMachine.Labelling.Predicate a)

module Test.StateMachine.ConstructorName

-- | The names of all possible commands
--   
--   This is used for things like tagging, coverage checking, etc.
class CommandNames (cmd :: k -> Type)

-- | Name of this particular command
cmdName :: CommandNames cmd => cmd r -> String

-- | Name of all possible commands
cmdNames :: CommandNames cmd => Proxy (cmd r) -> [String]

-- | Name of this particular command
cmdName :: (CommandNames cmd, Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String

-- | Name of all possible commands
cmdNames :: forall r. (CommandNames cmd, CommandNames (Rep1 cmd)) => Proxy (cmd r) -> [String]

-- | Convenience wrapper for <a>Command</a>
commandName :: CommandNames cmd => Command cmd resp -> String
instance Test.StateMachine.ConstructorName.CommandNames GHC.Generics.U1
instance Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.K1 i c)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *). GHC.Generics.Constructor c => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.C c f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.D c f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.M1 GHC.Generics.S c f)
instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.CommandNames f, Test.StateMachine.ConstructorName.CommandNames g) => Test.StateMachine.ConstructorName.CommandNames (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.CommandNames f, Test.StateMachine.ConstructorName.CommandNames g) => Test.StateMachine.ConstructorName.CommandNames (f GHC.Generics.:*: g)
instance forall k (f :: k -> *). Test.StateMachine.ConstructorName.CommandNames f => Test.StateMachine.ConstructorName.CommandNames (GHC.Generics.Rec1 f)


-- | This module contains functions for visualing a history of a parallel
--   execution.
module Test.StateMachine.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.Show.Show Test.StateMachine.BoxDrawer.EventType
instance GHC.Base.Functor Test.StateMachine.BoxDrawer.Fork


-- | This module contains helper functions for testing using Markov chains.
module Test.StateMachine.Markov

-- | Markov chain.
data Markov state cmd_ prob

-- | Constructor for <a>Markov</a> chains.
makeMarkov :: Ord state => [Map state [Transition state cmd_ prob]] -> Markov state cmd_ prob

-- | Expose inner graph structure of markov chain
toAdjacencyMap :: Ord state => Markov state cmd_ prob -> Map state (Map state (cmd_, prob))

-- | Infix operator for starting to creating a transition in the
--   <a>Markov</a> chain, finish the transition with one of <a>(&gt;-)</a>
--   or <a>(/-)</a> depending on whether the transition has a specific or a
--   uniform probability.
(-<) :: Fractional prob => state -> [Either (cmd_, state) ((cmd_, prob), state)] -> Map state [Transition state cmd_ prob]
infixl 5 -<

-- | Finish making a transition with a specified probability distribution.
(>-) :: (cmd_, prob) -> state -> Either (cmd_, state) ((cmd_, prob), state)
infixl 5 >-

-- | Finish making a transition with an uniform probability distribution.
(/-) :: cmd_ -> state -> Either (cmd_, state) ((cmd_, prob), state)
infixl 5 /-

-- | Create a generator from a <a>Markov</a> chain.
markovGenerator :: forall state cmd_ cmd model. (Show state, Show cmd_) => (Ord state, Ord cmd_) => Markov state cmd_ Double -> Map cmd_ (model Symbolic -> Gen (cmd Symbolic)) -> (model Symbolic -> state) -> (state -> Bool) -> model Symbolic -> Maybe (Gen (cmd Symbolic))

-- | Variant of QuickCheck's <a>coverTable</a> which works on <a>Markov</a>
--   chains.
coverMarkov :: (Show state, Show cmd_, Testable prop) => Markov state cmd_ Double -> prop -> Property

-- | Variant of QuickCheck's <a>tabulate</a> which works for <a>Markov</a>
--   chains.
tabulateMarkov :: forall model state cmd cmd_ m resp prop. Testable prop => (Show state, Show cmd_) => StateMachine model cmd m resp -> (model Symbolic -> state) -> (cmd Symbolic -> cmd_) -> Commands cmd resp -> prop -> Property
transitionMatrix :: forall state cmd_. Ord state => (Generic state, GEnum FiniteEnum (Rep state), GBounded (Rep state)) => Markov state cmd_ Double -> Matrix Double
stimulusMatrix :: forall state cmd. (Ord state, Ord cmd) => (Generic state, GEnum FiniteEnum (Rep state), GBounded (Rep state)) => (Generic cmd, GEnum FiniteEnum (Rep cmd), GBounded (Rep cmd)) => Markov state cmd Double -> Matrix Double
historyObservations :: forall model cmd m resp state cmd_ prob. Ord state => Ord cmd_ => (Generic state, GEnum FiniteEnum (Rep state), GBounded (Rep state)) => StateMachine model cmd m resp -> Markov state cmd_ prob -> (model Concrete -> state) -> (cmd Concrete -> cmd_) -> History cmd resp -> (Matrix Double, Matrix Double)
markovToDot :: (Show state, Show cmd_, Show prob) => state -> state -> Markov state cmd_ prob -> String
markovToPs :: (Show state, Show cmd_, Show prob) => state -> state -> Markov state cmd_ prob -> FilePath -> IO ()
data StatsDb m
StatsDb :: ((Matrix Double, Matrix Double) -> m ()) -> m (Maybe (Matrix Double, Matrix Double)) -> StatsDb m
[store] :: StatsDb m -> (Matrix Double, Matrix Double) -> m ()
[load] :: StatsDb m -> m (Maybe (Matrix Double, Matrix Double))
type PropertyName = String
nullStatsDb :: Monad m => StatsDb m
fileStatsDb :: FilePath -> PropertyName -> StatsDb IO
persistStats :: Monad m => StatsDb m -> (Matrix Double, Matrix Double) -> PropertyM m ()
computeReliability :: Monad m => StatsDb m -> Matrix Double -> (Matrix Double, Matrix Double) -> m (Double, Double)
printReliability :: Testable prop => StatsDb IO -> Matrix Double -> (Matrix Double, Matrix Double) -> prop -> Property
quickCheckReliability :: Testable prop => StatsDb IO -> Matrix Double -> prop -> IO ()
testChainToDot :: forall state cmd_ prob m. (Show state, Ord state, Monad m) => (Generic state, GEnum FiniteEnum (Rep state)) => StatsDb m -> state -> state -> Markov state cmd_ prob -> m String


-- | This module exports some QuickCheck utility functions. Some of these
--   should perhaps be upstreamed.
module Test.StateMachine.Utils

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

-- | Lifts <a>any</a> to properties.
anyP :: (a -> Property) -> [a] -> Property
suchThatEither :: forall a. Gen a -> (a -> Bool) -> Gen (Either [a] a)
collects :: Show a => [a] -> Property -> Property

-- | More permissive notion of shrinking where a value can shrink to itself
--   
--   For example
--   
--   <pre>
--   shrink  3 == [0, 2] -- standard QuickCheck shrink
--   shrinkS 3 == [Shrunk True 0, Shrunk True 2, Shrunk False 3]
--   </pre>
--   
--   This is primarily useful when shrinking composite structures: the
--   combinators here keep track of whether something was shrunk
--   <i>somewhere</i> in the structure. For example, we have
--   
--   <pre>
--      shrinkListS (shrinkPairS shrinkS shrinkS) [(1,3),(2,4)]
--   == [ Shrunk True  []             -- removed all elements of the list
--      , Shrunk True  [(2,4)]        -- removed the first
--      , Shrunk True  [(1,3)]        -- removed the second
--      , Shrunk True  [(0,3),(2,4)]  -- shrinking the '1'
--      , Shrunk True  [(1,0),(2,4)]  -- shrinking the '3'
--      , Shrunk True  [(1,2),(2,4)]  -- ..
--      , Shrunk True  [(1,3),(0,4)]  -- shrinking the '2'
--      , Shrunk True  [(1,3),(1,4)]  -- ..
--      , Shrunk True  [(1,3),(2,0)]  -- shrinking the '4'
--      , Shrunk True  [(1,3),(2,2)]  -- ..
--      , Shrunk True  [(1,3),(2,3)]  -- ..
--      , Shrunk False [(1,3),(2,4)]  -- the original unchanged list
--      ]
--   </pre>
data Shrunk a
Shrunk :: Bool -> a -> Shrunk a
[wasShrunk] :: Shrunk a -> Bool
[shrunk] :: Shrunk a -> a
shrinkS :: Arbitrary a => a -> [Shrunk a]
shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]

-- | Shrink list without shrinking elements.
shrinkListS' :: [a] -> [Shrunk [a]]

-- | Shrink list by only shrinking elements.
shrinkListS'' :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkPairS :: (a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
pickOneReturnRest :: [a] -> [(a, [a])]
pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a], [a]))]
pickOneReturnRestL :: [[a]] -> [(a, [[a]])]
mkModel :: StateMachine model cmd m resp -> History cmd resp -> model Concrete
instance GHC.Base.Functor Test.StateMachine.Utils.Shrunk
instance GHC.Show.Show a => GHC.Show.Show (Test.StateMachine.Utils.Shrunk a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Test.StateMachine.Utils.Shrunk a)


-- | This module contains helpers for generating, shrinking, and checking
--   sequential programs.
module Test.StateMachine.Sequential
forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd resp -> prop) -> Property

-- | Generate commands from a list of generators.
existsCommands :: forall model cmd m resp prop. (Testable prop, Foldable resp) => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> [model Symbolic -> Gen (cmd Symbolic)] -> (Commands cmd resp -> prop) -> Property
generateCommands :: (Foldable resp, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd resp)
generateCommandsState :: forall model cmd m resp. Foldable resp => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic) Gen (Commands cmd resp)
deadlockError :: (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => model Symbolic -> [Command cmd resp] -> String -> b
getUsedVars :: Foldable f => f Symbolic -> [Var]

-- | Shrink commands in a pre-condition and scope respecting way.
shrinkCommands :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd resp -> [Commands cmd resp]

-- | Validate list of commands, optionally shrinking one of the commands
--   
--   The input to this function is a list of commands (<a>Commands</a>),
--   for example
--   
--   <pre>
--   [A, B, C, D, E, F, G, H]
--   </pre>
--   
--   The <i>result</i> is a <i>list</i> of <a>Commands</a>, i.e. a list of
--   lists. The outermost list is used for all the shrinking possibilities.
--   For example, let's assume we haven't shrunk something yet, and
--   therefore need to shrink one of the commands. Let's further assume
--   that only commands B and E can be shrunk, to B1, B2 and E1, E2, E3
--   respectively. Then the result will look something like
--   
--   <pre>
--   [    -- outermost list recording all the shrink possibilities
--       [A', B1', C', D', E' , F', G', H']   -- B shrunk to B1
--     , [A', B2', C', D', E' , F', G', H']   -- B shrunk to B2
--     , [A', B' , C', D', E1', F', G', H']   -- E shrunk to E1
--     , [A', B' , C', D', E2', F', G', H']   -- E shrunk to E2
--     , [A', B' , C', D', E3', F', G', H']   -- E shrunk to E3
--   ]
--   </pre>
--   
--   where one of the commands has been shrunk and all commands have been
--   validated and renumbered (references updated). So, in this example,
--   the result will contain at most 5 lists; it may contain fewer, since
--   some of these lists may not be valid.
--   
--   If we _did_ already shrink something, then no commands will be shrunk,
--   and the resulting list will either be empty (if the list of commands
--   was invalid) or contain a <i>single</i> element with the validated and
--   renumbered commands.
shrinkAndValidate :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ValidateEnv model -> Commands cmd resp -> [(ValidateEnv model, Commands cmd resp)]

-- | Environment required during <a>shrinkAndValidate</a>
data ValidateEnv model
ValidateEnv :: model Symbolic -> Map Var Var -> Counter -> ValidateEnv model

-- | The model we're starting validation from
[veModel] :: ValidateEnv model -> model Symbolic

-- | Reference renumbering
--   
--   When a command
--   
--   <pre>
--   Command .. [Var i, ..]
--   </pre>
--   
--   is changed during validation to
--   
--   <pre>
--   Command .. [Var j, ..]
--   </pre>
--   
--   then any subsequent uses of <tt>Var i</tt> should be replaced by
--   <tt>Var j</tt>. This is recorded in <a>veScope</a>. When we
--   <i>remove</i> the first command altogether (during shrinking), then
--   <tt>Var i</tt> won't appear in the <a>veScope</a> and shrank
--   candidates that contain commands referring to <tt>Var i</tt> should be
--   considered as invalid.
[veScope] :: ValidateEnv model -> Map Var Var

-- | Counter (for generating new references)
[veCounter] :: ValidateEnv model -> Counter
data ShouldShrink
MustShrink :: ShouldShrink
DontShrink :: ShouldShrink
initValidateEnv :: model Symbolic -> ValidateEnv model
runCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
runCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => m (StateMachine model cmd m resp) -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => m (StateMachine model cmd m resp) -> Commands cmd resp -> m (History cmd resp, model Concrete, Reason)
getChanContents :: MonadIO m => TChan a -> m [a]
data Check
CheckPrecondition :: Check
CheckEverything :: Check
CheckNothing :: Check
executeCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadIO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Check -> Commands cmd resp -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason
prettyPrintHistory :: forall model cmd m resp. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> IO ()
prettyPrintHistory' :: forall model cmd m resp tag. ToExpr (model Concrete) => (Show (cmd Concrete), Show (resp Concrete), ToExpr tag) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> IO ()
prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()

-- | Variant of <a>prettyCommands</a> that also prints the <tt>tag</tt>s
--   covered by each command.
prettyCommands' :: (MonadIO m, ToExpr (model Concrete), ToExpr tag) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> Property -> PropertyM m ()
saveCommands :: (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property
runSavedCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => (Read (cmd Symbolic), Read (resp Symbolic)) => StateMachine model cmd m resp -> FilePath -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason)
commandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [(String, Int)]
commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String]

-- | Fail if some commands have not been executed.
coverCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property

-- | Print the percentage of each command used. The prefix check is an
--   unfortunate remaining for backwards compatibility.
checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property
showLabelledExamples :: (Show tag, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> IO ()

-- | Show minimal examples for each of the generated tags.
showLabelledExamples' :: (Show tag, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -> IO ()


-- | This module contains helpers for generating, shrinking, and checking
--   parallel programs.
--   
--   Note that:
--   
--   <ul>
--   <li>the <tt>.*NParallelCommands</tt> functions and the
--   <a>NParallelCommands</a> datatype are expected to be used when you
--   want to run <tt>N</tt> concurrent threads running at the same time and
--   repeat each test 10 (by default) times to get sufficient randomness on
--   the RTS scheduling of concurrent actions.</li>
--   <li>the <tt>.*ParallelCommandsNTimes</tt> functions and the
--   <a>ParallelCommandsF</a> datatype are expected to be used when you
--   want to run the test with 2 concurrent threads and repeat each test
--   <tt>N</tt> times to get sufficient randomness on the RTS scheduling of
--   concurrent actions.</li>
--   <li>the <tt>.*NParallelCommandsNTime</tt> functions do both of the
--   above points at the same time, in particular they take an
--   <a>NParallelCommands</a> value generated to be run by some number of
--   threads concurrently, and they take as input how many times each test
--   should be repeated.</li>
--   <li>the <tt>run.*WithSetup</tt> functions receive a monadic action
--   that must initialize the StateMachine which will be used at the
--   beginning of each repetition of each sequence of commands. See the
--   section in the <a>README</a> for more context.</li>
--   </ul>
module Test.StateMachine.Parallel
forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Int -> (NParallelCommands cmd resp -> prop) -> Property
forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property
generateNParallelCommands :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Int -> Gen (NParallelCommands cmd resp)

-- | Generate parallel commands.
--   
--   Parallel commands are generated as follows. We begin by generating
--   sequential commands and then splitting this list in two at some index.
--   The first half will be used as the prefix.
--   
--   The second half will be used to build suffixes. For example, starting
--   from the following sequential commands:
--   
--   <pre>
--   [A, B, C, D, E, F, G, H, I]
--   </pre>
--   
--   We split it in two, giving us the prefix and the rest:
--   
--   <pre>
--   prefix: [A, B]
--   rest:   [C, D, E, F, G, H, I]
--   </pre>
--   
--   We advance the model with the prefix.
--   
--   <b>Make a suffix</b>: we take commands from <tt>rest</tt> as long as
--   these are parallel safe (see <a>parallelSafe</a>). This means that the
--   pre-conditions (using the 'advanced' model) of each of those commands
--   will hold no matter in which order they are executed.
--   
--   Say this is true for <tt>[C, D, E]</tt>, but not anymore for
--   <tt>F</tt>, maybe because <tt>F</tt> depends on one of <tt>[C, D,
--   E]</tt>. Then we divide this 'chunk' in two by splitting it in the
--   middle, obtaining <tt>[C]</tt> and <tt>[D, E]</tt>. These two halves
--   of the chunk (stored as a <a>Pair</a>) will later be executed in
--   parallel. Together they form one suffix.
--   
--   Then the model is advanced using the whole chunk <tt>[C, D, E]</tt>.
--   Think of it as a barrier after executing the two halves of the chunk
--   in parallel. Then this process of building a chunk/suffix repeats
--   itself, starting from <b>Make a suffix</b> using the 'advanced' model.
--   
--   In the end we might end up with something like this:
--   
--   <pre>
--           ┌─ [C] ──┐  ┌ [F, G] ┐
--   [A, B] ─┤        ├──┤        │
--           └ [D, E] ┘  └ [H, I] ┘
--   </pre>
generateParallelCommands :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => (Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> Maybe Int -> Gen (ParallelCommands cmd resp)

-- | Shrink a parallel program in a pre-condition and scope respecting way.
shrinkNParallelCommands :: forall cmd model m resp. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> NParallelCommands cmd resp -> [NParallelCommands cmd resp]

-- | Shrink a parallel program in a pre-condition and scope respecting way.
shrinkParallelCommands :: forall cmd model m resp. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkAndValidateNParallel :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkAndValidateParallel :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ShouldShrink -> ParallelCommands cmd resp -> [ParallelCommands cmd resp]

-- | Shrinks Commands in a way that it has strictly less number of
--   commands.
shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)]
runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> TChan (Pid, HistoryEvent cmd resp) -> Bool -> m (History cmd resp, model Concrete, Reason, Reason)

-- | 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 cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic

-- | Draw an ASCII diagram of the history of a parallel program. Useful for
--   seeing how a race condition might have occured.
toBoxDrawings :: forall cmd resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> History cmd resp -> Doc
prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => ParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m ()

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyParallelCommandsWithOpts :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m ()

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m ()

-- | Apply the transition of some commands to a model.
advanceModel :: StateMachine model cmd m resp -> model Symbolic -> Commands cmd resp -> model Symbolic

-- | Print the percentage of each command used. The prefix check is an
--   unfortunate remaining for backwards compatibility.
checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property

-- | Fail if some commands have not been executed.
coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property
commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> [(String, Int)]


-- | The main module for state machine based testing, it contains
--   combinators that help you build sequential and parallel properties.
module Test.StateMachine
forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd resp -> prop) -> Property

-- | Generate commands from a list of generators.
existsCommands :: forall model cmd m resp prop. (Testable prop, Foldable resp) => (Show (model Symbolic), Show (cmd Symbolic), Show (resp Symbolic)) => StateMachine model cmd m resp -> [model Symbolic -> Gen (cmd Symbolic)] -> (Commands cmd resp -> prop) -> Property
runCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => StateMachine model cmd m resp -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
runCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => m (StateMachine model cmd m resp) -> Commands cmd resp -> PropertyM m (History cmd resp, model Concrete, Reason)
prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()

-- | Variant of <a>prettyCommands</a> that also prints the <tt>tag</tt>s
--   covered by each command.
prettyCommands' :: (MonadIO m, ToExpr (model Concrete), ToExpr tag) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> Commands cmd resp -> History cmd resp -> Property -> PropertyM m ()

-- | Print the percentage of each command used. The prefix check is an
--   unfortunate remaining for backwards compatibility.
checkCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property

-- | Fail if some commands have not been executed.
coverCommandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> Property -> Property
commandNames :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [(String, Int)]
commandNamesInOrder :: forall cmd resp. CommandNames cmd => Commands cmd resp -> [String]
saveCommands :: (Show (cmd Symbolic), Show (resp Symbolic)) => FilePath -> Commands cmd resp -> Property -> Property
runSavedCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadIO m) => (Read (cmd Symbolic), Read (resp Symbolic)) => StateMachine model cmd m resp -> FilePath -> PropertyM m (Commands cmd resp, History cmd resp, model Concrete, Reason)
showLabelledExamples :: (Show tag, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ([Event model cmd resp Symbolic] -> [tag]) -> IO ()

-- | Show minimal examples for each of the generated tags.
showLabelledExamples' :: (Show tag, Show (model Symbolic)) => (Show (cmd Symbolic), Show (resp Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> Int -> ([Event model cmd resp Symbolic] -> [tag]) -> (tag -> Bool) -> IO ()
noCleanup :: Monad m => model Concrete -> m ()
forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property
forAllNParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic)) => (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> Int -> (NParallelCommands cmd resp -> prop) -> Property
runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> (cmd Concrete -> resp Concrete) -> ParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadMask m, MonadUnliftIO m) => Int -> m (StateMachine model cmd m resp) -> NParallelCommands cmd resp -> PropertyM m [(History cmd resp, model Concrete, Logic)]
prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => ParallelCommands cmd resp -> [(History cmd resp, a, Logic)] -> PropertyM m ()

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyParallelCommandsWithOpts :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m ()

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete)) => MonadIO m => Foldable cmd => NParallelCommands cmd resp -> Maybe GraphOptions -> [(History cmd resp, a, Logic)] -> PropertyM m ()

-- | Print the percentage of each command used. The prefix check is an
--   unfortunate remaining for backwards compatibility.
checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property

-- | Fail if some commands have not been executed.
coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> Property -> Property
commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd => ParallelCommandsF t cmd resp -> [(String, Int)]
data StateMachine model cmd m resp
StateMachine :: (forall r. model r) -> (forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r) -> (model Symbolic -> cmd Symbolic -> Logic) -> (model Concrete -> cmd Concrete -> resp Concrete -> Logic) -> Maybe (model Concrete -> Logic) -> (model Symbolic -> Maybe (Gen (cmd Symbolic))) -> (model Symbolic -> cmd Symbolic -> [cmd Symbolic]) -> (cmd Concrete -> m (resp Concrete)) -> (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)) -> (model Concrete -> m ()) -> StateMachine model cmd m resp
data Concrete a
data Symbolic a
data Reference a r
concrete :: Reference a Concrete -> a
reference :: Typeable a => a -> Reference a Concrete
newtype Opaque a
Opaque :: a -> Opaque a
[unOpaque] :: Opaque a -> a
opaque :: Reference (Opaque a) Concrete -> a
data Reason
Ok :: Reason
PreconditionFailed :: String -> Reason
PostconditionFailed :: String -> Reason
InvariantBroken :: String -> Reason
ExceptionThrown :: String -> Reason
MockSemanticsMismatch :: String -> Reason
data GenSym a
genSym :: Typeable a => GenSym (Reference a Symbolic)

-- | The names of all possible commands
--   
--   This is used for things like tagging, coverage checking, etc.
class CommandNames (cmd :: k -> Type)

-- | Name of this particular command
cmdName :: CommandNames cmd => cmd r -> String

-- | Name of all possible commands
cmdNames :: CommandNames cmd => Proxy (cmd r) -> [String]

-- | Name of this particular command
cmdName :: (CommandNames cmd, Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String

-- | Name of all possible commands
cmdNames :: forall r. (CommandNames cmd, CommandNames (Rep1 cmd)) => Proxy (cmd r) -> [String]

-- | <a>toExpr</a> converts a Haskell value into untyped Haskell-like
--   syntax tree, <a>Expr</a>.
--   
--   <pre>
--   &gt;&gt;&gt; toExpr ((1, Just 2) :: (Int, Maybe Int))
--   App "_\215_" [App "1" [],App "Just" [App "2" []]]
--   </pre>
class ToExpr a
toExpr :: ToExpr a => a -> Expr

module Test.StateMachine.Lockstep.NAry

-- | Mock state
--   
--   The <tt>t</tt> argument (here and elsewhere) is a type-level tag that
--   combines all aspects of the test; it does not need any term-level
--   constructors
--   
--   <pre>
--   data MyTest
--   type instance MockState MyTest = ..
--   </pre>
type family MockState t :: Type

-- | Commands
--   
--   In <tt>Cmd t f hs</tt>, <tt>hs</tt> is the list of real handle types,
--   and <tt>f</tt> is some functor applied to each of them. Two typical
--   instantiations are
--   
--   <pre>
--   Cmd t I              (RealHandles t)   -- for the system under test
--   Cmd t (MockHandle t) (RealHandles t)   -- for the mock
--   </pre>
data family Cmd t :: (Type -> Type) -> [Type] -> Type

-- | Responses
--   
--   The type arguments are similar to those of <tt>Cmd</tt>. Two typical
--   instances:
--   
--   <pre>
--   Resp t I              (RealHandles t)  -- for the system under test
--   Resp t (MockHandle t) (RealHandles t)  -- for the mock
--   </pre>
data family Resp t :: (Type -> Type) -> [Type] -> Type

-- | Type-level list of the types of the handles in the system under test
--   
--   NOTE: If your system under test only requires a single real handle,
--   you might consider using <a>Test.StateMachine.Lockstep.Simple</a>
--   instead.
type family RealHandles t :: [Type]

-- | Mock handles
--   
--   For each real handle <tt>a</tt>, <tt>MockHandle t a</tt> is the
--   corresponding mock handle.
data family MockHandle t a :: Type
type family Test (f :: (Type -> Type) -> [Type] -> Type) :: Type

-- | Tags
--   
--   Tags are used when labelling execution runs in <a>prop_sequential</a>,
--   as well as when looking for minimal examples with a given label
--   (<a>showLabelledExamples</a>).
type family Tag t :: Type

-- | State machine test
--   
--   This captures the design patterns sketched in
--   <a>https://well-typed.com/blog/2019/01/qsm-in-depth/</a>.
data StateMachineTest t m
StateMachineTest :: (Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t)) -> (Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))) -> MockState t -> (forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)) -> (Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))) -> (Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]) -> (Model t Concrete -> m ()) -> ([Event t Symbolic] -> [Tag t]) -> StateMachineTest t m
[runMock] :: StateMachineTest t m -> Cmd t (MockHandle t) (RealHandles t) -> MockState t -> (Resp t (MockHandle t) (RealHandles t), MockState t)
[runReal] :: StateMachineTest t m -> Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
[initMock] :: StateMachineTest t m -> MockState t
[newHandles] :: StateMachineTest t m -> forall f. Resp t f (RealHandles t) -> NP ([] :.: f) (RealHandles t)
[generator] :: StateMachineTest t m -> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
[shrinker] :: StateMachineTest t m -> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
[cleanup] :: StateMachineTest t m -> Model t Concrete -> m ()
[tag] :: StateMachineTest t m -> [Event t Symbolic] -> [Tag t]
data Event t r
Event :: Model t r -> (Cmd t :@ r) -> Model t r -> Resp t (MockHandle t) (RealHandles t) -> Event t r
[before] :: Event t r -> Model t r
[cmd] :: Event t r -> Cmd t :@ r
[after] :: Event t r -> Model t r
[mockResp] :: Event t r -> Resp t (MockHandle t) (RealHandles t)
hoistStateMachineTest :: Monad n => (forall a. m a -> n a) -> StateMachineTest t m -> StateMachineTest t n
newtype At f r
At :: f (FlipRef r) (RealHandles (Test f)) -> At f r
[unAt] :: At f r -> f (FlipRef r) (RealHandles (Test f))
type f :@ r = At f r
data Model t r
Model :: MockState t -> Refss t r -> Model t r
[modelState] :: Model t r -> MockState t
[modelRefss] :: Model t r -> Refss t r

-- | Relation between real and mock references for single handle type
--   <tt>a</tt>
newtype Refs t r a
Refs :: [(Reference a r, MockHandle t a)] -> Refs t r a
[unRefs] :: Refs t r a -> [(Reference a r, MockHandle t a)]

-- | Relation between real and mock references for <i>all</i> handle types
newtype Refss t r
Refss :: NP (Refs t r) (RealHandles t) -> Refss t r
[unRefss] :: Refss t r -> NP (Refs t r) (RealHandles t)
newtype FlipRef r h
FlipRef :: Reference h r -> FlipRef r h
[unFlipRef] :: FlipRef r h -> Reference h r

-- | Sequential test
prop_sequential :: forall t. StateMachineTest t IO -> Maybe Int -> Property

-- | Parallel test
--   
--   NOTE: This currently does not do labelling.
prop_parallel :: StateMachineTest t IO -> Maybe Int -> Property

-- | Show minimal examples for each of the generated tags.
--   
--   This is the analogue of <a>showLabelledExamples'</a>. See also
--   <a>showLabelledExamples</a>.
showLabelledExamples' :: StateMachineTest t m -> Maybe Int -> Int -> (Tag t -> Bool) -> IO ()

-- | Simplified form of <a>showLabelledExamples'</a>
showLabelledExamples :: StateMachineTest t m -> IO ()
toStateMachine :: StateMachineTest t m -> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))
instance GHC.Generics.Generic (Test.StateMachine.Lockstep.NAry.Refs t r a)
instance GHC.Base.Monoid (Test.StateMachine.Lockstep.NAry.Refs t r a)
instance GHC.Base.Semigroup (Test.StateMachine.Lockstep.NAry.Refs t r a)
instance (Data.Functor.Classes.Show1 r, GHC.Show.Show h) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.FlipRef r h)
instance GHC.Generics.Generic (Test.StateMachine.Lockstep.NAry.Model t r)
instance (Data.Functor.Classes.Show1 r, GHC.Show.Show a, GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle t a)) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Refs t r a)
instance (Data.TreeDiff.Class.ToExpr a, Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle t a)) => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.Refs t Test.StateMachine.Types.References.Concrete a)
instance GHC.Show.Show (f (Test.StateMachine.Lockstep.NAry.FlipRef r) (Test.StateMachine.Lockstep.NAry.RealHandles (Test.StateMachine.Lockstep.NAry.Test f))) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.At f r)
instance (Data.Functor.Classes.Show1 r, GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockState t), Data.SOP.Constraint.All (Data.SOP.Constraint.And GHC.Show.Show (Data.SOP.Constraint.Compose GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t)) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Model t r)
instance (Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockState t), Data.SOP.Constraint.All (Data.SOP.Constraint.And Data.TreeDiff.Class.ToExpr (Data.SOP.Constraint.Compose Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.Model t Test.StateMachine.Types.References.Concrete)
instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Cmd t))
instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Cmd t))
instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Cmd t))
instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Functor (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Resp t))
instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Foldable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Resp t))
instance (Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp t), Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t)) => Test.StateMachine.Types.Rank2.Traversable (Test.StateMachine.Lockstep.NAry.At (Test.StateMachine.Lockstep.NAry.Resp t))
instance (Data.Functor.Classes.Show1 r, Data.SOP.Constraint.All (Data.SOP.Constraint.And GHC.Show.Show (Data.SOP.Constraint.Compose GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t)) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Refss t r)
instance Data.SOP.Constraint.All (Data.SOP.Constraint.And Data.TreeDiff.Class.ToExpr (Data.SOP.Constraint.Compose Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle t))) (Test.StateMachine.Lockstep.NAry.RealHandles t) => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.Refss t Test.StateMachine.Types.References.Concrete)
instance Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t) => GHC.Base.Semigroup (Test.StateMachine.Lockstep.NAry.Refss t r)
instance Data.SOP.Constraint.SListI (Test.StateMachine.Lockstep.NAry.RealHandles t) => GHC.Base.Monoid (Test.StateMachine.Lockstep.NAry.Refss t r)

module Test.StateMachine.Lockstep.Simple

-- | Mock state
--   
--   The <tt>t</tt> argument (here and elsewhere) is a type-level tag that
--   combines all aspects of the test; it does not need any term-level
--   constructors
--   
--   <pre>
--   data MyTest
--   type instance MockState MyTest = ..
--   </pre>
type family MockState t :: Type

-- | Commands
--   
--   In <tt>Cmd t h</tt>, <tt>h</tt> is the type of the handle
--   
--   <pre>
--   Cmd t (RealHandle t)  -- for the system under test
--   Cmd t (MockHandle t)  -- for the mock
--   </pre>
data family Cmd t :: Type -> Type

-- | Responses
--   
--   In <tt>Resp t h</tt>, <tt>h</tt> is the type of the handle
--   
--   <pre>
--   Resp t (RealHandle t)  -- for the system under test
--   Resp t (MockHandle t)  -- for the mock
--   </pre>
data family Resp t :: Type -> Type

-- | The type of the real handle in the system under test
--   
--   The key difference between the " simple " lockstep infrastructure and
--   the n-ary lockstep infrastructure is that the former only supports a
--   single real handle, whereas the latter supports an arbitrary list of
--   them.
data family RealHandle t :: Type

-- | The type of the mock handle
--   
--   NOTE: In the n-ary infrastructure, <a>MockHandle</a> is a type family
--   of <i>two</i> arguments, because we have a mock handle for each real
--   handle. Here, however, we only <i>have</i> a single real handle, so
--   the " corresponding " real handle is implicitly <tt>RealHandle t</tt>.
data family MockHandle t :: Type
type family Test (f :: Type -> Type) :: Type

-- | Tags
--   
--   Tags are used when labelling execution runs in <a>prop_sequential</a>,
--   as well as when looking for minimal examples with a given label
--   (<a>showLabelledExamples</a>).
type family Tag t :: Type

-- | State machine test
--   
--   This captures the design patterns sketched in
--   <a>https://well-typed.com/blog/2019/01/qsm-in-depth/</a> for the case
--   where there is exactly one real handle. See
--   <a>Test.StateMachine.Lockstep.NAry</a> for the generalization to
--   <tt>n</tt> handles.
data StateMachineTest t
StateMachineTest :: (Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t)) -> (Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))) -> MockState t -> (forall h. Resp t h -> [h]) -> (Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))) -> (Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]) -> (Model t Concrete -> IO ()) -> ([Event t Symbolic] -> [Tag t]) -> StateMachineTest t
[runMock] :: StateMachineTest t -> Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t)
[runReal] :: StateMachineTest t -> Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
[initMock] :: StateMachineTest t -> MockState t
[newHandles] :: StateMachineTest t -> forall h. Resp t h -> [h]
[generator] :: StateMachineTest t -> Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
[shrinker] :: StateMachineTest t -> Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
[cleanup] :: StateMachineTest t -> Model t Concrete -> IO ()
[tag] :: StateMachineTest t -> [Event t Symbolic] -> [Tag t]
data Event t r
Event :: Model t r -> (Cmd t :@ r) -> Model t r -> Resp t (MockHandle t) -> Event t r
[before] :: Event t r -> Model t r
[cmd] :: Event t r -> Cmd t :@ r
[after] :: Event t r -> Model t r
[mockResp] :: Event t r -> Resp t (MockHandle t)
newtype At f r
At :: f (Reference (RealHandle (Test f)) r) -> At f r
[unAt] :: At f r -> f (Reference (RealHandle (Test f)) r)
type f :@ r = At f r
data Model t r
Model :: MockState t -> [(Reference (RealHandle t) r, MockHandle t)] -> Model t r
[modelState] :: Model t r -> MockState t
[modelRefs] :: Model t r -> [(Reference (RealHandle t) r, MockHandle t)]
prop_sequential :: StateMachineTest t -> Maybe Int -> Property
prop_parallel :: StateMachineTest t -> Maybe Int -> Property
fromSimple :: StateMachineTest t -> StateMachineTest (Simple t) IO
instance GHC.Classes.Eq (Test.StateMachine.Lockstep.Simple.MockHandle t) => GHC.Classes.Eq (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.Simple.RealHandle t))
instance GHC.Show.Show (Test.StateMachine.Lockstep.Simple.MockHandle t) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.Simple.RealHandle t))
instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Resp t), GHC.Classes.Eq (Test.StateMachine.Lockstep.Simple.Resp t (Test.StateMachine.Lockstep.Simple.MockHandle t)), GHC.Classes.Eq (Test.StateMachine.Lockstep.Simple.MockHandle t)) => GHC.Classes.Eq (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t)) '[Test.StateMachine.Lockstep.Simple.RealHandle t])
instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Resp t), GHC.Show.Show (Test.StateMachine.Lockstep.Simple.Resp t (Test.StateMachine.Lockstep.Simple.MockHandle t))) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t)) '[Test.StateMachine.Lockstep.Simple.RealHandle t])
instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Resp t), GHC.Show.Show (Test.StateMachine.Lockstep.Simple.Resp t (Test.StateMachine.Types.References.Reference (Test.StateMachine.Lockstep.Simple.RealHandle t) r)), Data.Functor.Classes.Show1 r) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.FlipRef r) '[Test.StateMachine.Lockstep.Simple.RealHandle t])
instance (GHC.Base.Functor (Test.StateMachine.Lockstep.Simple.Cmd t), GHC.Show.Show (Test.StateMachine.Lockstep.Simple.Cmd t (Test.StateMachine.Types.References.Reference (Test.StateMachine.Lockstep.Simple.RealHandle t) r)), Data.Functor.Classes.Show1 r) => GHC.Show.Show (Test.StateMachine.Lockstep.NAry.Cmd (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.NAry.FlipRef r) '[Test.StateMachine.Lockstep.Simple.RealHandle t])
instance Data.Traversable.Traversable (Test.StateMachine.Lockstep.Simple.Resp t) => Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Resp (Test.StateMachine.Lockstep.Simple.Simple t))
instance Data.Traversable.Traversable (Test.StateMachine.Lockstep.Simple.Cmd t) => Test.StateMachine.Lockstep.Auxiliary.NTraversable (Test.StateMachine.Lockstep.NAry.Cmd (Test.StateMachine.Lockstep.Simple.Simple t))
instance Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.Simple.MockHandle t) => Data.TreeDiff.Class.ToExpr (Test.StateMachine.Lockstep.NAry.MockHandle (Test.StateMachine.Lockstep.Simple.Simple t) (Test.StateMachine.Lockstep.Simple.RealHandle t))


-- | 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
cons :: a -> [a] -> [a]
union :: Eq a => [a] -> [a] -> [a]
infixr 6 `union`
intersect :: Eq a => [a] -> [a] -> [a]
infixr 7 `intersect`

-- | Subset.
--   
--   <pre>
--   &gt;&gt;&gt; boolean ([1, 2] `isSubsetOf` [3, 2, 1])
--   True
--   </pre>
isSubsetOf :: (Eq a, Show a) => [a] -> [a] -> Logic
infix 5 `isSubsetOf`

-- | Set equality.
--   
--   <pre>
--   &gt;&gt;&gt; boolean ([1, 1, 2] ~= [2, 1])
--   True
--   </pre>
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic
infix 5 ~=

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

-- | (Partial) functions.
type Fun a b = Rel a b
type a :<-> b = Rel a b
infixr 1 :<->
type a :-> b = Fun a b
infixr 1 :->
type a :/-> b = Fun a b
infixr 1 :/->
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
infixr 4 <|

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

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

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

-- | 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
infixr 4 <+

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

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

-- | Application.
(!) :: (Eq a, Show a, Show b) => Fun a b -> a -> b
(!?) :: Eq a => Fun a b -> a -> Maybe b
(.%) :: (Eq a, Eq b, Show a, Show b) => (Fun a b, a) -> (b -> b) -> Fun a b
infixr 4 .%
(.!) :: Rel a b -> a -> (Rel a b, a)
infixr 9 .!

-- | 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
infix 4 .=