quickcheck-state-machine-0.3.1: Test monadic programs using state machine based models

Copyright(C) 2017 ATS Advanced Telematic Systems GmbH
LicenseBSD-style (see the file LICENSE)
MaintainerStevan Andjelkovic <stevan@advancedtelematic.com>
Stabilityprovisional
Portabilitynon-portable (GHC extensions)
Safe HaskellNone
LanguageHaskell2010

Test.StateMachine.Internal.Sequential

Description

This module contains helpers for generating, shrinking, and checking sequential programs.

Synopsis

Documentation

generateProgram Source #

Arguments

:: Generator model act 
-> Precondition model act 
-> Transition' model act err 
-> Int

Name supply for symbolic variables.

-> StateT (model Symbolic) Gen (Program act) 

Generate programs whose actions all respect their pre-conditions.

generateProgram' :: Generator model act -> Precondition model act -> Transition' model act err -> model Symbolic -> Gen (Program act) Source #

filterInvalid Source #

Arguments

:: HFoldable act 
=> Precondition model act 
-> Transition' model act err 
-> Program act 
-> State (model Symbolic, Set Var) (Program act)

Where Set Var is the scope.

Filter out invalid actions from a program. An action is invalid if either its pre-condition doesn't hold, or it uses references that are not in scope.

getUsedVars :: HFoldable act => act Symbolic a -> Set Var Source #

Returns the set of references an action uses.

liftShrinkInternal :: Shrinker act -> Internal act -> [Internal act] Source #

Given a shrinker of typed actions we can lift it to a shrinker of internal actions.

validProgram :: forall act model err. HFoldable act => Precondition model act -> Transition' model act err -> model Symbolic -> Program act -> Bool Source #

shrinkProgram Source #

Arguments

:: HFoldable act 
=> Shrinker act 
-> Precondition model act 
-> Transition' model act err 
-> model Symbolic 
-> Program act

Program to shrink.

-> [Program act] 

Shrink a program in a pre-condition and scope respecting way.

executeProgram :: forall m act model err. Monad m => Typeable err => Show1 (act Symbolic) => Show err => HTraversable act => StateMachine' model act m err -> Program act -> m (History act err, model Concrete, Reason) Source #

Execute a program and return a history, the final model and a result which contains the information of whether the execution respects the state machine model or not.