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 |
This module contains the building blocks needed to implement the
parallelProperty
helper.
- liftGenFork :: Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => Gen (Untyped cmd (RefPlaceholder ix)) -> Gen (Fork [IntRefed cmd])
- 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 :: forall cmd. IxFoldable cmd => HasResponse cmd => (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker (Fork [IntRefed cmd])
- liftSemFork :: forall ix cmd refs. SDecide ix => IxFunctor cmd => HasResponse cmd => (forall resp. cmd refs resp -> IO (Response_ refs resp)) -> Fork [IntRefed cmd] -> IO (History cmd)
- checkParallelInvariant :: (ShowCmd cmd, IxFunctor cmd, HasResponse cmd) => StateMachineModel model cmd -> History cmd -> PropertyM IO ()
Documentation
:: 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]) Source #
:: 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.
:: 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 () Source #
Check if a history can be linearised.