Safe Haskell	Safe-Inferred
Language	Haskell2010

Test.QuickCheck.StateModel.Lockstep

Contents

Main abstraction
- Convenience aliases
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 -> ModelLookUp state -> state -> (ModelValue state a, state)
- arbitraryWithVars :: ModelFindVariables state -> state -> Gen (Any (LockstepAction state))
- shrinkWithVars :: ModelFindVariables 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 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 ModelVar state = GVar (ModelOp state)
data GVar op f
data AnyGVar op where
- SomeGVar :: GVar op y -> AnyGVar op
unsafeMkGVar :: Typeable a => Var a -> op a b -> GVar op b
lookUpGVar :: InterpretOp op (WrapRealized m) => Proxy m -> LookUp m -> GVar op a -> Realized m a
mapGVar :: (forall x. op x a -> op x b) -> GVar op a -> GVar op b
class Operation op where
- opIdentity :: op a a
class Operation op => InterpretOp op f 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 -> ModelLookUp state -> state -> (ModelValue state a, state) Source #

Step the model

The order of the arguments mimicks perform.

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

Generate an arbitrary action, given a way to find variables

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

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] 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 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 #

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 Source #

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) Source #

Variables with a "functor-esque" instance

Variables

data GVar op f Source #

Generalized variables

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

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 where Source #

Constructors

SomeGVar :: 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

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

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 Source #

Operations

class Operation op 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 f 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 #