Mock state

The t argument (here and elsewhere) is a type-level tag that combines all aspects of the test; it does not need any term-level constructors

data MyTest
type instance MockState MyTest = ..

Commands

In Cmd t h, h is the type of the handle

Cmd t (RealHandle t)  -- for the system under test
Cmd t (MockHandle t)  -- for the mock

Responses

In Resp t h, h is the type of the handle

Resp t (RealHandle t)  -- for the system under test
Resp t (MockHandle t)  -- for the mock

The type of the real handle in the system under test

The key difference between the " simple " lockstep infrastructure and the n-ary lockstep infrastructure is that the former only supports a single real handle, whereas the latter supports an arbitrary list of them.

The type of the mock handle

NOTE: In the n-ary infrastructure, MockHandle is a type family of two arguments, because we have a mock handle for each real handle. Here, however, we only have a single real handle, so the " corresponding " real handle is implicitly RealHandle t.

Tags

Tags are used when labelling execution runs in prop_sequential, as well as when looking for minimal examples with a given label (showLabelledExamples).

State machine test

This captures the design patterns sketched in https://well-typed.com/blog/2019/01/qsm-in-depth/ for the case where there is exactly one real handle. See Test.StateMachine.Lockstep.NAry for the generalization to n handles.