| 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.Parallel
Description
This module contains helpers for generating, shrinking, and checking parallel programs.
- generateParallelProgram :: Generator model act -> Precondition model act -> Transition model act -> model Symbolic -> Gen (ParallelProgram act)
- shrinkParallelProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> ParallelProgram act -> [ParallelProgram act]
- executeParallelProgram :: forall act. HTraversable act => Show (Untyped act) => Semantics act IO -> ParallelProgram act -> IO (History act)
- checkParallelProgram :: HFoldable act => Transition model act -> Postcondition model act -> InitialModel model -> ParallelProgram act -> History act -> Property
- newtype History act = History {
- unHistory :: History' act
Documentation
generateParallelProgram :: Generator model act -> Precondition model act -> Transition model act -> model Symbolic -> Gen (ParallelProgram act) Source #
Generate a parallel program whose actions all respect their pre-conditions.
shrinkParallelProgram :: HFoldable act => Shrinker act -> Precondition model act -> Transition model act -> model Symbolic -> ParallelProgram act -> [ParallelProgram act] Source #
Shrink a parallel program in a pre-condition and scope respecting way.
executeParallelProgram :: forall act. HTraversable act => Show (Untyped act) => Semantics act IO -> ParallelProgram act -> IO (History act) Source #
Run a parallel program, by first executing the prefix sequentially and then the suffixes in parallel, and return the history (or trace) of the execution.
Arguments
| :: HFoldable act | |
| => Transition model act | |
| -> Postcondition model act | |
| -> InitialModel model | |
| -> ParallelProgram act | |
| -> History act | History to be checked. |
| -> Property |
Check if a history from a parallel execution can be linearised.