package qcheck-stm

  1. Overview
  2. Docs
package qcheck-stm
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module type STM.SpecSource

The specification of a state machine.

See also SpecExt and SpecDefaults.

Sourcetype cmd

The type of commands

Sourcetype state

The type of the model's state

Sourcetype sut

The type of the system under test

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

Sourceval init_state : state

The model's initial state.

Sourceval show_cmd : cmd -> string

show_cmd c returns a string representing the command c.

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

Sourceval init_sut : unit -> sut

Initialize the system under test.

Sourceval cleanup : sut -> unit

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

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

Sourceval run : cmd -> sut -> res

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

Sourceval postcond : cmd -> state -> 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.