Stateful (model-based) testing.

A stateful test applies a random sequence of rules to a piece of state and checks invariants along the way. A rule is a function that takes the TestCase and the state, draws whatever data it needs, and updates the state (and the system under test) in place. An invariant is a property of the state that must hold after every step.

Describe the machine as a plain object — a StateMachine — mapping rule names to rule functions and invariant names to invariant functions, then call run (or runAsync, for asynchronous rules) inside a Hegel test:

import { test } from "vitest";
import * as hegel from "@hegeldev/hegel";
import * as gs from "@hegeldev/hegel/generators";

interface Stack {
  items: number[];
}

const stackMachine: hegel.stateful.StateMachine<Stack> = {
  rules: {
    push: (tc, stack) => {
      stack.items.push(tc.draw(gs.integers()));
    },
    pop: (tc, stack) => {
      tc.assume(stack.items.length > 0);
      stack.items.pop();
    },
  },
  invariants: {
    nonNegativeLength: (_tc, stack) => {
      if (stack.items.length < 0) throw new Error("negative length");
    },
  },
};

test("stack", () =>
  hegel.test((tc) => {
    hegel.stateful.run(tc, stackMachine, { items: [] });
  }));
Copy

The engine owns the run: it decides how many steps to take (at most RunOptions.stepCount, 50 by default), which rule runs at each step — applying swarm testing, where each test case enables a random subset of the rules — and which sampled invariants to check after which steps. On failure it shrinks the sequence of steps like any other input, and the final replay reports each step as Step N: <rule> together with the draws the rule made.

Every invariant is checked on the initial state and on the final state. In between, invariants are sampled: each is checked after any given step with probability 1 / stepCount, so its expected cost per test case stays constant as the step count grows. Mark an invariant { check, alwaysCheck: true } to check it after every step instead — for invariants that must observe every intermediate state, or that mutate the state when checked.

Assumptions in rules

A rule may reject the current step with TestCase.assume: the step is dropped (it does not count toward the step budget) and the machine carries on with another rule. Rejection is not transactional — anything the rule did before the assumption failed has already happened — so place assumptions at the start of the rule, before mutating the state or the system under test. A filtered generator that runs out of retries rejects the step the same way.

Pools

Rules often need to act on values that earlier rules produced — a handle that was allocated, a key that was inserted. A Pool holds such values: rules add to it and draw from the generators it hands out, so which value a rule picks is a recorded, shrinkable choice like any other draw.