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 -> Gen (cmd Symbolic)
• distribution :: Maybe (Matrix Int)
• shrinker :: cmd Symbolic -> [cmd Symbolic]
• semantics :: cmd Concrete -> m (resp Concrete)
• mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)

data Command cmd

Constructors

Command !(cmd Symbolic) !(Set Var)

Instances

Show (cmd Symbolic) => Show (Command cmd)

Defined in Test.StateMachine.Types

Methods

showsPrec :: Int -> Command cmd -> ShowS

show :: Command cmd -> String

showList :: [Command cmd] -> ShowS

(Generic1 cmd, GConName1 (Rep1 cmd)) => GConName (Command cmd)

Defined in Test.StateMachine.ConstructorName

Methods

gconName :: Command cmd -> String

gconNames :: Proxy (Command cmd) -> [String]

newtype Commands cmd

Constructors

Commands

Fields

• unCommands :: [Command cmd]

Instances

Show (cmd Symbolic) => Show (Commands cmd)

Defined in Test.StateMachine.Types

Methods

showsPrec :: Int -> Commands cmd -> ShowS

show :: Commands cmd -> String

showList :: [Commands cmd] -> ShowS

Semigroup (Commands cmd)

Defined in Test.StateMachine.Types

Methods

(<>) :: Commands cmd -> Commands cmd -> Commands cmd

sconcat :: NonEmpty (Commands cmd) -> Commands cmd

stimes :: Integral b => b -> Commands cmd -> Commands cmd

Monoid (Commands cmd)

Defined in Test.StateMachine.Types

Methods

mempty :: Commands cmd

mappend :: Commands cmd -> Commands cmd -> Commands cmd

mconcat :: [Commands cmd] -> Commands cmd

lengthCommands :: Commands cmd -> Int

data ParallelCommandsF t cmd

Constructors

ParallelCommands

Fields

• prefix :: !(Commands cmd)
• suffixes :: [t (Commands cmd)]

Instances

(Show (cmd Symbolic), Show (t (Commands cmd))) => Show (ParallelCommandsF t cmd)

Defined in Test.StateMachine.Types

Methods

showsPrec :: Int -> ParallelCommandsF t cmd -> ShowS

show :: ParallelCommandsF t cmd -> String

showList :: [ParallelCommandsF t cmd] -> 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

data Reason

Constructors

Ok

PreconditionFailed

PostconditionFailed String

InvariantBroken String

ExceptionThrown

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

module Test.StateMachine.Types.Environment

module Test.StateMachine.Types.GenSym

module Test.StateMachine.Types.History

module Test.StateMachine.Types.References