Stateful model-based tests

Stateful & Model-Based Testing

Use this skill when bugs depend on the ordering, repetition, or interleaving of operations across stateful entities (credit wallets, subscriptions, orders, approvals, inventory reservations, or cache/DB synchronization).

State-Machine Command Architecture (Lamport & Hughes)

Model the system as an explicit state machine driven by generated sequences of Commands (fc.commands / fc.asyncModelRun in fast-check, RuleBasedStateMachine in Hypothesis):

1. Shadow Model State ($M$):
   • Maintain a minimal, transparent in-memory representation of the expected domain state (e.g., Map<AccountId, { balance: bigint, reserved: bigint, seenKeys: Set<string> }>).
   • Keep $M$ simple and free of production infrastructure concerns (no SQL, no caching, no framework middleware).
2. Command Catalog ($C_1, C_2, \dots, C_k$):
   • Define a command for each domain action, including adversarial and duplicate actions:
     • Normal lifecycle actions (GrantCredit, Reserve, Capture, Release, Refund, Cancel).
     • Replay / duplicate actions (ReplayLastRequestWithSameIdempotencyKey, DuplicateWebhookDelivery).
     • Invalid / out-of-order actions (CaptureAlreadyReleasedReservation, OverRefund, ApproveOwnRequest).
3. Command Contract (check + run):
   • Precondition (check(model)): Determines whether the command is applicable in the current model state. Include commands that specifically test invalid state transitions so rejection behavior is verified too.
   • Execution (run(model, realSystem)):
     1. Execute the operation against realSystem.
     2. If the operation is legal in model, update model and assert that realSystem's return value and observable state match model.
     3. If the operation is illegal in model (e.g., insufficient funds or terminal state), assert that realSystem rejects it with the expected domain error and that realSystem state remains completely unchanged.
   • Global Step Invariant: After every command in the sequence, assert global cross-entity invariants (e.g., ledger conservation, no negative available balances, cache matches DB).

Designing Effective State-Space Exploration

• Pool-Based Entity References: Draw IDs, accounts, and reservations from bounded pools (Bundles in Hypothesis or shared model arrays in fast-check) so generated commands repeatedly collide on the same entities instead of creating a fresh, isolated entity on every step.
• Test State Re-Entry & Loops: Ensure command sequences can cycle through reserve -> release -> reserve -> partial capture -> refund or subscribe -> cancel -> reactivate -> upgrade to expose stale flags or leaked locks.

Checklist

• Does the shadow model track the essential business state clearly without copying production code?
• Do generated command sequences include replays, out-of-order calls, and rejected transitions alongside happy-path steps?
• Do commands draw from a shared pool of entities so multiple operations hit the same records?
• Are global state invariants verified after every individual command step, not only at the end of the run?