| 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.Internal.Sequential
Description
This module contains helpers for generating, shrinking, and checking sequential programs.
- generateProgram :: forall model act. Generator model act -> Precondition model act -> Transition model act -> Int -> StateT (model Symbolic) Gen (Program act)
- filterInvalid :: HFoldable act => Precondition model act -> Transition model act -> Program act -> State (model Symbolic, Set Var) (Program act)
- getUsedVars :: HFoldable act => act Symbolic a -> Set Var
- liftShrinkInternal :: Shrinker act -> Internal act -> [Internal act]
- shrinkProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> Program act -> [Program act]
- checkProgram :: Monad m => HFunctor act => Precondition model act -> Transition model act -> Postcondition model act -> model Symbolic -> model Concrete -> Semantics act m -> Program act -> PropertyM (StateT Environment m) ()
Documentation
Arguments
| :: Generator model act | |
| -> Precondition model act | |
| -> Transition model act | |
| -> Int | Name supply for symbolic variables. |
| -> StateT (model Symbolic) Gen (Program act) |
Generate programs whose actions all respect their pre-conditions.
Arguments
| :: HFoldable act | |
| => Precondition model act | |
| -> Transition model act | |
| -> Program act | |
| -> State (model Symbolic, Set Var) (Program act) | Where |
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.
Arguments
| :: HFoldable act | |
| => Shrinker act | |
| -> Precondition model act | |
| -> Transition model act | |
| -> model Symbolic | |
| -> Program act | Program to shrink. |
| -> [Program act] |
Shrink a program in a pre-condition and scope respecting way.
Arguments
| :: Monad m | |
| => HFunctor act | |
| => Precondition model act | |
| -> Transition model act | |
| -> Postcondition model act | |
| -> model Symbolic | The model with symbolic references is used to check pre-conditions against. |
| -> model Concrete | While the one with concrete referenes is used for checking post-conditions. |
| -> Semantics act m | |
| -> Program act | |
| -> PropertyM (StateT Environment m) () |
For each action in a program, check that if the pre-condition holds for the action, then so does the post-condition.