Test.StateMachine.Lockstep.Simple

Test type-level parameters

type family MockState t :: Type

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

data family Cmd t :: Type -> Type

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

data family Resp t :: Type -> Type

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

data family RealHandle t :: Type

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.

data family MockHandle t :: Type

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.

type family Test (f :: Type -> Type) :: Type where ...

Equations

Test (Cmd t) = t

Test (Resp t) = t

type family Tag t :: Type

Tags

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

Test term-level parameters

data StateMachineTest t

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.

Constructors

(Typeable t, Eq (Resp t (MockHandle t)), Show (Resp t (Reference (RealHandle t) Symbolic)), Show (Resp t (Reference (RealHandle t) Concrete)), Show (Resp t (MockHandle t)), Traversable (Resp t), Show (Cmd t (Reference (RealHandle t) Symbolic)), Show (Cmd t (Reference (RealHandle t) Concrete)), Traversable (Cmd t), Eq (RealHandle t), Show (RealHandle t), ToExpr (RealHandle t), Eq (MockHandle t), Show (MockHandle t), ToExpr (MockHandle t), Show (MockState t), ToExpr (MockState t), Show (Tag t)) => StateMachineTest

Fields

• runMock :: Cmd t (MockHandle t) -> MockState t -> (Resp t (MockHandle t), MockState t)
• runReal :: Cmd t (RealHandle t) -> IO (Resp t (RealHandle t))
• initMock :: MockState t
• newHandles :: forall h. Resp t h -> [h]
• generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
• shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
• cleanup :: Model t Concrete -> IO ()
• tag :: [Event t Symbolic] -> [Tag t]

data Event t r

Constructors

Event

Fields

• before :: Model t r
• cmd :: Cmd t :@ r
• after :: Model t r
• mockResp :: Resp t (MockHandle t)

Handle instantiation

newtype At f r

Constructors

At

Fields

• unAt :: f (Reference (RealHandle (Test f)) r)

type (:@) f r = At f r

Model state

data Model t r

Constructors

Model

Fields

• modelState :: MockState t
• modelRefs :: [(Reference (RealHandle t) r, MockHandle t)]

Running the tests

prop_sequential

Arguments

:: StateMachineTest t

-> Maybe Int

(Optional) minimum number of commands

-> Property

prop_parallel

Arguments

:: StateMachineTest t

-> Maybe Int

(Optional) minimum number of commands

-> Property

Translate to n-ary model model

fromSimple :: StateMachineTest t -> StateMachineTest (Simple t) IO