Test.StateMachine.Types

Documentation

data StateMachine model cmd m resp

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

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)

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)

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)

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

newtype Commands cmd resp

Constructors

Commands

Fields

• unCommands :: [Command cmd resp]

Instances

(Eq (cmd Symbolic), Eq (resp Symbolic)) => Eq (Commands cmd resp)

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)

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)

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)

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)

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

lengthCommands :: Commands cmd resp -> Int

data ParallelCommandsF t cmd resp

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)

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)

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

data Pair a

Constructors

Pair

Fields

• proj1 :: !a
• proj2 :: !a

Instances

Functor Pair

Defined in Test.StateMachine.Types

Methods

fmap :: (a -> b) -> Pair a -> Pair b

(<$) :: a -> Pair b -> Pair a

Foldable Pair

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

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)

Defined in Test.StateMachine.Types

Methods

(==) :: Pair a -> Pair a -> Bool

(/=) :: Pair a -> Pair a -> Bool

Ord a => Ord (Pair a)

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)

Defined in Test.StateMachine.Types

Methods

showsPrec :: Int -> Pair a -> ShowS

show :: Pair a -> String

showList :: [Pair a] -> ShowS

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

Constructors

Ok

PreconditionFailed String

PostconditionFailed String

InvariantBroken String

ExceptionThrown String

MockSemanticsMismatch

Instances

Eq Reason

Defined in Test.StateMachine.Types

Methods

(==) :: Reason -> Reason -> Bool

(/=) :: Reason -> Reason -> Bool

Show Reason

Defined in Test.StateMachine.Types

Methods

showsPrec :: Int -> Reason -> ShowS

show :: Reason -> String

showList :: [Reason] -> ShowS

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