quickcheck-state-machine-0.4.0: 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.Parallel

Description

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

Synopsis

Documentation

forAllParallelCommands Source #

Arguments

:: 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)

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. 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 #

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 runParallelCommands.

-> PropertyM m () 

Takes the output of parallel program runs and pretty prints a counterexample if any of the runs fail.