Safe Haskell	None
Language	Haskell2010

Test.QuickCheck.StateModel.Lockstep

Contents

Main abstraction
- Convenience aliases
Variable context
Variables
- Operations

Description

Lockstep-style testing using quickcheck-dynamic

See https://well-typed.com/blog/2022/09/lockstep-with-quickcheck-dynamic/ for a tutorial.

This module is intended for unqualified import alongside imports of Test.QuickCheck.StateModel.

import Test.QuickCheck.StateModel
import Test.QuickCheck.StateModel.Lockstep
import Test.QuickCheck.StateModel.Lockstep.Run      qualified as Lockstep
import Test.QuickCheck.StateModel.Lockstep.Defaults qualified as Lockstep

Synopsis

data Lockstep state
getModel :: Lockstep state -> state
class (StateModel (Lockstep state), Typeable state, InterpretOp (ModelOp state) (ModelValue state), forall a. Show (ModelValue state a), forall a. Eq (Observable state a), forall a. Show (Observable state a)) => InLockstep state where
- data ModelValue state a
- data Observable state a
- type ModelOp state :: Type -> Type -> Type
- observeModel :: ModelValue state a -> Observable state a
- usedVars :: LockstepAction state a -> [AnyGVar (ModelOp state)]
- modelNextState :: LockstepAction state a -> ModelVarContext state -> state -> (ModelValue state a, state)
- arbitraryWithVars :: ModelVarContext state -> state -> Gen (Any (LockstepAction state))
- shrinkWithVars :: ModelVarContext state -> state -> LockstepAction state a -> [Any (LockstepAction state)]
- tagStep :: (state, state) -> LockstepAction state a -> ModelValue state a -> [String]
class (InLockstep state, RunModel (Lockstep state) m) => RunLockstep state (m :: Type -> Type) where
- observeReal :: Proxy m -> LockstepAction state a -> Realized m a -> Observable state a
- showRealResponse :: Proxy m -> LockstepAction state a -> Maybe (Dict (Show (Realized m a)))
type LockstepAction state = Action (Lockstep state)
type ModelFindVariables state = forall a. Typeable a => Proxy a -> [GVar (ModelOp state) a]
type ModelLookUp state = forall a. ModelVar state a -> ModelValue state a
type ModelShrinkVar state = forall a. ModelVar state a -> [ModelVar state a]
type ModelVar state = GVar (ModelOp state)
type RealLookUp (m :: Type -> Type) (op :: Type -> Type -> Type) = forall a. Proxy m -> LookUp m -> GVar op a -> Realized m a
type ModelVarContext state = EnvF (ModelValue state)
lookupVar :: InLockstep state => ModelVarContext state -> ModelLookUp state
findVars :: InLockstep state => ModelVarContext state -> ModelFindVariables state
shrinkVar :: (Typeable state, InterpretOp (ModelOp state) (ModelValue state)) => ModelVarContext state -> ModelShrinkVar state
realLookupVar :: forall (op :: Type -> Type -> Type) (m :: Type -> Type). InterpretOp op (WrapRealized m) => RealLookUp m op
data GVar (op :: Type -> Type -> Type) f
data AnyGVar (op :: Type -> Type -> Type) where
- SomeGVar :: forall (op :: Type -> Type -> Type) y. GVar op y -> AnyGVar op
unsafeMkGVar :: Typeable a => Var a -> op a b -> GVar op b
mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b
class Operation (op :: Type -> Type -> Type) where
- opIdentity :: op a a
class Operation op => InterpretOp (op :: Type -> Type -> Type) (f :: Type -> Type) where
- intOp :: op a b -> f a -> Maybe (f b)

Main abstraction

data Lockstep state Source #

Instances

Instances details

Show state => Show (Lockstep state) Source #	The `Show` instance does not show the internal environment
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.API Methods showsPrec :: Int -> Lockstep state -> ShowS # show :: Lockstep state -> String # showList :: [Lockstep state] -> ShowS #
HasVariables (Lockstep state) Source #	Ignore variables for lockstep state. We largely ignore `quickcheck-dynamic`'s variables in the lockstep framework, since it does its own accounting of model variables.
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Defaults Methods getAllVariables :: Lockstep state -> Set (Any Var) #
InLockstep state => HasVariables (Action (Lockstep state) a) Source #	Do not ignore variables for lockstep actions. `quickcheck-dynamic` prints counterexamples as code that is more or less runnable, which requires a sensible `HasVariables` instance for lockstep actions.
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Defaults Methods getAllVariables :: Action (Lockstep state) a -> Set (Any Var) #

getModel :: Lockstep state -> state Source #

Inspect the model that resides inside the Lockstep state

class (StateModel (Lockstep state), Typeable state, InterpretOp (ModelOp state) (ModelValue state), forall a. Show (ModelValue state a), forall a. Eq (Observable state a), forall a. Show (Observable state a)) => InLockstep state where Source #

Minimal complete definition

observeModel, usedVars, modelNextState, arbitraryWithVars

Associated Types

data ModelValue state a Source #

Values in the mock environment

ModelValue witnesses the relation between values returned by the real system and values returned by the model.

In most cases, we expect the real system and the model to return the same value. However, for some things we must allow them to diverge: consider file handles for example.

data Observable state a Source #

Observable responses

The real system returns values of type a, and the model returns values of type MockValue a. Observable a defines the parts of those results that expect to be the same for both.

type ModelOp state :: Type -> Type -> Type Source #

Type of operations required on the results of actions

Whenever an action has a result of type a, but we later need a variable of type b, we need a constructor

GetB :: ModelOp state a b

in the ModelOp type. For many tests, the standard Op type will suffice, but not always.

type ModelOp state = Op

Methods

observeModel :: ModelValue state a -> Observable state a Source #

