package qcheck-stm

  1. Overview
  2. Docs
package qcheck-stm
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.