Module Internal.Make

A precondition checker (stops early, thanks to short-circuit Boolean evaluation). Accepts the initial state and the command sequence as parameters.

A generator of command sequences. Accepts the initial state as parameter.

A consistency test that generates a number of cmd sequences and checks that all contained cmds satisfy the precondition precond. Accepts two labeled parameters: count is the test count and name is the printed test name.

Checks agreement between the model and the system under test (stops early, thanks to short-circuit Boolean evaluation).

check_disagree state sut pg checks that none of the commands present in pg violated the declared postconditions when pg is run in state. Return None if none of the commands violate its postcondition, and Some list corresponding to the prefix of pg ending with the cmd violating its postcondition.

check_obs pref cs1 cs2 s tests whether the observations from the sequential prefix pref and the parallel traces cs1 cs2 agree with the model started in state s.

gen_cmds_size arb state gen_int generates a program of size generated by gen_int using arb to generate cmds according to the current state. state is the starting state.

arb_cmds_triple seq_len par_len generates a cmd triple with at most seq_len sequential commands and at most par_len parallel commands each.

all_interleavings_ok seq spawn0 spawn1 state checks that preconditions of all the cmds of seq, spawn0, and spawn1 are satisfied in all the possible interleavings and starting with state

shrink_triple arb0 arb1 arb2 is a QCheck.Shrink.t for programs (triple of list of cmds) that is specialized for each part of the program.

arb_triple seq_len par_len arb0 arb1 arb2 generates a cmd triple with at most seq_len sequential commands and at most par_len parallel commands each. The three cmd components are generated with arb0, arb1, and arb2, respectively. Each of these take the model state as a parameter.