From Property-Based Testing to Model-Based Testing

In my previous post on property-based testing in Go, I generated values and checked properties such as serialization round trips and stable event IDs. Each generated value was one test case.

Many of the failures I care about in distributed systems depend on history instead. Each operation in a booking system may pass its own unit tests while the lifecycle still mishandles a sequence such as:

create
confirm
cancel
confirm

The last confirmation should be rejected. Other failures need less obvious histories: a retry applies an effect twice, a delayed command reopens a cancelled booking, or a rejected command changes state before returning an error.

Hand-written examples cover the histories I anticipate. In this post, I use model-based testing to mean a stateful property test: Rapid generates commands, a small model predicts each result, and the test compares those predictions with the real system.

1. Generate a history, not just a value

A property test usually draws a value, calls the code under test and checks an invariant:

generated value -> system under test -> invariant

For stateful behavior, the generated input is the next command in a history. Rapid chooses an action, the model predicts its response and state transition, and the system under test executes the same command. After every step, the test compares the expected and observed behavior.

The model supplies the expected results, but it should not recreate the production implementation. It contains only the state needed to predict the behavior under test. The real booking service might use HTTP, a database, an outbox and several workers; the model can still be an enum and an integer.

2. A booking lifecycle model

Suppose a booking begins in Missing, moves to Pending when created, and may then be confirmed or cancelled. A confirmed booking may also be cancelled. Retrying the same confirmation command is idempotent; it succeeds without publishing another confirmation event. Other invalid commands return an error and leave the state unchanged.

The model needs to track only two facts:

type BookingState string

const (
	Missing   BookingState = "missing"
	Pending   BookingState = "pending"
	Confirmed BookingState = "confirmed"
	Cancelled BookingState = "cancelled"
)

type BookingModel struct {
	state              BookingState
	confirmationEvents int
	sut                BookingSystem
	id                 string
}

Missing is the test adapter’s representation of an absent booking, not a state the production domain needs to store.

BookingSystem is a test adapter around the real implementation. It exposes operations and observations in a form the model can use:

type BookingSystem interface {
	Create(id string) error
	Confirm(id, idempotencyKey string) error
	Cancel(id string) error
	State(id string) BookingState
	ConfirmationEvents(id string) int
}

The adapter could call an in-memory service, an HTTP API or a test deployment. Its State method normalizes a not-found response to Missing. ConfirmationEvents might read a fake publisher or drain a test outbox. Those details stay outside the model.

3. Turn commands into Rapid actions

Rapid’s T.Repeat generates a sequence from a map of named actions. For a larger model, StateMachineActions builds that map from exported action methods. A method named Check is reserved for invariants and runs before and after every non-skipped action. Rapid’s repository includes a complete queue state-machine example.

The examples below assume that the system exposes ErrAlreadyExists and ErrInvalidTransition. A small helper compares those errors with errors.Is:

func expectError(t *rapid.T, got, want error) {
	t.Helper()
	if !errors.Is(got, want) {
		t.Fatalf("error mismatch: got %v, want %v", got, want)
	}
}

The Create action predicts either success or ErrAlreadyExists from the current model state:

func (m *BookingModel) Create(t *rapid.T) {
	var want error
	if m.state != Missing {
		want = ErrAlreadyExists
	}

	got := m.sut.Create(m.id)
	expectError(t, got, want)

	if want == nil {
		m.state = Pending
	}
}

The action calls the real system first. If its response differs from the prediction, expectError stops the test. The model changes only after the response agrees.

Confirm also describes the idempotency contract. The same key is reused whenever Rapid selects this action:

func (m *BookingModel) Confirm(t *rapid.T) {
	want := ErrInvalidTransition

	switch m.state {
	case Pending:
		want = nil
	case Confirmed:
		want = nil // retry with the same idempotency key
	}

	got := m.sut.Confirm(m.id, "confirm-command")
	expectError(t, got, want)

	if m.state == Pending {
		m.state = Confirmed
		m.confirmationEvents++
	}
}

Confirming a pending booking changes its state and records one expected event. Confirming it again succeeds but changes neither. Confirming a missing or cancelled booking must return ErrInvalidTransition.

