Copyright	(C) 2017 ATS Advanced Telematic Systems GmbH
License	BSD-style (see the file LICENSE)
Maintainer	Stevan Andjelkovic <stevan@advancedtelematic.com>
Stability	provisional
Portability	non-portable (GHC extensions)
Safe Haskell	None
Language	Haskell2010

Test.StateMachine

Contents

Sequential property combinators
Parallel property combinators
Types

Description

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

Synopsis

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 ()
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)]
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))
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 {
- unOpaque :: a
}
opaque :: Reference (Opaque a) Concrete -> a
data Reason
- = Ok
- | PreconditionFailed
- | PostconditionFailed String
- | InvariantBroken String
- | ExceptionThrown String
data GenSym a
genSym :: Typeable a => GenSym (Reference a Symbolic)
module Test.StateMachine.Logic

Sequential property combinators

forAllCommands Source #

Arguments

:: Testable prop
=> (Show (cmd Symbolic), Show (model Symbolic))
=> (Generic1 cmd, GConName1 (Rep1 cmd))
=> (Foldable cmd, Foldable resp)
=> StateMachine model cmd m resp
-> Maybe Int	Minimum number of commands.
-> (Commands cmd -> prop)	Predicate.
-> Property

transitionMatrix :: forall cmd. GConName1 (Rep1 cmd) => Proxy (cmd Symbolic) -> (String -> String -> Int) -> Matrix Int Source #

modelCheck :: forall model cmd resp m. Monad m => StateMachine model cmd m resp -> Commands cmd -> PropertyM m Reason Source #

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

prettyCommands :: (MonadIO m, ToExpr (model Concrete)) => (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Property -> PropertyM m () Source #

checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> Property -> Property Source #

Print distribution of commands and fail if some commands have not been executed.

commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [(String, Int)] Source #

commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd)) => Commands cmd -> [String] Source #

Parallel property combinators

forAllParallelCommands Source #

Arguments

:: 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)	Predicate.
-> Property

runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)] Source #

runParallelCommandsNTimes Source #

Arguments

:: (Traversable cmd, Foldable resp)
=> (MonadCatch m, MonadBaseControl IO m)
=> Int	How many times to execute the parallel program.
-> StateMachine model cmd m resp
-> ParallelCommands cmd
-> PropertyM m [(History cmd resp, Bool)]

prettyParallelCommands Source #

Arguments

:: (MonadIO m, Foldable cmd)
=> (Show (cmd Concrete), Show (resp Concrete))
=> ParallelCommands cmd
-> [(History cmd resp, Bool)]	Output of `runParallelCommands`.
-> PropertyM m ()

Takes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.

Types

data StateMachine model cmd m resp Source #

Constructors

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

data Concrete a Source #

Instances

