Test.StateMachine.Types

This module contains the main types exposed to the user. The module is perhaps best read indirectly, on a per need basis, via the main module Test.StateMachine.

Untyped actions

data Untyped (act :: (* -> *) -> * -> *) where

An untyped action is an action where the response type is hidden away using an existential type.

We need to hide the response type when generating actions, because in general the actions we want to generate will have different response types; and thus we can only type the generating function if we hide the response type.

Constructors

Untyped :: (Show resp, Typeable resp) => act Symbolic resp -> Untyped act

Type aliases

type StateMachine model act m = StateMachine' model act m Void

A (non-failing) state machine record bundles up all functionality needed to perform our tests.

stateMachine :: forall m model act. Functor m => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> Semantics act m -> Runner m -> StateMachine' model act m Void

Helper for lifting non-failing semantics to a possibly failing state machine record.

okTransition :: Transition model act -> Transition' model act Void

okPostcondition :: Postcondition model act -> Postcondition' model act Void

okSemantics :: Functor m => Semantics act m -> Semantics' act m Void

data StateMachine' model act m err

Same as above, but with possibly failing semantics.

Constructors

StateMachine

Fields

• generator' :: Generator model act
• shrinker' :: Shrinker act
• precondition' :: Precondition model act
• transition' :: Transition' model act err
• postcondition' :: Postcondition' model act err
• model' :: InitialModel model
• semantics' :: Semantics' act m err
• runner' :: Runner m

type Generator model act = model Symbolic -> Gen (Untyped act)

When generating actions we have access to a model containing symbolic references.

type Shrinker act = forall (v :: * -> *) resp. act v resp -> [act v resp]

Shrinking should preserve the response type of the action.

type Precondition model act = forall resp. model Symbolic -> act Symbolic resp -> Bool

Pre-conditions are checked while generating, at this stage we do not yet have access to concrete references.

type Transition model act = forall resp v. (Ord1 v, Show1 v) => model v -> act v resp -> v resp -> model v

The transition function must be polymorphic in the type of variables used, as it is used both while generating and executing.

type Transition' model act err = forall resp v. (Ord1 v, Show1 v) => model v -> act v resp -> Result err (v resp) -> model v

type Postcondition model act = forall resp. model Concrete -> act Concrete resp -> resp -> Bool

Post-conditions are checked after the actions have been executed and we got a response.

type Postcondition' model act err = forall resp. model Concrete -> act Concrete resp -> Result err resp -> Bool

type InitialModel m = forall (v :: * -> *). m v

The initial model is polymorphic in the type of references it uses, so that it can be used both in the pre- and the post-condition check.

data Result err resp

The result of executing an action.

Constructors

Success resp

Fail err

Instances

Functor (Result err)

Methods

fmap :: (a -> b) -> Result err a -> Result err b

(<$) :: a -> Result err b -> Result err a

ppResult :: (Show err, Show resp) => Result err resp -> String

type Semantics act m = forall resp. act Concrete resp -> m resp

When we execute our actions we have access to concrete references.

type Semantics' act m err = forall resp. act Concrete resp -> m (Result err resp)

type Runner m = m Property -> IO Property

How to run the monad used by the semantics.

data Reason

Constructors

Ok

PreconditionFailed

PostconditionFailed

Instances

Eq Reason

Methods

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

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

Show Reason

Methods

showsPrec :: Int -> Reason -> ShowS

show :: Reason -> String

showList :: [Reason] -> ShowS

Data type generic operations

module Test.StateMachine.Types.Generics

Higher-order functors, foldables and traversables

module Test.StateMachine.Types.HFunctor

References

module Test.StateMachine.Types.References