State Testing

The idea

State machine testing works by:

1. Defining an abstract model of the system's expected behavior
2. Generating random command sequences
3. Executing commands against both the real system and the model
4. Checking that the real system's behavior matches the model at every step

Defining a specification

You implement the Hedgehog.Stm.Spec module type. Here's a complete example testing a mutable counter:

open Hedgehog

(* The system under test: a simple mutable counter *)
module Counter = struct
  type t = { mutable value : int }
  let create () = { value = 0 }
  let get c = c.value
  let incr c = c.value <- c.value + 1
  let decr c = c.value <- c.value - 1
  let reset c = c.value <- 0
end

module Counter_spec = struct
  type cmd = Get | Incr | Decr | Reset
  type state = int
  type sut = Counter.t
  type result = Int of int | Unit

  let show_cmd = function
    | Get -> "get"
    | Incr -> "incr"
    | Decr -> "decr"
    | Reset -> "reset"

  let show_result = function
    | Int n -> string_of_int n
    | Unit -> "()"

  let gen_cmd _state =
    Gen.element [Get; Incr; Decr; Reset]

  let shrink_cmd _cmd = Seq.empty

  let init_state = 0
  let init_sut () = Counter.create ()
  let cleanup _sut = ()

  let next_state cmd state =
    match cmd with
    | Get -> state
    | Incr -> state + 1
    | Decr -> state - 1
    | Reset -> 0

  let precond _state _cmd = true

  let run cmd sut =
    match cmd with
    | Get -> Int (Counter.get sut)
    | Incr -> Counter.incr sut; Unit
    | Decr -> Counter.decr sut; Unit
    | Reset -> Counter.reset sut; Unit

  let postcond cmd state result =
    match cmd, result with
    | Get, Int n -> n = state
    | Get, _ -> false
    | _, Unit -> true
    | _, _ -> false
end

module Counter_test = Stm.Make(Counter_spec)

Running sequential tests

open Hedgehog

module Counter = struct
  type t = { mutable value : int }
  let create () = { value = 0 }
  let get c = c.value
  let incr c = c.value <- c.value + 1
  let decr c = c.value <- c.value - 1
  let reset c = c.value <- 0
end

module Counter_spec = struct
  type cmd = Get | Incr | Decr | Reset
  type state = int
  type sut = Counter.t
  type result = Int of int | Unit
  let show_cmd = function
    | Get -> "get" | Incr -> "incr" | Decr -> "decr" | Reset -> "reset"
  let show_result = function
    | Int n -> string_of_int n | Unit -> "()"
  let gen_cmd _state = Gen.element [Get; Incr; Decr; Reset]
  let shrink_cmd _cmd = Seq.empty
  let init_state = 0
  let init_sut () = Counter.create ()
  let cleanup _sut = ()
  let next_state cmd state =
    match cmd with
    | Get -> state | Incr -> state + 1 | Decr -> state - 1 | Reset -> 0
  let precond _state _cmd = true
  let run cmd sut =
    match cmd with
    | Get -> Int (Counter.get sut) | Incr -> Counter.incr sut; Unit
    | Decr -> Counter.decr sut; Unit | Reset -> Counter.reset sut; Unit
  let postcond cmd state result =
    match cmd, result with
    | Get, Int n -> n = state | Get, _ -> false | _, Unit -> true | _, _ -> false
end

module Counter_test = Stm.Make(Counter_spec)

let () =
  let prop = Counter_test.sequential () in
  Property.check prop |> ignore

The sequential test generates random command sequences, executes them one at a time, and checks postconditions after each step. If a postcondition fails, the sequence is shrunk to find the minimal failing prefix.

Parallel testing

Parallel testing detects concurrency bugs by running commands concurrently and checking that the results are linearizable — that there exists some sequential ordering of the commands that explains the observed results:

open Hedgehog

module Counter = struct
  type t = { mutable value : int }
  let create () = { value = 0 }
  let get c = c.value
  let incr c = c.value <- c.value + 1
  let decr c = c.value <- c.value - 1
  let reset c = c.value <- 0
end

module Counter_spec = struct
  type cmd = Get | Incr | Decr | Reset
  type state = int
  type sut = Counter.t
  type result = Int of int | Unit
  let show_cmd = function
    | Get -> "get" | Incr -> "incr" | Decr -> "decr" | Reset -> "reset"
  let show_result = function
    | Int n -> string_of_int n | Unit -> "()"
  let gen_cmd _state = Gen.element [Get; Incr; Decr; Reset]
  let shrink_cmd _cmd = Seq.empty
  let init_state = 0
  let init_sut () = Counter.create ()
  let cleanup _sut = ()
  let next_state cmd state =
    match cmd with
    | Get -> state | Incr -> state + 1 | Decr -> state - 1 | Reset -> 0
  let precond _state _cmd = true
  let run cmd sut =
    match cmd with
    | Get -> Int (Counter.get sut) | Incr -> Counter.incr sut; Unit
    | Decr -> Counter.decr sut; Unit | Reset -> Counter.reset sut; Unit
  let postcond cmd state result =
    match cmd, result with
    | Get, Int n -> n = state | Get, _ -> false | _, Unit -> true | _, _ -> false
end

module Counter_test = Stm.Make(Counter_spec)

let () =
  let prop = Counter_test.parallel () in
  Property.check prop |> ignore

For the simple counter above, parallel testing would likely find a bug since the incr and decr operations are not atomic. In a real application, you'd use locks or atomic operations and verify the implementation is correct.

Specification reference

The Hedgehog.Stm.Spec module type requires:

Tips

• Generate commands based on state. Use gen_cmd's state parameter to only generate valid commands. For example, don't generate "pop" on an empty stack.
• Use precond as a safety net. Even with state-aware generation, shrinking might produce invalid sequences. precond filters these out.
• Keep the model simple. The model should be obviously correct. Use simple data structures (lists, maps) even if the real system uses something more complex.
• Parallel testing is non-deterministic. Run parallel tests multiple times or with more test cases to increase confidence.