Parameter Make.1-Spec

type cmd

The type of commands

type state

The type of the model's state

type sut

The type of the system under test

val arb_cmd : state -> cmd QCheck.arbitrary

A command generator. Accepts a state parameter to enable state-dependent cmd generation.

val init_state : state

The model's initial state.

val show_cmd : cmd -> string

show_cmd c returns a string representing the command c.

val next_state : cmd -> state -> state

next_state c s expresses how interpreting the command c moves the model's internal state machine from the state s to the next state. Ideally a next_state function is pure.

val init_sut : unit -> sut

Initialize the system under test.

val cleanup : sut -> unit

Utility function to clean up the sut after each test instance, e.g., for closing sockets, files, or resetting global parameters

val precond : cmd -> state -> bool

precond c s expresses preconditions for command c in terms of the model state s. A precond function should be pure. precond is useful, e.g., to prevent the shrinker from breaking invariants when minimizing counterexamples.

val run : cmd -> sut -> STM.res

run c i should interpret the command c over the system under test (typically side-effecting).

val postcond : cmd -> state -> STM.res -> bool

postcond c s res checks whether res arising from interpreting the command c over the system under test with run agrees with the model's result. A postcond function should be a pure.

Note: the state parameter s is the model's state before executing the command c (the "old/pre" state). This is helpful to model, e.g., a remove cmd that returns the removed element.