Stateful (hegel.Hegel.Stateful)

Introduction

A stateful test exercises a system through a sequence of randomly chosen actions ("rules") applied to a state. Rules are constructed with Rule.create from a name and a step function that performs one application of the rule, drawing any arguments it needs from the test case and returning the new state. Invariants are 'state -> unit functions evaluated before any step is run and after every successful step.

To run a state machine, call run inside a Hegel test. Examples in this documentation assume open Hegel.

Example: an integer stack.

let push =
  Stateful.Rule.create ~name:"push" ~step:(fun tc stack ->
      let n =
        draw tc (Generators.integers ~min_value:0 ~max_value:100 ())
      in
      n :: stack)

let pop =
  Stateful.Rule.create ~name:"pop" ~step:(fun tc stack ->
      assume tc (not (List.is_empty stack));
      List.tl stack)

let%hegel_test integer_stack tc =
  Stateful.run
    ~init:[]
    ~rules:[ push; pop ]
    ~sexp_of_state:(Core.List.sexp_of_t Core.Int.sexp_of_t)
    tc

Passing ?sexp_of_state makes a failing sequence print the model state after each step, so you can see how it evolved; see run.

Submodules

module Pool : sig ... end

module Rule : sig ... end

Running stateful tests

val run : 
  init:'state ->
  rules:'state Rule.t list ->
  ?invariants:('state -> unit) list ->
  ?sexp_of_state:('state -> Core.Sexp.t) ->
  test_case ->
  unit

Executes a stateful test by repeatedly applying randomly chosen rules to a state threaded from init, checking each of the invariants before the first step and after every successful step. Raises Invalid_argument if rules is empty.

On a failing replay, each applied rule prints as Step N: <name>, with the values the rule draws nested under it. When sexp_of_state is supplied, the model state also prints as state = <value> after the initial state and after every step. An invariant that is violated prints Invariant N violated after step M or Invariant N violated in the initial state, where N is the invariant's index in invariants.

  state = 0
  Step 1: add
    draw_1 = 3
  state = 3
  Step 2: add
    draw_2 = 7
  state = 10
  Invariant 0 violated after step 2.