| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.QuickCheck.StateModel.Lockstep.Defaults
Description
Default implementations for the quickcheck-dynamic class methods
Intended for qualified import.
import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep
Synopsis
- initialState :: state -> Lockstep state
- nextState :: (InLockstep state, Typeable a) => Lockstep state -> LockstepAction state a -> Var a -> Lockstep state
- precondition :: InLockstep state => Lockstep state -> LockstepAction state a -> Bool
- arbitraryAction :: InLockstep state => VarContext -> Lockstep state -> Gen (Any (LockstepAction state))
- shrinkAction :: InLockstep state => VarContext -> Lockstep state -> LockstepAction state a -> [Any (LockstepAction state)]
- postcondition :: forall (m :: Type -> Type) state a. RunLockstep state m => (Lockstep state, Lockstep state) -> LockstepAction state a -> LookUp m -> Realized m a -> PostconditionM m Bool
- postconditionWith :: forall (m :: Type -> Type) state a. RunLockstep state m => Bool -> (Lockstep state, Lockstep state) -> LockstepAction state a -> LookUp m -> Realized m a -> PostconditionM m Bool
- monitoring :: forall (m :: Type -> Type) state a. RunLockstep state m => Proxy m -> (Lockstep state, Lockstep state) -> LockstepAction state a -> LookUp m -> Either (Error (Lockstep state)) (Realized m a) -> Property -> Property
Default implementations for methods of StateModel
initialState :: state -> Lockstep state Source #
Default implementation for initialState
nextState :: (InLockstep state, Typeable a) => Lockstep state -> LockstepAction state a -> Var a -> Lockstep state Source #
Default implementation for nextState
precondition :: InLockstep state => Lockstep state -> LockstepAction state a -> Bool Source #
Default implementation for precondition
The default precondition only checks that all variables have a value and that the operations on them are defined.
arbitraryAction :: InLockstep state => VarContext -> Lockstep state -> Gen (Any (LockstepAction state)) Source #
Default implementation for arbitraryAction
shrinkAction :: InLockstep state => VarContext -> Lockstep state -> LockstepAction state a -> [Any (LockstepAction state)] Source #
Default implementation for shrinkAction
Default implementations for methods of RunModel
postcondition :: forall (m :: Type -> Type) state a. RunLockstep state m => (Lockstep state, Lockstep state) -> LockstepAction state a -> LookUp m -> Realized m a -> PostconditionM m Bool Source #
Default implementation for postcondition
The default postcondition verifies that the real system and the model return the same results, up to " observability ".
Arguments
| :: forall (m :: Type -> Type) state a. RunLockstep state m | |
| => Bool | Verbose output |
| -> (Lockstep state, Lockstep state) | |
| -> LockstepAction state a | |
| -> LookUp m | |
| -> Realized m a | |
| -> PostconditionM m Bool |
Like postcondition, but with configurable verbosity.
By default, all states of the model are printed when a property counterexample is printed. If verbose output is enabled, the counterexample will also print all responses from the real system and the model.
monitoring :: forall (m :: Type -> Type) state a. RunLockstep state m => Proxy m -> (Lockstep state, Lockstep state) -> LockstepAction state a -> LookUp m -> Either (Error (Lockstep state)) (Realized m a) -> Property -> Property Source #
Orphan instances
| HasVariables (Lockstep state) Source # | Ignore variables for lockstep state. We largely ignore |
| InLockstep state => HasVariables (Action (Lockstep state) a) Source # | Do not ignore variables for lockstep actions.
|