| 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 err. Generator model act -> Precondition model act -> Transition' model act err -> Int -> StateT (model Symbolic) Gen (Program act)
- generateProgram' :: Generator model act -> Precondition model act -> Transition' model act err -> model Symbolic -> Gen (Program act)
- filterInvalid :: HFoldable act => Precondition model act -> Transition' model act err -> Program act -> State (model Symbolic, Set Var) (Program act)
- getUsedVars :: HFoldable act => act Symbolic a -> Set Var
- liftShrinkInternal :: Shrinker act -> Internal act -> [Internal act]
- validProgram :: forall act model err. HFoldable act => Precondition model act -> Transition' model act err -> model Symbolic -> Program act -> Bool
- shrinkProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition' model act err -> model Symbolic -> Program act -> [Program act]
- 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)
Documentation
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 #
Arguments
| :: HFoldable act | |
| => Precondition model act | |
| -> Transition' model act err | |
| -> 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.
validProgram :: forall act model err. HFoldable act => Precondition model act -> Transition' model act err -> model Symbolic -> Program act -> Bool 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.