-- 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.4.0


-- | 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
Predicate :: Predicate -> Logic
Forall :: [a] -> (a -> Logic) -> Logic
Exists :: [a] -> (a -> Logic) -> Logic
Boolean :: Bool -> 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
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
predicate :: Predicate -> Value
(.==) :: (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 .>=
elem :: (Eq a, Show a) => a -> [a] -> Logic
infix 5 `elem`
notElem :: (Eq a, Show a) => a -> [a] -> Logic
infix 5 `notElem`
(.//) :: Logic -> String -> Logic
infixl 4 .//
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.Predicate
instance GHC.Show.Show Test.StateMachine.Logic.Counterexample

module Test.StateMachine.Types.Rank2
class Functor (f :: (k -> *) -> *)
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 -> *) -> *)
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 -> *) -> *)
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
data 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 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.Generics.Generic (Test.StateMachine.Types.References.Reference a r)
instance Data.TreeDiff.Class.ToExpr 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.Show.Show (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.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

-- | 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
makeOperations :: History' cmd resp -> [Operation cmd resp]

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


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.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.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
instance GHC.Show.Show Test.StateMachine.Types.Environment.Environment
instance GHC.Base.Monoid Test.StateMachine.Types.Environment.Environment
instance GHC.Base.Semigroup Test.StateMachine.Types.Environment.Environment


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 Symbolic -> cmd Symbolic -> resp Symbolic -> Logic) -> Maybe (model Concrete -> Logic) -> model Symbolic -> Gen (cmd Symbolic) -> Maybe (Matrix Int) -> cmd Symbolic -> [cmd Symbolic] -> cmd Concrete -> m (resp Concrete) -> m Property -> IO Property -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) -> 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
[spostcondition] :: StateMachine model cmd m resp -> Maybe (model Symbolic -> cmd Symbolic -> resp Symbolic -> Logic)
[invariant] :: StateMachine model cmd m resp -> Maybe (model Concrete -> Logic)
[generator] :: StateMachine model cmd m resp -> model Symbolic -> Gen (cmd Symbolic)
[distribution] :: StateMachine model cmd m resp -> Maybe (Matrix Int)
[shrinker] :: StateMachine model cmd m resp -> cmd Symbolic -> [cmd Symbolic]
[semantics] :: StateMachine model cmd m resp -> cmd Concrete -> m (resp Concrete)
[runner] :: StateMachine model cmd m resp -> m Property -> IO Property
[mock] :: StateMachine model cmd m resp -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
data Command cmd
Command :: !(cmd Symbolic) -> !(Set Var) -> Command cmd
newtype Commands cmd
Commands :: [Command cmd] -> Commands cmd
[unCommands] :: Commands cmd -> [Command cmd]
lengthCommands :: Commands cmd -> Int
data ParallelCommandsF t cmd
ParallelCommands :: !(Commands cmd) -> [t (Commands cmd)] -> ParallelCommandsF t cmd
[prefix] :: ParallelCommandsF t cmd -> !(Commands cmd)
[suffixes] :: ParallelCommandsF t cmd -> [t (Commands cmd)]
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
data Reason
Ok :: Reason
PreconditionFailed :: Reason
PostconditionFailed :: String -> Reason
InvariantBroken :: String -> Reason
ExceptionThrown :: String -> 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 Test.StateMachine.Types.Reason
instance GHC.Classes.Eq Test.StateMachine.Types.Reason
instance GHC.Base.Monoid (Test.StateMachine.Types.Commands cmd)
instance GHC.Base.Semigroup (Test.StateMachine.Types.Commands cmd)
instance GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic) => GHC.Show.Show (Test.StateMachine.Types.Command cmd)
instance GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic) => GHC.Show.Show (Test.StateMachine.Types.Commands cmd)
instance (GHC.Show.Show (cmd Test.StateMachine.Types.References.Symbolic), GHC.Show.Show (t (Test.StateMachine.Types.Commands cmd))) => GHC.Show.Show (Test.StateMachine.Types.ParallelCommandsF t cmd)

