The type of commands

The type of the model's state

The type of the system under test

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

The model's initial state.

show_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, as it is run more than once.

Initialize the system under test.

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