Copyright  (C) 2017 ATS Advanced Telematic Systems GmbH 

License  BSDstyle (see the file LICENSE) 
Maintainer  Stevan Andjelkovic <stevan@advancedtelematic.com> 
Stability  provisional 
Portability  nonportable (GHC extensions) 
Safe Haskell  None 
Language  Haskell2010 
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 m Void
 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
 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 = StateMachine {
 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)
 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, Show1 v) => model v > act v resp > v resp > model v
 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
 type Postcondition' model act err = forall resp. model Concrete > act Concrete resp > Result err resp > Bool
 type InitialModel m = forall (v :: * > *). m v
 data Result err resp
 ppResult :: (Show err, Show resp) => Result err resp > String
 type Semantics act m = forall resp. act Concrete resp > m resp
 type Semantics' act m err = forall resp. act Concrete resp > m (Result err resp)
 type Runner m = m Property > IO Property
 data Reason
 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 m Void Source #
A (nonfailing) 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 Source #
Helper for lifting nonfailing semantics to a possibly failing state machine record.
okTransition :: Transition model act > Transition' model act Void Source #
okPostcondition :: Postcondition model act > Postcondition' model act Void Source #
okSemantics :: Functor m => Semantics act m > Semantics' act m Void Source #
data StateMachine' model act m err Source #
Same as above, but with possibly failing semantics.
StateMachine  

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 #
Preconditions 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 Source #
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 Source #
type Postcondition model act = forall resp. model Concrete > act Concrete resp > resp > Bool Source #
Postconditions 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 Source #
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 postcondition check.
The result of executing an action.
type Semantics act m = forall resp. act Concrete resp > m resp Source #
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) Source #