| 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]
- executeProgram :: forall m act err model. Monad m => Show (Untyped act) => HTraversable act => StateMachine' model act err m -> Program act -> m (History act err, model Concrete, Property)
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.
executeProgram :: forall m act err model. Monad m => Show (Untyped act) => HTraversable act => StateMachine' model act err m -> Program act -> m (History act err, model Concrete, Property) Source #
Execute a program and return a history, the final model and a property which contains the information of whether the execution respects the state machine model or not.