Copyright | (C) 2017 ATS Advanced Telematic Systems GmbH |
---|---|
License | BSD-style (see the file LICENSE) |
Maintainer | Stevan Andjelkovic <stevan.andjelkovic@here.com> |
Stability | provisional |
Portability | non-portable (GHC extensions) |
Safe Haskell | None |
Language | Haskell2010 |
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)) => (Traversable 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. Traversable cmd => Foldable resp => StateMachine model cmd m resp -> ParallelCommands cmd -> [ParallelCommands cmd]
- validParallelCommands :: forall model cmd m resp. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd -> State (model Symbolic, Map Var Var, Counter) (Maybe (ParallelCommands cmd))
- prop_splitCombine :: [[Int]] -> Bool
- runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)]
- runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => Int -> StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)]
- executeParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> m (History cmd resp, Reason)
- linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic
- 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, Logic)] -> PropertyM m ()
Documentation
forAllParallelCommands Source #
:: Testable prop | |
=> (Show (cmd Symbolic), Show (model Symbolic)) | |
=> (Generic1 cmd, GConName1 (Rep1 cmd)) | |
=> (Traversable cmd, Foldable resp) | |
=> StateMachine model cmd m resp | |
-> (ParallelCommands cmd -> prop) | Predicate. |
-> 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) Source #
shrinkParallelCommands :: forall cmd model m resp. Traversable 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. (Traversable cmd, Foldable resp) => StateMachine model cmd m resp -> ParallelCommands cmd -> State (model Symbolic, Map Var Var, Counter) (Maybe (ParallelCommands cmd)) Source #
prop_splitCombine :: [[Int]] -> Bool Source #
runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete)) => (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> PropertyM m [(History cmd resp, Logic)] Source #
runParallelCommandsNTimes Source #
:: (Show (cmd Concrete), Show (resp Concrete)) | |
=> (Traversable cmd, Foldable resp) | |
=> (MonadCatch m, MonadUnliftIO m) | |
=> Int | How many times to execute the parallel program. |
-> StateMachine model cmd m resp | |
-> ParallelCommands cmd | |
-> PropertyM m [(History cmd resp, Logic)] |
executeParallelCommands :: (Traversable cmd, Foldable resp) => (MonadCatch m, MonadUnliftIO m) => StateMachine model cmd m resp -> ParallelCommands cmd -> m (History cmd resp, Reason) Source #
linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete)) => StateMachine model cmd m resp -> History cmd resp -> Logic 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 #
:: (MonadIO m, Foldable cmd) | |
=> (Show (cmd Concrete), Show (resp Concrete)) | |
=> ParallelCommands cmd | |
-> [(History cmd resp, Logic)] | Output of |
-> PropertyM m () |
Takes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.