Extract the observable part of a response from the model

usedVars :: LockstepAction state a -> [AnyGVar (ModelOp state)] Source #

All variables required by a command

modelNextState :: LockstepAction state a -> ModelVarContext state -> state -> (ModelValue state a, state) Source #

Step the model

The order of the arguments mimicks perform.

arbitraryWithVars :: ModelVarContext state -> state -> Gen (Any (LockstepAction state)) Source #

Generate an arbitrary action, given a variable context

shrinkWithVars :: ModelVarContext state -> state -> LockstepAction state a -> [Any (LockstepAction state)] Source #

Shrink an action, given a variable context

This is optional; without an implementation of shrinkWithVars, lists of actions will still be pruned, but individual actions will not be shrunk.

tagStep :: (state, state) -> LockstepAction state a -> ModelValue state a -> [String] Source #

Tag actions

Tagging is optional, but can help understand your test input data as well as your shrinker (see tagActions).

class (InLockstep state, RunModel (Lockstep state) m) => RunLockstep state (m :: Type -> Type) where Source #

Minimal complete definition

observeReal

Methods

observeReal :: Proxy m -> LockstepAction state a -> Realized m a -> Observable state a Source #

showRealResponse :: Proxy m -> LockstepAction state a -> Maybe (Dict (Show (Realized m a))) Source #

Show responses from the real system

This method does not need to be implemented, but if it is, counter-examples can include the real response in addition to the observable response.

Convenience aliases

type LockstepAction state = Action (Lockstep state) Source #

An action in the lock-step model

type ModelFindVariables state = forall a. Typeable a => Proxy a -> [GVar (ModelOp state) a] Source #

See findVars.

type ModelLookUp state = forall a. ModelVar state a -> ModelValue state a Source #

See lookupVar.

type ModelShrinkVar state = forall a. ModelVar state a -> [ModelVar state a] Source #

See shrinkVar.

type ModelVar state = GVar (ModelOp state) Source #

Variables with a "functor-esque" instance

type RealLookUp (m :: Type -> Type) (op :: Type -> Type -> Type) = forall a. Proxy m -> LookUp m -> GVar op a -> Realized m a Source #

See realLookupVar.

Variable context

type ModelVarContext state = EnvF (ModelValue state) Source #

The environment of known variables and their (model) values.

This environment can be queried for information about known variables through findVars, lookupVar, and shrinkVar. This environment is updated automically by the lockstep framework.

lookupVar :: InLockstep state => ModelVarContext state -> ModelLookUp state Source #

Look up a variable for execution of the model.

The type of the variable is the type in the real system.

findVars :: InLockstep state => ModelVarContext state -> ModelFindVariables state Source #

Find variables of the appropriate type

The type you pass must be the result type of (previously executed) actions. If you want to change the type of the variable, see mapGVar.

shrinkVar :: (Typeable state, InterpretOp (ModelOp state) (ModelValue state)) => ModelVarContext state -> ModelShrinkVar state Source #

Shrink variables to earlier variables of the same type.

realLookupVar :: forall (op :: Type -> Type -> Type) (m :: Type -> Type). InterpretOp op (WrapRealized m) => RealLookUp m op Source #

Look up a variable for execution of the real system.

The type of the variable is the type in the real system.

Variables

data GVar (op :: Type -> Type -> Type) f Source #

Generalized variables

The key difference between GVar and the standard Var type is that GVar have a functor-esque structure: see mapGVar.

Instances

Instances details

(forall x. Show (op x a)) => Show (GVar op a) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.GVar Methods showsPrec :: Int -> GVar op a -> ShowS # show :: GVar op a -> String # showList :: [GVar op a] -> ShowS #
(forall x. Eq (op x a)) => Eq (GVar op a) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.GVar Methods (==) :: GVar op a -> GVar op a -> Bool # (/=) :: GVar op a -> GVar op a -> Bool #
HasVariables (GVar op f) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.GVar Methods getAllVariables :: GVar op f -> Set (Any Var) #

data AnyGVar (op :: Type -> Type -> Type) where Source #

Constructors

SomeGVar :: forall (op :: Type -> Type -> Type) y. GVar op y -> AnyGVar op

Instances

Instances details

HasVariables (AnyGVar op) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.GVar Methods getAllVariables :: AnyGVar op -> Set (Any Var) #

unsafeMkGVar :: Typeable a => Var a -> op a b -> GVar op b Source #

Only for pretty-printing counter-examples, do not use directly

mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b Source #

Operations

class Operation (op :: Type -> Type -> Type) where Source #

Methods

opIdentity :: op a a Source #

Instances

Instances details

Operation Op Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Op.Identity Methods opIdentity :: Op a a Source #
Operation Op Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd Methods opIdentity :: Op a a Source #

class Operation op => InterpretOp (op :: Type -> Type -> Type) (f :: Type -> Type) where Source #

Methods

intOp :: op a b -> f a -> Maybe (f b) Source #

Instances

Instances details

InterpretOp Op f Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Op.Identity Methods intOp :: Op a b -> f a -> Maybe (f b) Source #
InterpretOp Op (WrapRealized IO) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd Methods intOp :: Op a b -> WrapRealized IO a -> Maybe (WrapRealized IO b) Source #
InterpretOp Op (WrapRealized m) => InterpretOp Op (WrapRealized (ReaderT r m)) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd Methods intOp :: Op a b -> WrapRealized (ReaderT r m) a -> Maybe (WrapRealized (ReaderT r m) b) Source #
InterpretOp Op (WrapRealized m) => InterpretOp Op (WrapRealized (StateT s m)) Source #
Instance details Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd Methods intOp :: Op a b -> WrapRealized (StateT s m) a -> Maybe (WrapRealized (StateT s m) b) Source #