module Test.StateMachine.ConstructorName
class GConName a
gconName :: GConName a => a -> String
gconNames :: GConName a => Proxy a -> [String]
class GConName1 f
gconName1 :: GConName1 f => f a -> String
gconNames1 :: GConName1 f => Proxy (f a) -> [String]
instance Test.StateMachine.ConstructorName.GConName1 GHC.Generics.U1
instance Test.StateMachine.ConstructorName.GConName1 (GHC.Generics.K1 i c)
instance forall k (c :: GHC.Generics.Meta) (f :: k -> *). GHC.Generics.Constructor c => Test.StateMachine.ConstructorName.GConName1 (GHC.Generics.M1 GHC.Generics.C c f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.GConName1 f => Test.StateMachine.ConstructorName.GConName1 (GHC.Generics.M1 GHC.Generics.D c f)
instance forall k (f :: k -> *) (c :: GHC.Generics.Meta). Test.StateMachine.ConstructorName.GConName1 f => Test.StateMachine.ConstructorName.GConName1 (GHC.Generics.M1 GHC.Generics.S c f)
instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.GConName1 f, Test.StateMachine.ConstructorName.GConName1 g) => Test.StateMachine.ConstructorName.GConName1 (f GHC.Generics.:+: g)
instance forall k (f :: k -> *) (g :: k -> *). (Test.StateMachine.ConstructorName.GConName1 f, Test.StateMachine.ConstructorName.GConName1 g) => Test.StateMachine.ConstructorName.GConName1 (f GHC.Generics.:*: g)
instance forall k (f :: k -> *). Test.StateMachine.ConstructorName.GConName1 f => Test.StateMachine.ConstructorName.GConName1 (GHC.Generics.Rec1 f)
instance Test.StateMachine.ConstructorName.GConName1 (Test.StateMachine.Types.References.Reference a)
instance (GHC.Generics.Generic1 cmd, Test.StateMachine.ConstructorName.GConName1 (GHC.Generics.Rep1 cmd)) => Test.StateMachine.ConstructorName.GConName (Test.StateMachine.Types.Command cmd)


-- | 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.Base.Functor Test.StateMachine.BoxDrawer.Fork
instance GHC.Show.Show Test.StateMachine.BoxDrawer.EventType


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

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

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

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

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


-- | This module contains helpers for generating, shrinking, and checking
--   sequential programs.
module Test.StateMachine.Sequential
forAllCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd -> prop) -> Property
generateCommands :: (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Maybe Int -> Gen (Commands cmd)
generateCommandsState :: forall model cmd m resp. Foldable resp => Show (model Symbolic) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Counter -> Maybe Int -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd)
measureFrequency :: (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Maybe Int -> Int -> IO (Map (String, Maybe String) Int)
calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Map (String, Maybe String) Int
getUsedVars :: Foldable f => f Symbolic -> Set Var

-- | Shrink commands in a pre-condition and scope respecting way.
shrinkCommands :: (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> [Commands cmd]
liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic]) -> (Command cmd -> [Command cmd])
validCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Commands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (Commands cmd))
filterMaybe :: (a -> Maybe b) -> [a] -> [b]
modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp -> Commands cmd -> PropertyM m Reason
runCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> Commands cmd -> PropertyM m (History cmd resp, model Concrete, Reason)
getChanContents :: TChan a -> IO [a]
executeCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> TChan (Pid, HistoryEvent cmd resp) -> Pid -> Bool -> Commands cmd -> StateT (Environment, 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 ()
prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m ()
commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [(String, Int)]
commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [String]

-- | Print distribution of commands and fail if some commands have not been
--   executed.
checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Property -> Property
transitionMatrix :: forall cmd. GConName1 (Rep1 cmd) => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int


-- | This module contains helpers for generating, shrinking, and checking
--   parallel programs.
module Test.StateMachine.Parallel
forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd -> prop) -> Property
generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Gen (ParallelCommands cmd)

-- | Shrink a parallel program in a pre-condition and scope respecting way.
shrinkParallelCommands :: forall cmd model m resp. Foldable cmd => Foldable resp => StateMachine model cmd m resp -> (ParallelCommands cmd -> [ParallelCommands cmd])
validParallelCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (ParallelCommands cmd))
prop_splitCombine :: [[Int]] -> Bool
runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
runParallelCommandsNTimes :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]

-- | 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. StateMachine model cmd m resp -> History cmd resp -> Bool

-- | 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 -> History cmd resp -> Doc

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


-- | 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 (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> Maybe Int -> (Commands cmd -> prop) -> Property
transitionMatrix :: forall cmd. GConName1 (Rep1 cmd) => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int
modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp -> Commands cmd -> PropertyM m Reason
runCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> Commands cmd -> 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 ()

-- | Print distribution of commands and fail if some commands have not been
--   executed.
checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Property -> Property
commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [(String, Int)]
commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [String]
forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd -> prop) -> Property
runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
runParallelCommandsNTimes :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]

-- | Takes the output of parallel program runs and pretty prints a
--   counterexample if any of the runs fail.
prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> [(History cmd resp, Bool)] -> PropertyM m ()
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 Symbolic -> cmd Symbolic -> resp Symbolic -> Logic) -> Maybe (model Concrete -> Logic) -> model Symbolic -> Gen (cmd Symbolic) -> Maybe (Matrix Int) -> cmd Symbolic -> [cmd Symbolic] -> cmd Concrete -> m (resp Concrete) -> m Property -> IO Property -> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic) -> 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 :: Reason
PostconditionFailed :: String -> Reason
InvariantBroken :: String -> Reason
ExceptionThrown :: String -> Reason
data GenSym a
genSym :: Typeable a => GenSym (Reference a Symbolic)


-- | 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, Show a) => [a] -> [a] -> Logic
(~=) :: (Eq a, Show a) => [a] -> [a] -> Logic

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