Test.StateMachine.Lockstep.NAry

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

Instances

type MockState (Simple t)

Defined in Test.StateMachine.Lockstep.Simple

type MockState (Simple t) = MockState t

data family Cmd t :: (Type -> Type) -> [Type] -> Type

Commands

In Cmd t f hs, hs is the list of real handle types, and f is some functor applied to each of them. Two typical instantiations are

Cmd t I              (RealHandles t)   -- for the system under test
Cmd t (MockHandleN t) (RealHandles t)   -- for the mock

Instances

Traversable (Cmd t) => NTraversable (Cmd (Simple t) :: (Type -> Type) -> [Type] -> Type)

Defined in Test.StateMachine.Lockstep.Simple

Methods

nctraverse :: forall m c (xs :: [k]) proxy g h. (Applicative m, All c xs) => proxy c -> (forall (a :: k). c a => Elem xs a -> g a -> m (h a)) -> Cmd (Simple t) g xs -> m (Cmd (Simple t) h xs)

(NTraversable (Cmd t), SListI (RealHandles t)) => Foldable (At (Cmd t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

foldMap :: Monoid m => (forall (x :: k). p x -> m) -> At (Cmd t) p -> m

(NTraversable (Cmd t), SListI (RealHandles t)) => Functor (At (Cmd t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

fmap :: (forall (x :: k). p x -> q x) -> At (Cmd t) p -> At (Cmd t) q

(NTraversable (Cmd t), SListI (RealHandles t)) => Traversable (At (Cmd t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

traverse :: Applicative f => (forall (a :: k). p a -> f (q a)) -> At (Cmd t) p -> f (At (Cmd t) q)

(Functor (Cmd t), Show (Cmd t (Reference (RealHandle t) r)), Show1 r) => Show (Cmd (Simple t) (FlipRef r) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> Cmd (Simple t) (FlipRef r) '[RealHandle t] -> ShowS

show :: Cmd (Simple t) (FlipRef r) '[RealHandle t] -> String

showList :: [Cmd (Simple t) (FlipRef r) '[RealHandle t]] -> ShowS

data Cmd (Simple _1) _f _hs

Defined in Test.StateMachine.Lockstep.Simple

data Cmd (Simple _1) _f _hs where

• SimpleCmd :: forall _ (_f :: Type -> Type) h. Cmd _ (_f h) -> Cmd (Simple _) _f '[h]

data family Resp t :: (Type -> Type) -> [Type] -> Type

Responses

The type arguments are similar to those of Cmd. Two typical instances:

Resp t I              (RealHandles t)  -- for the system under test
Resp t (MockHandleN t) (RealHandles t)  -- for the mock

Instances

Traversable (Resp t) => NTraversable (Resp (Simple t) :: (Type -> Type) -> [Type] -> Type)

Defined in Test.StateMachine.Lockstep.Simple

Methods

nctraverse :: forall m c (xs :: [k]) proxy g h. (Applicative m, All c xs) => proxy c -> (forall (a :: k). c a => Elem xs a -> g a -> m (h a)) -> Resp (Simple t) g xs -> m (Resp (Simple t) h xs)

(NTraversable (Resp t), SListI (RealHandles t)) => Foldable (At (Resp t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

foldMap :: Monoid m => (forall (x :: k). p x -> m) -> At (Resp t) p -> m

(NTraversable (Resp t), SListI (RealHandles t)) => Functor (At (Resp t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

fmap :: (forall (x :: k). p x -> q x) -> At (Resp t) p -> At (Resp t) q

(NTraversable (Resp t), SListI (RealHandles t)) => Traversable (At (Resp t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

traverse :: Applicative f => (forall (a :: k). p a -> f (q a)) -> At (Resp t) p -> f (At (Resp t) q)

(Functor (Resp t), Show (Resp t (Reference (RealHandle t) r)), Show1 r) => Show (Resp (Simple t) (FlipRef r) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> Resp (Simple t) (FlipRef r) '[RealHandle t] -> ShowS

show :: Resp (Simple t) (FlipRef r) '[RealHandle t] -> String

showList :: [Resp (Simple t) (FlipRef r) '[RealHandle t]] -> ShowS

(Functor (Resp t), Show (Resp t (MockHandle t))) => Show (Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> ShowS

show :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> String

showList :: [Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]] -> ShowS

(Functor (Resp t), Eq (Resp t (MockHandle t)), Eq (MockHandle t)) => Eq (Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

(==) :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Bool

(/=) :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Bool

data Resp (Simple _1) _f _hs

Defined in Test.StateMachine.Lockstep.Simple

data Resp (Simple _1) _f _hs where

• SimpleResp :: forall _ (_f :: Type -> Type) h. Resp _ (_f h) -> Resp (Simple _) _f '[h]

type family RealHandles t :: [Type]

Type-level list of the types of the handles in the system under test

NOTE: If your system under test only requires a single real handle, you might consider using Test.StateMachine.Lockstep.Simple instead.

Instances

type RealHandles (Simple t)

Defined in Test.StateMachine.Lockstep.Simple

type RealHandles (Simple t) = '[RealHandle t]

data family MockHandleN t a :: Type

Mock handles

For each real handle a, MockHandleN t a is the corresponding mock handle.

Instances

Show (MockHandle t) => Show (MockHandleN (Simple t) (RealHandle t))

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> MockHandleN (Simple t) (RealHandle t) -> ShowS

show :: MockHandleN (Simple t) (RealHandle t) -> String

showList :: [MockHandleN (Simple t) (RealHandle t)] -> ShowS

Eq (MockHandle t) => Eq (MockHandleN (Simple t) (RealHandle t))

Defined in Test.StateMachine.Lockstep.Simple

Methods

(==) :: MockHandleN (Simple t) (RealHandle t) -> MockHandleN (Simple t) (RealHandle t) -> Bool

(/=) :: MockHandleN (Simple t) (RealHandle t) -> MockHandleN (Simple t) (RealHandle t) -> Bool

(Functor (Resp t), Show (Resp t (MockHandle t))) => Show (Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> ShowS

show :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> String

showList :: [Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t]] -> ShowS

(Functor (Resp t), Eq (Resp t (MockHandle t)), Eq (MockHandle t)) => Eq (Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

(==) :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Bool

(/=) :: Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Resp (Simple t) (MockHandleN (Simple t)) '[RealHandle t] -> Bool

newtype MockHandleN (Simple t) (RealHandle t)

Defined in Test.StateMachine.Lockstep.Simple

newtype MockHandleN (Simple t) (RealHandle t) = SimpleToMock {

• unSimpleToMock :: MockHandle t

}

type family Test (f :: (Type -> Type) -> [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).

Instances

type Tag (Simple t)

Defined in Test.StateMachine.Lockstep.Simple

type Tag (Simple t) = Tag t

Test term-level parameters

data StateMachineTest t m

State machine test

This captures the design patterns sketched in https://well-typed.com/blog/2019/01/qsm-in-depth/.

Constructors

(Monad m, All Typeable (RealHandles t), All Eq (RealHandles t), All (And Show (Compose Show (MockHandleN t))) (RealHandles t), All (And CanDiff (Compose CanDiff (MockHandleN t))) (RealHandles t), NTraversable (Resp t), Eq (Resp t (MockHandleN t) (RealHandles t)), Show (Resp t (MockHandleN t) (RealHandles t)), Show (Resp t (FlipRef Symbolic) (RealHandles t)), Show (Resp t (FlipRef Concrete) (RealHandles t)), NTraversable (Cmd t), Show (Cmd t (FlipRef Symbolic) (RealHandles t)), Show (Cmd t (FlipRef Concrete) (RealHandles t)), Show (MockState t), CanDiff (MockState t), Show (Tag t), CanDiff (Model t Concrete)) => StateMachineTest

Fields

• runMock :: Cmd t (MockHandleN t) (RealHandles t) -> MockState t -> (Resp t (MockHandleN t) (RealHandles t), MockState t)
• runReal :: Cmd t I (RealHandles t) -> m (Resp t I (RealHandles t))
• initMock :: MockState t
• newHandles :: forall f. Resp t f (RealHandles t) -> NP (List :.: f) (RealHandles t)
• generator :: Model t Symbolic -> Maybe (Gen (Cmd t :@ Symbolic))
• shrinker :: Model t Symbolic -> (Cmd t :@ Symbolic) -> [Cmd t :@ Symbolic]
• cleanup :: Model t Concrete -> m ()
• 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 (MockHandleN t) (RealHandles t)

hoistStateMachineTest :: Monad n => (forall a. m a -> n a) -> StateMachineTest t m -> StateMachineTest t n

Handle instantiation

newtype At f r

Constructors

At

Fields

• unAt :: f (FlipRef r) (RealHandles (Test f))

Instances

(NTraversable (Cmd t), SListI (RealHandles t)) => Foldable (At (Cmd t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

foldMap :: Monoid m => (forall (x :: k). p x -> m) -> At (Cmd t) p -> m

(NTraversable (Resp t), SListI (RealHandles t)) => Foldable (At (Resp t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

foldMap :: Monoid m => (forall (x :: k). p x -> m) -> At (Resp t) p -> m

(NTraversable (Cmd t), SListI (RealHandles t)) => Functor (At (Cmd t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

fmap :: (forall (x :: k). p x -> q x) -> At (Cmd t) p -> At (Cmd t) q

(NTraversable (Resp t), SListI (RealHandles t)) => Functor (At (Resp t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

fmap :: (forall (x :: k). p x -> q x) -> At (Resp t) p -> At (Resp t) q

(NTraversable (Cmd t), SListI (RealHandles t)) => Traversable (At (Cmd t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

traverse :: Applicative f => (forall (a :: k). p a -> f (q a)) -> At (Cmd t) p -> f (At (Cmd t) q)

(NTraversable (Resp t), SListI (RealHandles t)) => Traversable (At (Resp t) :: (Type -> Type) -> Type)

Defined in Test.StateMachine.Lockstep.NAry

Methods

traverse :: Applicative f => (forall (a :: k). p a -> f (q a)) -> At (Resp t) p -> f (At (Resp t) q)

Show (f (FlipRef r) (RealHandles (Test f))) => Show (At f r)

Defined in Test.StateMachine.Lockstep.NAry

Methods

showsPrec :: Int -> At f r -> ShowS

show :: At f r -> String

showList :: [At f r] -> ShowS

type (:@) f r = At f r

Model state

data Model t r

Constructors

Model

Fields

• modelState :: MockState t
• modelRefss :: Refss t r

Instances

Generic (Model t r)

Defined in Test.StateMachine.Lockstep.NAry

Associated Types

type Rep (Model t r) :: Type -> Type

Methods

from :: Model t r -> Rep (Model t r) x

to :: Rep (Model t r) x -> Model t r

(Show1 r, Show (MockState t), All (And Show (Compose Show (MockHandleN t))) (RealHandles t)) => Show (Model t r)

Defined in Test.StateMachine.Lockstep.NAry

Methods

showsPrec :: Int -> Model t r -> ShowS

show :: Model t r -> String

showList :: [Model t r] -> ShowS

type Rep (Model t r)

Defined in Test.StateMachine.Lockstep.NAry

type Rep (Model t r) = D1 ('MetaData "Model" "Test.StateMachine.Lockstep.NAry" "quickcheck-state-machine-0.9.0-8zWHYIJYc77JtQ2efkvn1E-no-vendored-treediff" 'False) (C1 ('MetaCons "Model" 'PrefixI 'True) (S1 ('MetaSel ('Just "modelState") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (MockState t)) :*: S1 ('MetaSel ('Just "modelRefss") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Refss t r))))

newtype Refs t r a

Relation between real and mock references for single handle type a

Constructors

Refs

Fields

• unRefs :: [(Reference a r, MockHandleN t a)]

Instances

Monoid (Refs t r a)

Defined in Test.StateMachine.Lockstep.NAry

Methods

mempty :: Refs t r a

mappend :: Refs t r a -> Refs t r a -> Refs t r a

mconcat :: [Refs t r a] -> Refs t r a

Semigroup (Refs t r a)

Defined in Test.StateMachine.Lockstep.NAry

Methods

(<>) :: Refs t r a -> Refs t r a -> Refs t r a

sconcat :: NonEmpty (Refs t r a) -> Refs t r a

stimes :: Integral b => b -> Refs t r a -> Refs t r a

Generic (Refs t r a)

Defined in Test.StateMachine.Lockstep.NAry

Associated Types

type Rep (Refs t r a) :: Type -> Type

Methods

from :: Refs t r a -> Rep (Refs t r a) x

to :: Rep (Refs t r a) x -> Refs t r a

(Show1 r, Show a, Show (MockHandleN t a)) => Show (Refs t r a)

Defined in Test.StateMachine.Lockstep.NAry

Methods

showsPrec :: Int -> Refs t r a -> ShowS

show :: Refs t r a -> String

showList :: [Refs t r a] -> ShowS

type Rep (Refs t r a)

Defined in Test.StateMachine.Lockstep.NAry

type Rep (Refs t r a) = Rep [(Reference a r, MockHandleN t a)]

newtype Refss t r

Relation between real and mock references for all handle types

Constructors

Refss

Fields

• unRefss :: NP (Refs t r) (RealHandles t)

Instances

SListI (RealHandles t) => Monoid (Refss t r)

Defined in Test.StateMachine.Lockstep.NAry

Methods

mempty :: Refss t r

mappend :: Refss t r -> Refss t r -> Refss t r

mconcat :: [Refss t r] -> Refss t r

SListI (RealHandles t) => Semigroup (Refss t r)

Defined in Test.StateMachine.Lockstep.NAry

Methods

(<>) :: Refss t r -> Refss t r -> Refss t r

sconcat :: NonEmpty (Refss t r) -> Refss t r

stimes :: Integral b => b -> Refss t r -> Refss t r

(Show1 r, All (And Show (Compose Show (MockHandleN t))) (RealHandles t)) => Show (Refss t r)

Defined in Test.StateMachine.Lockstep.NAry

Methods

showsPrec :: Int -> Refss t r -> ShowS

show :: Refss t r -> String

showList :: [Refss t r] -> ShowS

newtype FlipRef r h

Constructors

FlipRef

Fields

• unFlipRef :: Reference h r

Instances

(Show1 r, Show h) => Show (FlipRef r h)

Defined in Test.StateMachine.Lockstep.NAry

Methods

showsPrec :: Int -> FlipRef r h -> ShowS

show :: FlipRef r h -> String

showList :: [FlipRef r h] -> ShowS

(Functor (Cmd t), Show (Cmd t (Reference (RealHandle t) r)), Show1 r) => Show (Cmd (Simple t) (FlipRef r) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> Cmd (Simple t) (FlipRef r) '[RealHandle t] -> ShowS

show :: Cmd (Simple t) (FlipRef r) '[RealHandle t] -> String

showList :: [Cmd (Simple t) (FlipRef r) '[RealHandle t]] -> ShowS

(Functor (Resp t), Show (Resp t (Reference (RealHandle t) r)), Show1 r) => Show (Resp (Simple t) (FlipRef r) '[RealHandle t])

Defined in Test.StateMachine.Lockstep.Simple

Methods

showsPrec :: Int -> Resp (Simple t) (FlipRef r) '[RealHandle t] -> ShowS

show :: Resp (Simple t) (FlipRef r) '[RealHandle t] -> String

showList :: [Resp (Simple t) (FlipRef r) '[RealHandle t]] -> ShowS

Running the tests

prop_sequential

Arguments

:: forall t. StateMachineTest t IO

-> Maybe Int

(Optional) minimum number of commands

-> Property

Sequential test

prop_parallel

Arguments

:: StateMachineTest t IO

-> Maybe Int

(Optional) minimum number of commands

-> Property

Parallel test

NOTE: This currently does not do labelling.

Examples

showLabelledExamples'

Arguments

:: StateMachineTest t m

-> Maybe Int

Seed

-> Int

Number of tests to run to find examples

-> (Tag t -> Bool)

Tag filter (can be const True)

-> IO ()

Show minimal examples for each of the generated tags.

This is the analogue of showLabelledExamples'. See also showLabelledExamples.

showLabelledExamples :: StateMachineTest t m -> IO ()

Simplified form of showLabelledExamples'

Translate to state machine model

toStateMachine :: StateMachineTest t m -> StateMachine (Model t) (At (Cmd t)) m (At (Resp t))