Cancellation has two valid starting states:

func (m *BookingModel) Cancel(t *rapid.T) {
	want := ErrInvalidTransition
	if m.state == Pending || m.state == Confirmed {
		want = nil
	}

	got := m.sut.Cancel(m.id)
	expectError(t, got, want)

	if want == nil {
		m.state = Cancelled
	}
}

I do not skip invalid transitions here. Rejection and preservation of state are part of the public behavior I want to test. I use t.Skip only for an action that is meaningless outside its precondition and whose invalid form is not part of the contract.

Check compares observations with the model after each command:

func (m *BookingModel) Check(t *rapid.T) {
	if got := m.sut.State(m.id); got != m.state {
		t.Fatalf("state mismatch: got %q, want %q", got, m.state)
	}

	gotEvents := m.sut.ConfirmationEvents(m.id)
	if gotEvents > 1 {
		t.Fatalf("confirmation was applied more than once")
	}

	if gotEvents != m.confirmationEvents {
		t.Fatalf(
			"confirmation events: got %d, want %d",
			gotEvents,
			m.confirmationEvents,
		)
	}
}

The test creates a fresh system for each generated history and asks Rapid to repeat the actions:

func TestBookingLifecycle(t *testing.T) {
	rapid.Check(t, func(t *rapid.T) {
		model := &BookingModel{
			state: Missing,
			sut:   newIsolatedBookingSystem(t),
			id:    "booking-1",
		}

		t.Repeat(rapid.StateMachineActions(model))
	})
}

newIsolatedBookingSystem is the boundary between the generic test pattern and the application. It must reset the database, fake queues and any other observable state. If histories leak state into one another, the test no longer has a reliable starting point.

4. Shrinking a failing history

Suppose the service treats an idempotent retry as a second confirmation and publishes another event. Rapid might first find the failure in a noisy history:

create
confirm
confirm
cancel
cancel
create

Because Rapid controls the action choices, it can minimize the generated data that produced the history. The useful counterexample is likely to become:

create
confirm
confirm

That is the stateful equivalent of shrinking a long string to the character that breaks a parser. The minimized history is usually good material for a named regression test, especially when it documents a production bug.

When an action also needs generated arguments, I draw them inside the action with stable labels. Randomness hidden inside the system or test helpers gives the shrinker less control over the failure.

5. Designing a useful model

Comparing one state enum is a start, but the most useful checks are often at the boundary of the system:

• returned values and domain errors
• durable state visible through the public API
• emitted events, messages or audit records
• resource invariants such as capacity never becoming negative
• idempotency, including the absence of duplicate effects

The model and the implementation do not need identical internal state. They need to agree on behavior that callers can observe. If the production service has an intermediate Confirming state, for example, the adapter can wait for the operation to settle and map the result to the model’s Confirmed state.

I keep the model independent from the implementation. Reusing the production transition table or its helper functions would allow one mistake to satisfy both sides of the comparison. The model should remain small enough to inspect; if it starts accumulating database schemas, retry loops and implementation-specific phases, I narrow the property.

Valid paths are not the whole contract. Incorrect rejection behavior can change state or emit an event before returning an error, so invalid commands deserve explicit actions when those effects matter.

For asynchronous systems, I prefer deterministic test controls: explicitly run a worker, drain a queue or advance a fake clock. Go’s testing/synctest provides fake time and quiescence detection for goroutines running inside a test bubble. Every generated history also needs isolated storage, queues, clocks and identifiers. Sleeping until the expected state appears makes failures slower and can turn a behavioral test into a timing test.

A sequential state machine can represent retries and message delivery order as commands. It does not explore thread interleavings by itself; concurrency needs a separate test or a model that controls the scheduler.

6. Choosing the level of testing

These techniques cover different kinds of uncertainty:

The last row is related but distinct. Once states, transitions and invariants are explicit, the test already contains a small model of the system. A model-based test samples paths through that model and executes them against real code. Tools such as Alloy and TLA+ analyze an abstract specification directly and can explore its bounded state space more systematically.

The booking model began as a test oracle, but it is already close to a specification. The next question I want to explore is what changes when I stop sampling histories and ask a model checker to explore them.