| 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.Parallel
Description
This module contains helpers for generating, shrinking, and checking parallel programs.
Synopsis
- forAllParallelCommands :: Testable prop => (Show (cmd Symbolic), Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> (ParallelCommands cmd -> prop) -> Property
- generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Gen (ParallelCommands cmd)
- shrinkParallelCommands :: forall cmd model m resp. Foldable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd -> [ParallelCommands cmd]
- validParallelCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (ParallelCommands cmd))
- prop_splitCombine :: [[Int]] -> Bool
- runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
- runParallelCommandsNTimes :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)]
- linearise :: forall model cmd m resp. StateMachine model cmd m resp -> History cmd resp -> Bool
- toBoxDrawings :: forall cmd resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> History cmd resp -> Doc
- prettyParallelCommands :: (MonadIO m, Foldable cmd) => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> [(History cmd resp, Bool)] -> PropertyM m ()
Documentation
generateParallelCommands :: forall model cmd m resp. (Foldable resp, Show (model Symbolic)) => (Generic1 cmd, GConName1 (Rep1 cmd)) => StateMachine model cmd m resp -> Gen (ParallelCommands cmd) Source #
shrinkParallelCommands :: forall cmd model m resp. Foldable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd -> [ParallelCommands cmd] Source #
Shrink a parallel program in a pre-condition and scope respecting way.
validParallelCommands :: forall model cmd m resp. (Foldable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd -> State (model Symbolic, Set Var, Counter) (Maybe (ParallelCommands cmd)) Source #
prop_splitCombine :: [[Int]] -> Bool Source #
runParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadBaseControl IO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Bool)] Source #
runParallelCommandsNTimes Source #
Arguments
| :: (Traversable cmd, Foldable resp) | |
| => (MonadCatch m, MonadBaseControl IO m) | |
| => Int | How many times to execute the parallel program. |
| -> StateMachine model cmd m resp | |
| -> ParallelCommands cmd | |
| -> PropertyM m [(History cmd resp, Bool)] |
linearise :: forall model cmd m resp. StateMachine model cmd m resp -> History cmd resp -> Bool 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 :: forall cmd resp. Foldable cmd => (Show (cmd Concrete), Show (resp Concrete)) => ParallelCommands cmd -> History cmd resp -> Doc Source #
Draw an ASCII diagram of the history of a parallel program. Useful for seeing how a race condition might have occured.
prettyParallelCommands Source #
Arguments
| :: (MonadIO m, Foldable cmd) | |
| => (Show (cmd Concrete), Show (resp Concrete)) | |
| => ParallelCommands cmd | |
| -> [(History cmd resp, Bool)] | Output of |
| -> PropertyM m () |
Takes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.