Test.StateMachine.Internal.Parallel

This module contains the building blocks needed to implement the parallelProperty helper.

Documentation

liftGenFork

Arguments

:: Ord ix

=> SingKind ix

=> DemoteRep ix ~ ix

=> IxTraversable cmd

=> HasResponse cmd

=> Gen (Untyped cmd (RefPlaceholder ix))

Generator to be lifted.

-> Gen (Fork [IntRefed cmd])

Lift a generator of untyped commands with reference placeholders into a generator of forks of untyped internal commands.

liftGenFork' :: Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -> genState -> Gen (Fork [IntRefed cmd])

liftShrinkFork

Arguments

:: IxFoldable cmd

=> HasResponse cmd

=> (forall resp. Shrinker (cmd ConstIntRef resp))

Shrinker to be lifted.

-> Shrinker (Fork [IntRefed cmd])

Lift a shrinker of internal commands into a shrinker of forks of untyped internal commands.

liftSemFork

Arguments

:: forall (ix :: Type) (cmd :: Signature ix) (refs :: TyFun ix Type -> Type). SDecide ix

=> IxFunctor cmd

=> HasResponse cmd

=> (forall resp. cmd refs resp -> IO (Response_ refs resp))

Semantics to be lifted.

-> Fork [IntRefed cmd]

-> IO (History cmd)

Lift the semantics of a single typed command into a semantics for forks of untyped internal commands. The prefix of the fork is executed sequentially, while the two suffixes are executed in parallel, and the result (or trace) is collected in a so called history.

checkParallelInvariant :: (ShowCmd cmd, IxFunctor cmd, HasResponse cmd) => StateMachineModel model cmd -> History cmd -> PropertyM IO ()

Check if a history can be linearised.