quickcheck-state-machine-0.3.1: Test monadic programs using state machine based models

Copyright(C) 2017 ATS Advanced Telematic Systems GmbH
LicenseBSD-style (see the file LICENSE)
MaintainerStevan Andjelkovic <stevan@advancedtelematic.com>
Stabilityprovisional
Portabilitynon-portable (GHC extensions)
Safe HaskellNone
LanguageHaskell2010

Test.StateMachine.Internal.Parallel

Description

This module contains helpers for generating, shrinking, and checking parallel programs.

Synopsis

Documentation

generateParallelProgram :: Generator model act -> Precondition model act -> Transition' model act err -> model Symbolic -> Gen (ParallelProgram act) Source #

Generate a parallel program whose actions all respect their pre-conditions.

shrinkParallelProgram :: forall act model err. HFoldable act => Eq (Untyped act) => Shrinker act -> Precondition model act -> Transition' model act err -> model Symbolic -> ParallelProgram act -> [ParallelProgram act] Source #

Shrink a parallel program in a pre-condition and scope respecting way.

validParallelProgram :: HFoldable act => Precondition model act -> Transition' model act err -> model Symbolic -> ParallelProgram act -> Bool Source #

executeParallelProgram :: forall m act err. MonadBaseControl IO m => HTraversable act => Show1 (act Symbolic) => Semantics' act m err -> 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 err -> Postcondition' model act err -> 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.