Test.QuickCheck.StateModel.Lockstep

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

Main abstraction

data Lockstep state

Instances

Show state => Show (Lockstep state)

The Show instance does not show the internal environment

Defined in Test.QuickCheck.StateModel.Lockstep.API

Methods

showsPrec :: Int -> Lockstep state -> ShowS

show :: Lockstep state -> String

showList :: [Lockstep state] -> ShowS

HasVariables (Lockstep state)

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.

Defined in Test.QuickCheck.StateModel.Lockstep.Defaults

Methods

getAllVariables :: Lockstep state -> Set (Any Var)

InLockstep state => HasVariables (Action (Lockstep state) a)

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.

Defined in Test.QuickCheck.StateModel.Lockstep.Defaults

Methods

getAllVariables :: Action (Lockstep state) a -> Set (Any Var)

getModel :: Lockstep state -> state

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

Minimal complete definition

observeModel, usedVars, modelNextState, arbitraryWithVars

Associated Types

data ModelValue state a

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

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

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

Extract the observable part of a response from the model

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

All variables required by a command

modelNextState :: LockstepAction state a -> ModelLookUp state -> state -> (ModelValue state a, state)

Step the model

The order of the arguments mimicks perform.

arbitraryWithVars :: ModelFindVariables state -> state -> Gen (Any (LockstepAction state))

Generate an arbitrary action, given a way to find variables

shrinkWithVars :: ModelFindVariables state -> state -> LockstepAction state a -> [Any (LockstepAction state)]

Shrink an action, given a way to find variables

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]

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 where

Minimal complete definition

observeReal

Methods

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

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

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)

An action in the lock-step model

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

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 map.

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

Look up a variable for model execution

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

type ModelVar state = GVar (ModelOp state)

Variables with a "functor-esque" instance

Variables

data GVar op f

Generalized variables

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

Instances

(forall x. Show (op x a)) => Show (GVar op a)

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)

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)

Defined in Test.QuickCheck.StateModel.Lockstep.GVar

Methods

getAllVariables :: GVar op f -> Set (Any Var)

data AnyGVar op where

Constructors

SomeGVar :: GVar op y -> AnyGVar op

Instances

HasVariables (AnyGVar op)

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

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

lookUpGVar :: InterpretOp op (WrapRealized m) => Proxy m -> LookUp m -> GVar op a -> Realized m a

Lookup GVar given a lookup function for Var

The variable must be in the environment and evaluation must succeed. This is normally guaranteed by the default test precondition.

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

Operations

class Operation op where

Methods

opIdentity :: op a a

Instances

Operation Op

Defined in Test.QuickCheck.StateModel.Lockstep.Op.Identity

Methods

opIdentity :: Op a a

Operation Op

Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd

Methods

opIdentity :: Op a a

class Operation op => InterpretOp op f where

Methods

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

Instances

InterpretOp Op f

Defined in Test.QuickCheck.StateModel.Lockstep.Op.Identity

Methods

intOp :: Op a b -> f a -> Maybe (f b)

InterpretOp Op (WrapRealized IO)

Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd

Methods

intOp :: Op a b -> WrapRealized IO a -> Maybe (WrapRealized IO b)

InterpretOp Op (WrapRealized m) => InterpretOp Op (WrapRealized (ReaderT r m))

Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd

Methods

intOp :: Op a b -> WrapRealized (ReaderT r m) a -> Maybe (WrapRealized (ReaderT r m) b)

InterpretOp Op (WrapRealized m) => InterpretOp Op (WrapRealized (StateT s m))

Defined in Test.QuickCheck.StateModel.Lockstep.Op.SumProd

Methods

intOp :: Op a b -> WrapRealized (StateT s m) a -> Maybe (WrapRealized (StateT s m) b)