The specification of a state machine.
val arb_cmd : state -> cmd QCheck.arbitraryA command generator. Accepts a state parameter to enable state-dependent cmd generation.
val init_state : stateThe model's initial state.
val show_cmd : cmd -> stringshow_cmd c returns a string representing the command c.
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 -> sutInitialize the system under test.
val cleanup : sut -> unitUtility function to clean up the sut after each test instance, e.g., for closing sockets, files, or resetting global parameters
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.
run c i should interpret the command c over the system under test (typically side-effecting).
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.