Eq1 Concrete Source #
Instance details Defined in Test.StateMachine.Types.References Methods liftEq :: (a -> b -> Bool) -> Concrete a -> Concrete b -> Bool #
Ord1 Concrete Source #
Instance details Defined in Test.StateMachine.Types.References Methods liftCompare :: (a -> b -> Ordering) -> Concrete a -> Concrete b -> Ordering #
Show1 Concrete Source #
Instance details Defined in Test.StateMachine.Types.References Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Concrete a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Concrete a] -> ShowS #
Show a => Show (Concrete a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods showsPrec :: Int -> Concrete a -> ShowS # show :: Concrete a -> String # showList :: [Concrete a] -> ShowS #
ToExpr a => ToExpr (Concrete a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods toExpr :: Concrete a -> Expr # listToExpr :: [Concrete a] -> Expr #

data Symbolic a Source #

Instances

Eq1 Symbolic Source #
Instance details Defined in Test.StateMachine.Types.References Methods liftEq :: (a -> b -> Bool) -> Symbolic a -> Symbolic b -> Bool #
Ord1 Symbolic Source #
Instance details Defined in Test.StateMachine.Types.References Methods liftCompare :: (a -> b -> Ordering) -> Symbolic a -> Symbolic b -> Ordering #
Show1 Symbolic Source #
Instance details Defined in Test.StateMachine.Types.References Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Symbolic a -> ShowS # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Symbolic a] -> ShowS #
Eq (Symbolic a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods (==) :: Symbolic a -> Symbolic a -> Bool # (/=) :: Symbolic a -> Symbolic a -> Bool #
Ord (Symbolic a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods compare :: Symbolic a -> Symbolic a -> Ordering # (<) :: Symbolic a -> Symbolic a -> Bool # (<=) :: Symbolic a -> Symbolic a -> Bool # (>) :: Symbolic a -> Symbolic a -> Bool # (>=) :: Symbolic a -> Symbolic a -> Bool # max :: Symbolic a -> Symbolic a -> Symbolic a # min :: Symbolic a -> Symbolic a -> Symbolic a #
Show (Symbolic a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods showsPrec :: Int -> Symbolic a -> ShowS # show :: Symbolic a -> String # showList :: [Symbolic a] -> ShowS #
ToExpr a => ToExpr (Symbolic a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods toExpr :: Symbolic a -> Expr # listToExpr :: [Symbolic a] -> Expr #

data Reference a r Source #

Instances

Traversable (Reference a :: (* -> ) -> ) Source #
Instance details Defined in Test.StateMachine.Types.References Methods traverse :: Applicative f => (forall (a0 :: k). p a0 -> f (q a0)) -> Reference a p -> f (Reference a q) Source #
Foldable (Reference a :: (* -> ) -> ) Source #
Instance details Defined in Test.StateMachine.Types.References Methods foldMap :: Monoid m => (forall (x :: k). p x -> m) -> Reference a p -> m Source #
Functor (Reference a :: (* -> ) -> ) Source #
Instance details Defined in Test.StateMachine.Types.References Methods fmap :: (forall (x :: k). p x -> q x) -> Reference a p -> Reference a q Source #
(Eq a, Eq1 r) => Eq (Reference a r) Source #
Instance details Defined in Test.StateMachine.Types.References Methods (==) :: Reference a r -> Reference a r -> Bool # (/=) :: Reference a r -> Reference a r -> Bool #
(Ord a, Ord1 r) => Ord (Reference a r) Source #
Instance details Defined in Test.StateMachine.Types.References Methods compare :: Reference a r -> Reference a r -> Ordering # (<) :: Reference a r -> Reference a r -> Bool # (<=) :: Reference a r -> Reference a r -> Bool # (>) :: Reference a r -> Reference a r -> Bool # (>=) :: Reference a r -> Reference a r -> Bool # max :: Reference a r -> Reference a r -> Reference a r # min :: Reference a r -> Reference a r -> Reference a r #
(Show1 r, Show a) => Show (Reference a r) Source #
Instance details Defined in Test.StateMachine.Types.References Methods showsPrec :: Int -> Reference a r -> ShowS # show :: Reference a r -> String # showList :: [Reference a r] -> ShowS #
Generic (Reference a r) Source #
Instance details Defined in Test.StateMachine.Types.References Associated Types type Rep (Reference a r) :: * -> * # Methods from :: Reference a r -> Rep (Reference a r) x # to :: Rep (Reference a r) x -> Reference a r #
ToExpr (r a) => ToExpr (Reference a r) Source #
Instance details Defined in Test.StateMachine.Types.References Methods toExpr :: Reference a r -> Expr # listToExpr :: [Reference a r] -> Expr #
GConName1 (Reference a :: (* -> ) -> ) Source #
Instance details Defined in Test.StateMachine.ConstructorName Methods gconName1 :: Reference a a0 -> String Source # gconNames1 :: Proxy (Reference a a0) -> [String] Source #
type Rep (Reference a r) Source #
Instance details Defined in Test.StateMachine.Types.References type Rep (Reference a r) = D1 (MetaData "Reference" "Test.StateMachine.Types.References" "quickcheck-state-machine-0.4.0-LCNcOu7FGqH6wuUxD0jkCH" False) (C1 (MetaCons "Reference" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (r a))))

concrete :: Reference a Concrete -> a Source #

reference :: Typeable a => a -> Reference a Concrete Source #

newtype Opaque a Source #

Constructors

Opaque
Fields unOpaque :: a

Instances

Eq a => Eq (Opaque a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods (==) :: Opaque a -> Opaque a -> Bool # (/=) :: Opaque a -> Opaque a -> Bool #
Ord a => Ord (Opaque a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods compare :: Opaque a -> Opaque a -> Ordering # (<) :: Opaque a -> Opaque a -> Bool # (<=) :: Opaque a -> Opaque a -> Bool # (>) :: Opaque a -> Opaque a -> Bool # (>=) :: Opaque a -> Opaque a -> Bool # max :: Opaque a -> Opaque a -> Opaque a # min :: Opaque a -> Opaque a -> Opaque a #
Show (Opaque a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods showsPrec :: Int -> Opaque a -> ShowS # show :: Opaque a -> String # showList :: [Opaque a] -> ShowS #
ToExpr (Opaque a) Source #
Instance details Defined in Test.StateMachine.Types.References Methods toExpr :: Opaque a -> Expr # listToExpr :: [Opaque a] -> Expr #

opaque :: Reference (Opaque a) Concrete -> a Source #

data Reason Source #

Constructors

Ok
PreconditionFailed
PostconditionFailed String
InvariantBroken String
ExceptionThrown String

Instances

Eq Reason Source #
Instance details Defined in Test.StateMachine.Types Methods (==) :: Reason -> Reason -> Bool # (/=) :: Reason -> Reason -> Bool #
Show Reason Source #
Instance details Defined in Test.StateMachine.Types Methods showsPrec :: Int -> Reason -> ShowS # show :: Reason -> String # showList :: [Reason] -> ShowS #

data GenSym a Source #

Instances

Monad GenSym Source #
Instance details Defined in Test.StateMachine.Types.GenSym Methods (>>=) :: GenSym a -> (a -> GenSym b) -> GenSym b # (>>) :: GenSym a -> GenSym b -> GenSym b # return :: a -> GenSym a # fail :: String -> GenSym a #
Functor GenSym Source #
Instance details Defined in Test.StateMachine.Types.GenSym Methods fmap :: (a -> b) -> GenSym a -> GenSym b # (<$) :: a -> GenSym b -> GenSym a #
Applicative GenSym Source #
Instance details Defined in Test.StateMachine.Types.GenSym Methods pure :: a -> GenSym a # (<>) :: GenSym (a -> b) -> GenSym a -> GenSym b # liftA2 :: (a -> b -> c) -> GenSym a -> GenSym b -> GenSym c # (>) :: GenSym a -> GenSym b -> GenSym b # (<*) :: GenSym a -> GenSym b -> GenSym a #

genSym :: Typeable a => GenSym (Reference a Symbolic) Source #

module Test.StateMachine.Logic