| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.StateMachine.Lockstep.Simple
Synopsis
- 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 ...
- type family Tag t :: Type
- data StateMachineTest t = (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), CanDiff (RealHandle t), Eq (MockHandle t), Show (MockHandle t), CanDiff (MockHandle t), CanDiff (MockHandleN (Simple t) (RealHandle t)), Show (MockState t), CanDiff (MockState t), Show (Tag t), CanDiff (Model (Simple t) Concrete)) => StateMachineTest {
- 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 = Event {}
- newtype At f r = At {
- unAt :: f (Reference (RealHandle (Test f)) r)
- type (:@) f r = At f r
- data Model t r = Model {
- modelState :: MockState t
- modelRefs :: [(Reference (RealHandle t) r, MockHandle t)]
- prop_sequential :: StateMachineTest t -> Maybe Int -> Property
- prop_parallel :: StateMachineTest t -> Maybe Int -> Property
- fromSimple :: StateMachineTest t -> StateMachineTest (Simple t) IO
- data Simple t
- data family MockHandleN t a :: Type
Test type-level parameters
type family MockState t :: Type Source #
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 Source #
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 Source #
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 Source #
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.
Instances
data family MockHandle t :: Type Source #
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 Tag t :: Type Source #
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 Source #
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
Handle instantiation
Model state
Constructors
| Model | |
Fields
| |
Running the tests
Arguments
| :: StateMachineTest t | |
| -> Maybe Int | (Optional) minimum number of commands |
| -> Property |
Arguments
| :: StateMachineTest t | |
| -> Maybe Int | (Optional) minimum number of commands |
| -> Property |
Translate to n-ary model model
fromSimple :: StateMachineTest t -> StateMachineTest (Simple t) IO Source #
For orphan ToExpr instances
Instances
data family MockHandleN t a :: Type Source #
Mock handles
For each real handle a, MockHandleN t a is the corresponding mock handle.