Chapter 7 of 8

Test transitions, histories, faults, and properties

Chapter 7

About 5 minutes · includes examples, an exercise, and references

Chapter at a glance

•Test reducers and transition tables first, then histories, adapters, and complete controlled environments.
•Use property-based, model-based, and model-checking methods to explore sequences and interleavings.
•Inject faults before and after every commit boundary and verify authoritative effects independently.

A loop test suite should challenge the controller's behavior over sequences, not only isolated functions or one happy path. The smallest test target is the pure reducer: given state and event, assert next state, commands, and invariants. The next target is a history: replay a sequence including duplicates, delays, cancellation, expiry, and recovery. Integration tests exercise effect adapters and persistence. System tests run the complete loop in a controlled environment with fault injection and authoritative outcome checks.

Start with transition-table coverage. Every legal state-event pair needs at least one test, every guard needs pass and fail cases, and every illegal pair needs defined behavior. Assert commands as data rather than executing them in reducer tests. Check monotonic fields, terminal absorption, authority predicates, budgets, and effect cardinality after each transition. A coverage map tied to the specification is more meaningful than statement coverage alone.

Property-based testing generates states and event sequences within a model and checks general claims. Useful properties include replay determinism, duplicate-event idempotency, consumed budget monotonicity, no write without approval, at most one confirmed effect per intent, and terminal states producing no ordinary commands. Generators should include invalid and boundary values, not only realistic averages. When a property fails, shrinking can reveal a minimal sequence such as approve, expire, stale dispatch.

Model-based testing maintains a simple reference machine and compares the implementation after generated commands. It is effective for queues, workflows, and APIs because the reference model captures semantics without production infrastructure. Commands run against the system under test; observations update the model; state queries compare visible outcomes. Record the random seed and minimized command sequence so every failure becomes reproducible.

Model checking complements generated tests by exhaustively exploring a finite abstraction. In TLA+, define Init, Next, variables, invariants, and liveness properties. Bound identifiers and counters while preserving the interleavings that matter. Ask the checker to reorder duplicate delivery, timeout, cancellation, lease expiry, approval, and effect confirmation. A liveness check requires fairness assumptions; otherwise the environment can legally withhold every response forever. Review counterexample traces with implementers and convert them into tests.

Replay tests protect long-lived instances from incompatible code changes. Maintain a corpus of representative and adversarial histories from each behavior version. New workflow code must replay them to the expected state and command markers without nondeterministic divergence. Add a history whenever an incident reveals a new interleaving. Test checkpoints by comparing full replay with checkpoint-plus-tail and by corrupting digest, version, or sequence metadata.

Fault injection should target the uncertainty boundary, not merely return generic errors. Crash before intent commit, after intent commit, before dispatch, after destination commit but before response, after result receipt but before state commit, and during compensation. Deliver every event twice. Delay old observations until newer state exists. Drop and reorder messages where the transport allows it. Pause a worker past lease expiry. Advance the clock across approval and run deadlines. Partition the authoritative read used for reconciliation.

Use virtual time so retry, timer, and expiry tests finish instantly and deterministically. Inject clock and random sources; record scheduled wake-ups rather than sleeping. A fake destination should implement idempotency and an effect ledger, and support scripted faults before and after commit. Assertions inspect the ledger to prove what happened, not what the workflow believes happened. This separation catches false success and false failure.

Concurrency tests need controlled scheduling. Barriers can pause two workers after reading the same version, then release them in chosen orders. Assert only one commit succeeds and the loser reloads. Test fencing by letting an old owner call the destination after a new token is active. Race cancellation against confirmation in both orders. Repeat under load for implementation defects, but keep deterministic schedule tests as the diagnostic core.

For model-driven policies, freeze or stub policy outputs when testing the controller. Script malformed actions, unknown tools, repeated equivalent actions, excessive calls, contradictory completion claims, and attacks embedded in observations. Separately evaluate model decision quality across repeated trials. Mixing both sources of variance in every test makes lifecycle regressions hard to localize.

