| 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.Types
Contents
Description
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.
- data Untyped act where
- type StateMachine model act m = StateMachine' model act Void m
- stateMachine :: Functor m => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> (forall resp. act Concrete resp -> m resp) -> Runner m -> StateMachine' model act Void m
- data StateMachine' model act err m = StateMachine {
- generator' :: Generator model act
- shrinker' :: Shrinker act
- precondition' :: Precondition model act
- transition' :: Transition model act
- postcondition' :: Postcondition model act
- model' :: InitialModel model
- semantics' :: Semantics act err m
- runner' :: Runner m
- type Generator model act = model Symbolic -> Gen (Untyped act)
- type Shrinker act = forall v resp. act v resp -> [act v resp]
- type Precondition model act = forall resp. model Symbolic -> act Symbolic resp -> Bool
- type Transition model act = forall resp v. Ord1 v => model v -> act v resp -> v resp -> model v
- type Postcondition model act = forall resp. model Concrete -> act Concrete resp -> resp -> Property
- type InitialModel m = forall v. m v
- data Result resp err
- type Semantics act err m = forall resp. act Concrete resp -> m (Result resp err)
- type Runner m = m Property -> IO Property
- module Test.StateMachine.Types.Generics
- module Test.StateMachine.Types.HFunctor
- module Test.StateMachine.Types.References
Untyped actions
data Untyped act where Source #
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.
Type aliases
type StateMachine model act m = StateMachine' model act Void m Source #
A (non-failing) state machine record bundles up all functionality needed to perform our tests.
stateMachine :: Functor m => Generator model act -> Shrinker act -> Precondition model act -> Transition model act -> Postcondition model act -> InitialModel model -> (forall resp. act Concrete resp -> m resp) -> Runner m -> StateMachine' model act Void m Source #
Helper for lifting non-failing semantics to a possibly failing state machine record.
data StateMachine' model act err m Source #
Same as above, but with possibly failing semantics.
Constructors
| StateMachine | |
Fields
| |
type Generator model act = model Symbolic -> Gen (Untyped act) Source #
When generating actions we have access to a model containing symbolic references.
type Shrinker act = forall v resp. act v resp -> [act v resp] Source #
Shrinking should preserve the response type of the action.
type Precondition model act = forall resp. model Symbolic -> act Symbolic resp -> Bool Source #
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 => model v -> act v resp -> v resp -> model v Source #
The transition function must be polymorphic in the type of variables used, as it is used both while generating and executing.
type Postcondition model act = forall resp. model Concrete -> act Concrete resp -> resp -> Property Source #
Post-conditions are checked after the actions have been executed and we got a response.
type InitialModel m = forall v. m v Source #
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.
type Semantics act err m = forall resp. act Concrete resp -> m (Result resp err) Source #
When we execute our actions we have access to concrete references.