| 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 |
Test.StateMachine.Internal.Sequential
Description
This module contains the building blocks needed to implement the
sequentialProperty helper.
- liftGen :: forall ix cmd. Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => Gen (Untyped cmd (RefPlaceholder ix)) -> Pid -> Map ix Int -> Gen ([IntRefed cmd], Map ix Int)
- liftGen' :: forall ix cmd genState. Ord ix => SingKind ix => DemoteRep ix ~ ix => IxTraversable cmd => HasResponse cmd => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) -> genState -> Pid -> Map ix Int -> Gen (([IntRefed cmd], genState), Map ix Int)
- liftShrinker :: (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker (IntRefed cmd)
- liftShrink :: IxFoldable cmd => HasResponse cmd => (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker [IntRefed cmd]
- liftSem :: forall ix cmd refs resp m. SDecide ix => Monad m => IxFunctor cmd => HasResponse cmd => (cmd refs resp -> m (Response_ refs resp)) -> cmd ConstIntRef resp -> MayResponse_ ConstIntRef resp -> StateT (IxMap ix IntRef refs) m (Response_ ConstIntRef resp)
- removeCommands :: forall cmd. IxFoldable cmd => HasResponse cmd => IntRefed cmd -> [IntRefed cmd] -> [IntRefed cmd]
- collectStats :: [a] -> Property -> Property
- checkSequentialInvariant :: ShowCmd cmd => Monad m => SDecide ix => IxFunctor cmd => Show (model ConstIntRef) => HasResponse cmd => StateMachineModel model cmd -> model ConstIntRef -> (forall resp. model ConstIntRef -> MayResponse_ ConstIntRef resp -> cmd refs resp -> m (Response_ refs resp)) -> [IntRefed cmd] -> PropertyM (StateT (IxMap ix IntRef refs) m) ()
Documentation
Arguments
| :: Ord ix | |
| => SingKind ix | |
| => DemoteRep ix ~ ix | |
| => IxTraversable cmd | |
| => HasResponse cmd | |
| => Gen (Untyped cmd (RefPlaceholder ix)) | Generator to be lifted. |
| -> Pid | Process id. |
| -> Map ix Int | Keeps track of how many
refereces of sort |
| -> Gen ([IntRefed cmd], Map ix Int) |
Lift a generator of untyped commands with reference placeholders into a generator of lists of untyped internal commands.
Arguments
| :: Ord ix | |
| => SingKind ix | |
| => DemoteRep ix ~ ix | |
| => IxTraversable cmd | |
| => HasResponse cmd | |
| => StateT genState Gen (Untyped cmd (RefPlaceholder ix)) | Stateful generator to be lifted. |
| -> genState | Initial generator state. |
| -> Pid | |
| -> Map ix Int | |
| -> Gen (([IntRefed cmd], genState), Map ix Int) |
Same as the above, but for stateful generators.
liftShrinker :: (forall resp. Shrinker (cmd ConstIntRef resp)) -> Shrinker (IntRefed cmd) Source #
A shrinker of typed commands can be lifted to a shrinker of untyped commands.
Arguments
| :: IxFoldable cmd | |
| => HasResponse cmd | |
| => (forall resp. Shrinker (cmd ConstIntRef resp)) | Shrinker to be lifted. |
| -> Shrinker [IntRefed cmd] |
Lift a shrinker of internal commands into a shrinker of lists of untyped internal commands.
Arguments
| :: SDecide ix | |
| => Monad m | |
| => IxFunctor cmd | |
| => HasResponse cmd | |
| => (cmd refs resp -> m (Response_ refs resp)) | Semantics to be lifted. |
| -> cmd ConstIntRef resp | |
| -> MayResponse_ ConstIntRef resp | |
| -> StateT (IxMap ix IntRef refs) m (Response_ ConstIntRef resp) |
Lift semantics of typed commands with external references, into semantics for typed commands with internal references.
Arguments
| :: IxFoldable cmd | |
| => HasResponse cmd | |
| => IntRefed cmd | If this command returns a reference, then |
| -> [IntRefed cmd] | remove all commands that use that reference in this list. If a command we remove uses another reference, then we proceed recursively. |
| -> [IntRefed cmd] |
Remove commands that uses a reference.
collectStats :: [a] -> Property -> Property Source #
Collects length statistics about the input list.
checkSequentialInvariant Source #
Arguments
| :: ShowCmd cmd | |
| => Monad m | |
| => SDecide ix | |
| => IxFunctor cmd | |
| => Show (model ConstIntRef) | |
| => HasResponse cmd | |
| => StateMachineModel model cmd | |
| -> model ConstIntRef | |
| -> (forall resp. model ConstIntRef -> MayResponse_ ConstIntRef resp -> cmd refs resp -> m (Response_ refs resp)) | |
| -> [IntRefed cmd] | List of commands to check. |
| -> PropertyM (StateT (IxMap ix IntRef refs) m) () |
Check that the pre- and post-conditions hold in a sequential way.