Define oracles at multiple layers. State oracle checks projection. Trace oracle checks ordering and authority. Effect oracle checks the real or simulated destination. Resource oracle checks steps, elapsed logical time, retries, and writes. Security oracle checks information flows and denied capabilities. A case passes only if all required oracles agree. Snapshotting a final chat transcript is a weak substitute.

Test evidence should be versioned with workflow code, event schemas, adapters, policies, and fixtures. A release report lists property results, replay compatibility, fault matrix, performance bounds, and unresolved risks. The goal is not to prove that dependencies never fail. It is to prove that each injected uncertainty maps to a bounded, invariant-preserving state and that recovery does not invent or duplicate effects.

Key points

Test reducers and transition tables first, then histories, adapters, and complete controlled environments.
Use property-based, model-based, and model-checking methods to explore sequences and interleavings.
Inject faults before and after every commit boundary and verify authoritative effects independently.
Keep policy variance separate from controller correctness and preserve replay histories as upgrade gates.

Enumerate short event sequences against invariants

Read the expected behavior in the surrounding walkthrough, then copy and run this reference implementation.

Enumerate short event sequences against invariantspython

from dataclasses import dataclass, replace
from itertools import product

@dataclass(frozen=True)
class State:
    approved: bool = False
    writes: int = 0
    terminal: bool = False

def step(s: State, event: str) -> State:
    if s.terminal:
        return s
    if event == "approve":
        return replace(s, approved=True)
    if event == "write" and s.approved and s.writes == 0:
        return replace(s, writes=1)
    if event == "finish":
        return replace(s, terminal=True)
    return s

def invariant(s: State) -> bool:
    return 0 <= s.writes <= 1 and (s.writes == 0 or s.approved)

events = ("approve", "write", "finish", "duplicate_write")
checked = 0
for length in range(5):
    for sequence in product(events, repeat=length):
        state = State()
        for event in sequence:
            normalized = "write" if event == "duplicate_write" else event
            state = step(state, normalized)
            assert invariant(state), (sequence, state)
        checked += 1
print({"sequences_checked": checked})

Worked examples

Toy

Generated duplicate-event property

A reducer applies a generated list of deposit events, then receives the same list again.

Each event has a stable identity. The property asserts the balance and receipt set remain unchanged after duplicate delivery. A deliberately faulty reducer fails with a one-event counterexample. The minimized case explains exactly which deduplication state is missing.

The property ranges across amounts and orderings.
Failure shrinks to a reproducible sequence.
Effect count is checked in addition to state.

Application

Crash matrix for report delivery

A test harness crashes the worker at six points around outbox dispatch and storage commit.

Recovery reloads history and outbox. The fake storage service records stable keys and can lose responses after commit. Every case eventually confirms one artifact or reaches a bounded operator state. Full replay and checkpoint replay yield identical projections.

All commit boundaries have named injection points.
The destination ledger is the effect oracle.
No process memory is required after restart.

System

Cancellation and stale-owner schedule

Two workers, a lease handoff, cancellation, and an external completion are scheduled in adversarial orders.

Barriers force the old worker to pause after reading. A new worker gets a higher fencing token and applies cancellation. The old write is rejected by the destination. A variant lets the original effect confirm first and requires cancellation to become too_late. Both traces preserve one-effect and terminal-consistency invariants.

The schedule is deterministic.
Fencing is checked at the destination.
Both legitimate event orders have defined outcomes.

Exercise

Build a fault-oriented verification matrix

Take a durable loop with at least one external write and design tests that prove its invariants through replay, duplication, and crashes.

Map every transition and guard to reducer tests, including illegal and boundary events.
Write five general properties and one finite formal abstraction for concurrency or authority.
Create fault points before and after each persistence and external-effect boundary.
Define state, trace, effect, resource, and security oracles plus a replay-compatibility corpus.

Success criteria

A minimal sequence reproduces every property failure.
Duplicate, reordered, and stale events preserve invariants.
No injected timeout is judged solely from the caller's exception.
Candidate workflow code replays every supported historical version deterministically.

Reflect: Which untested crash point currently separates an intended effect from the evidence that it occurred?