Test.StateMachine.Lockstep.Simple

Test type-level parameters

type family MockState t :: Type

data family Cmd t :: Type -> Type

data family Resp t :: Type -> Type

data family RealHandle t :: Type

data family MockHandle t :: Type

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

Equations

Test (Cmd t) = t

Test (Resp t) = t

Test term-level parameters

data StateMachineTest t

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)) => 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 ()

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)