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

Test.StateMachine.Types

Description

Synopsis

data StateMachine model cmd m resp = StateMachine {
- initModel :: forall r. model r
- transition :: forall r. (Show1 r, Ord1 r) => model r -> cmd r -> resp r -> model r
- precondition :: model Symbolic -> cmd Symbolic -> Logic
- postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
- invariant :: Maybe (model Concrete -> Logic)
- generator :: model Symbolic -> Maybe (Gen (cmd Symbolic))
- shrinker :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
- semantics :: cmd Concrete -> m (resp Concrete)
- mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
- cleanup :: model Concrete -> m ()
}
data Command cmd resp = Command !(cmd Symbolic) !(resp Symbolic) ![Var]
getCommand :: Command cmd resp -> cmd Symbolic
newtype Commands cmd resp = Commands {
- unCommands :: [Command cmd resp]
}
type NParallelCommands = ParallelCommandsF []
lengthCommands :: Commands cmd resp -> Int
data ParallelCommandsF t cmd resp = ParallelCommands {
- prefix :: !(Commands cmd resp)
- suffixes :: [t (Commands cmd resp)]
}
type ParallelCommands = ParallelCommandsF Pair
data Pair a = Pair {
- proj1 :: !a
- proj2 :: !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
- | PreconditionFailed String
- | PostconditionFailed String
- | InvariantBroken String
- | ExceptionThrown String
- | MockSemanticsMismatch
isOK :: Reason -> Bool
noCleanup :: Monad m => model Concrete -> m ()
module Test.StateMachine.Types.Environment
module Test.StateMachine.Types.GenSym
module Test.StateMachine.Types.History
module Test.StateMachine.Types.References

Documentation

data StateMachine model cmd m resp Source #

Constructors

StateMachine

Fields

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

data Command cmd resp Source #

Previously symbolically executed command

Invariant: the variables must be the variables in the response.

Constructors

Command !(cmd Symbolic) !(resp Symbolic) ![Var]

Instances

(Eq (cmd Symbolic), Eq (resp Symbolic)) => Eq (Command cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods (==) :: Command cmd resp -> Command cmd resp -> Bool # (/=) :: Command cmd resp -> Command cmd resp -> Bool #
(Read (cmd Symbolic), Read (resp Symbolic)) => Read (Command cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods readsPrec :: Int -> ReadS (Command cmd resp) # readList :: ReadS [Command cmd resp] # readPrec :: ReadPrec (Command cmd resp) # readListPrec :: ReadPrec [Command cmd resp] #
(Show (cmd Symbolic), Show (resp Symbolic)) => Show (Command cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods showsPrec :: Int -> Command cmd resp -> ShowS # show :: Command cmd resp -> String # showList :: [Command cmd resp] -> ShowS #

getCommand :: Command cmd resp -> cmd Symbolic Source #

newtype Commands cmd resp Source #

Constructors

Commands
Fields unCommands :: [Command cmd resp]

Instances

(Eq (cmd Symbolic), Eq (resp Symbolic)) => Eq (Commands cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods (==) :: Commands cmd resp -> Commands cmd resp -> Bool # (/=) :: Commands cmd resp -> Commands cmd resp -> Bool #
(Read (cmd Symbolic), Read (resp Symbolic)) => Read (Commands cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods readsPrec :: Int -> ReadS (Commands cmd resp) # readList :: ReadS [Commands cmd resp] # readPrec :: ReadPrec (Commands cmd resp) # readListPrec :: ReadPrec [Commands cmd resp] #
(Show (cmd Symbolic), Show (resp Symbolic)) => Show (Commands cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods showsPrec :: Int -> Commands cmd resp -> ShowS # show :: Commands cmd resp -> String # showList :: [Commands cmd resp] -> ShowS #
Semigroup (Commands cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods (<>) :: Commands cmd resp -> Commands cmd resp -> Commands cmd resp # sconcat :: NonEmpty (Commands cmd resp) -> Commands cmd resp # stimes :: Integral b => b -> Commands cmd resp -> Commands cmd resp #
Monoid (Commands cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods mempty :: Commands cmd resp # mappend :: Commands cmd resp -> Commands cmd resp -> Commands cmd resp # mconcat :: [Commands cmd resp] -> Commands cmd resp #

type NParallelCommands = ParallelCommandsF [] Source #

lengthCommands :: Commands cmd resp -> Int Source #

data ParallelCommandsF t cmd resp Source #

Constructors

ParallelCommands
Fields prefix :: !(Commands cmd resp) suffixes :: [t (Commands cmd resp)]

Instances

(Eq (cmd Symbolic), Eq (resp Symbolic), Eq (t (Commands cmd resp))) => Eq (ParallelCommandsF t cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods (==) :: ParallelCommandsF t cmd resp -> ParallelCommandsF t cmd resp -> Bool # (/=) :: ParallelCommandsF t cmd resp -> ParallelCommandsF t cmd resp -> Bool #
(Show (cmd Symbolic), Show (resp Symbolic), Show (t (Commands cmd resp))) => Show (ParallelCommandsF t cmd resp) Source #
Instance details Defined in Test.StateMachine.Types Methods showsPrec :: Int -> ParallelCommandsF t cmd resp -> ShowS # show :: ParallelCommandsF t cmd resp -> String # showList :: [ParallelCommandsF t cmd resp] -> ShowS #

type ParallelCommands = ParallelCommandsF Pair Source #

data Pair a Source #

Constructors

Pair
Fields proj1 :: !a proj2 :: !a

Instances

Functor Pair Source #
Instance details Defined in Test.StateMachine.Types Methods fmap :: (a -> b) -> Pair a -> Pair b # (<$) :: a -> Pair b -> Pair a #
Foldable Pair Source #
Instance details Defined in Test.StateMachine.Types Methods fold :: Monoid m => Pair m -> m # foldMap :: Monoid m => (a -> m) -> Pair a -> m # foldr :: (a -> b -> b) -> b -> Pair a -> b # foldr' :: (a -> b -> b) -> b -> Pair a -> b # foldl :: (b -> a -> b) -> b -> Pair a -> b # foldl' :: (b -> a -> b) -> b -> Pair a -> b # foldr1 :: (a -> a -> a) -> Pair a -> a # foldl1 :: (a -> a -> a) -> Pair a -> a # toList :: Pair a -> [a] # null :: Pair a -> Bool # length :: Pair a -> Int # elem :: Eq a => a -> Pair a -> Bool # maximum :: Ord a => Pair a -> a # minimum :: Ord a => Pair a -> a # sum :: Num a => Pair a -> a # product :: Num a => Pair a -> a #
Traversable Pair Source #
Instance details Defined in Test.StateMachine.Types Methods traverse :: Applicative f => (a -> f b) -> Pair a -> f (Pair b) # sequenceA :: Applicative f => Pair (f a) -> f (Pair a) # mapM :: Monad m => (a -> m b) -> Pair a -> m (Pair b) # sequence :: Monad m => Pair (m a) -> m (Pair a) #
Eq a => Eq (Pair a) Source #
Instance details Defined in Test.StateMachine.Types Methods (==) :: Pair a -> Pair a -> Bool # (/=) :: Pair a -> Pair a -> Bool #
Ord a => Ord (Pair a) Source #
Instance details Defined in Test.StateMachine.Types Methods compare :: Pair a -> Pair a -> Ordering # (<) :: Pair a -> Pair a -> Bool # (<=) :: Pair a -> Pair a -> Bool # (>) :: Pair a -> Pair a -> Bool # (>=) :: Pair a -> Pair a -> Bool # max :: Pair a -> Pair a -> Pair a # min :: Pair a -> Pair a -> Pair a #
Show a => Show (Pair a) Source #
Instance details Defined in Test.StateMachine.Types Methods showsPrec :: Int -> Pair a -> ShowS # show :: Pair a -> String # showList :: [Pair a] -> ShowS #

fromPair :: Pair a -> (a, a) Source #

toPair :: (a, a) -> Pair a Source #

fromPair' :: ParallelCommandsF Pair cmd resp -> ParallelCommandsF [] cmd resp Source #

toPairUnsafe' :: ParallelCommandsF [] cmd resp -> ParallelCommandsF Pair cmd resp Source #

data Reason Source #

Constructors

Ok
PreconditionFailed String
PostconditionFailed String
InvariantBroken String
ExceptionThrown String
MockSemanticsMismatch

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 #

isOK :: Reason -> Bool Source #

noCleanup :: Monad m => model Concrete -> m () Source #

module Test.StateMachine.Types.Environment

module Test.StateMachine.Types.GenSym

module Test.StateMachine.Types.History

module Test.StateMachine.Types.References