class (forall a. Show (Action state a), forall a. HasVariables (Action state a), Show state, HasVariables state) => StateModel state whereThe typeclass users implement to define a model against which to validate some implementation.
To implement a StateModel, user needs to provide at least the following:
A datatype for Actions: Each test case is a sequence of Actions that's supposed to lead from some initialState to some end state,
A generator for traces of Actions, the arbitraryAction function,
An initialState,
A transition function, nextState, that "interprets" each Action and producing some new
state.
For finer grained control over the testing process, one can also define:
shrinkAction: Shrinking is an important part of MBT as it allows QuickCheck engine to look for simpler test cases when something goes wrong which makes troubleshooting easier,
precondition: Filters generated Action depending on the
state. When precondition is False then the action is rejected and a new one is tried. This is also useful when shrinking a trace in order to ensure that removing some Action still produces a valid trace. The precondition can be somewhat redundant with the generator's conditions,validFailingAction: Specifies when an action that fails it's precondition can still run as what is called a _negative_ action. This means that the action is (1) expected to fail and (2) not expected to change the model state. This is very useful for testing the checks and failure conditions in the SUT are implemented correctly. Should it be necessary to update the model state with e.g. book-keeping for a negative action one can define failureNextState - but it is generally recommended to let this be as simple an action as possible.
Associated types
data family Action state aThe type of Action relevant for this
state.This is expected to be defined as a GADT where the
aparameter is instantiated to some observable output from the SUT a given action is expected to produce. For example, here is a fragment of the `Action RegState` (taken from theSpec.Dynamic.RegistryModelmodule) :data Action RegState a where Spawn :: Action RegState ThreadId Register :: String -> Var ThreadId -> Action RegState () KillThread :: Var ThreadId -> Action RegState ()The
Spawnaction should produce aThreadId, whereas theKillThreadaction does not return anything.
Methods
actionName :: Action state a -> StringarbitraryAction :: VarContext -> state -> Gen (Any (Action state))Generator for Action depending on
state.shrinkAction :: Typeable a => VarContext -> state -> Action state a -> [Any (Action state)]Shrinker for Action. Defaults to no-op but as usual, defining a good shrinker greatly enhances the usefulness of property-based testing.
initialState :: stateInitial state of generated traces.
nextState :: Typeable a => state -> Action state a -> Var a -> stateTransition function for the model. The `Var a` parameter is useful to keep reference to actual value of type
aproduced by performing the Action inside thestateso that further actions can useLookupto retrieve that data. This allows the model to be ignorant of those values yet maintain some references that can be compared and looked for.failureNextState :: Typeable a => state -> Action state a -> stateTransition function for negative actions. Note that most negative testing applications should not require an implementation of this function!
precondition :: state -> Action state a -> BoolPrecondition for filtering generated Action. This function is applied before the action is performed, it is useful to refine generators that can produce more values than are useful.
validFailingAction :: state -> Action state a -> BoolPrecondition for filtering an Action that can meaningfully run but is supposed to fail. An action will run as a _negative_ action if the precondition fails and validFailingAction succeeds. A negative action should have _no effect_ on the model state. This may not be desierable in all situations - in which case one can override this semantics for book-keeping in failureNextState.