| 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 m act err. MonadBaseControl IO m => HTraversable act => Show (Untyped act) => Semantics act err m -> ParallelProgram act -> m (History act err)
- linearise :: forall model act err. Transition model act -> Postcondition model act -> InitialModel model -> History act err -> Property
- toBoxDrawings :: HFoldable act => ParallelProgram act -> History act err -> Doc
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 m act err. MonadBaseControl IO m => HTraversable act => Show (Untyped act) => Semantics act err m -> ParallelProgram act -> m (History act err) 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.
linearise :: forall model act err. Transition model act -> Postcondition model act -> InitialModel model -> History act err -> Property Source #
Try to linearise a history of a parallel program execution using a sequential model. See the *Linearizability: a correctness condition for concurrent objects* paper linked to from the README for more info.
toBoxDrawings :: HFoldable act => ParallelProgram act -> History act err -> Doc Source #
Draw an ASCII diagram of the history of a parallel program. Useful for seeing how a race condition might have occured.