Skip to content

Stateful Testing & Documentation #31

Merged
kommundsen merged 19 commits intomainfrom
feat/stateful-testing
Apr 3, 2026
Merged

Stateful Testing & Documentation #31
kommundsen merged 19 commits intomainfrom
feat/stateful-testing

Conversation

@kommundsen
Copy link
Copy Markdown
Owner

@kommundsen kommundsen commented Apr 2, 2026

Core feature: IStateMachine<TState, TCommand> — an interface-based model for testing stateful systems by generating and shrinking command sequences.
Key capabilities:

  • State machine interface — users implement InitialState(), Commands(state) (state-dependent availability), RunCommand(state, cmd), and Invariant(state)
  • Gen.StateMachine<TMachine,TState,TCommand>() — public factory that generates StateMachineRun values via the existing [Property] + [From] infrastructure
  • Automatic sequence shrinking — CommandSequenceShrinkPass (tier 0) reduces failing sequences via truncate-from-end, binary-halve, and delete-one-at-a-time sub-passes; uses a new IRNodeKind.CommandStart = 7 sentinel for span identification
  • Rich failure output — StateMachineFormatter formats failures as step sequences (state = InitialState(); RunCommand(state, Push(0)); Invariant(state); // ← fails here), registered globally so all adapters pick it up
  • End-to-end examples — StackMachine and QueueMachine with planted bugs to validate find + shrink behavior
  • Self-tests — property-based invariant tests over the shrinker itself (monotone, idempotent, preserves failure)
  • Documentation — DocFX stateful testing guide + XML doc audit on all new public API

@kommundsen kommundsen added documentation Improvements or additions to documentation enhancement New feature or request labels Apr 2, 2026
@kommundsen kommundsen changed the title Statful testing Stateful Testing & Documentation Apr 2, 2026
@kommundsen kommundsen force-pushed the feat/stateful-testing branch from 2eb0353 to d2bb460 Compare April 3, 2026 16:48
kommundsen added 18 commits April 3, 2026 18:48
@kommundsen
Adds IStateMachine<TState, TCommand> interface for stateful testing
bfd3fc2 
- Four-method contract: InitialState, Commands, RunCommand, Invariant
- Commands returns state-dependent IEnumerable<Strategy<TCommand>>,
  enabling the engine to draw applicable commands per step
- Invariant throws on violation; returns normally for valid states
- Full XML doc on all members per ADR-0015
@kommundsen
Adds StateMachineRun<TState> and ExecutedStep<TState> result types
506aa30 
- StateMachineRun carries the executed step sequence, failure step index,
  final state, and a Passed convenience property
- ExecutedStep is a readonly record struct pairing post-command state with
  a human-readable command label for use in failure output
@kommundsen
Adds StateMachineStrategy for state-dependent command sequence genera…
922fa15 
…tion

- Draws a bounded length integer then loops, inserting a CommandStart
  sentinel before each command draw so the shrinker can identify command
  boundaries in the IR stream
- Stops early when Commands() returns empty or Invariant() throws;
  records the failure step index on the run
- Adds IRNodeKind.CommandStart = 7 and supporting IRNode/ConjectureData
  plumbing for the new sentinel node kind
@kommundsen
Adds Generate.StateMachine<TMachine,TState,TCommand> public entry point
e66f8fa
@kommundsen
Extracts StateMachineRunner to decouple execution from IR drawing
40dcd54 
- Adds StateMachineRunner.Execute — a pure function that takes a machine
  and a pre-drawn command list, runs each command, checks invariants, and
  returns a StateMachineRun with steps and failure index
- StateMachineStrategy.Generate now draws commands into a list, then
  delegates all execution and step recording to StateMachineRunner
@kommundsen
Propagates invariant failures from StateMachineStrategy to TestRunner
45e1574 
- StateMachineRunner.Execute now captures the invariant exception alongside
  the run result; StateMachineStrategy throws a wrapped exception with a
  formatted step sequence when the run fails
- StateMachineRunner gains FormatSteps to produce the failure message,
  listing each executed step with a ✗ marker at the failure point
@kommundsen
Adds CommandSequenceShrinkPass truncate-from-end sub-pass
9eedfd0 
- Scans IR nodes for CommandStart sentinels to locate command span
  boundaries, then removes the last command span and decrements the
  length integer to keep replay consistent
- Returns false when fewer than two commands are present (nothing to
  truncate) or when the truncated candidate is no longer interesting
@kommundsen
Adds binary-halve and delete-one sub-passes to CommandSequenceShrinkPass
5dccb60 
- TryBinaryHalve: removes the second half of the command sequence in one step
  (faster convergence than removing one at a time)
- TryDeleteOne: tries removing each command span individually; skips deletions
  that make the sequence non-interesting, enabling state-dependent shrinking
- Both share a new BuildPrefixCandidate helper; TryDeleteOne composes
  ShrinkHelper.WithoutInterval + Replace instead of reimplementing them
- Updated the existing single-step test to use a minimum-count predicate,
  since TryDeleteOne can now delete the last command when the predicate allows it
@kommundsen
Registers CommandSequenceShrinkPass in Shrinker tier 0
1fe9b70 
- Adds CommandSequenceShrinkPass to tier 0 alongside ZeroBlocksPass,
  DeleteBlocksPass, and IntervalDeletionPass
- Updates ShrinkerPassOrderTests: pass count 10→11, tier-0 count 3→4
- Adds ShrinkIntegrationTests: end-to-end shrink of a state machine that
  fails at state >= 3 converges to exactly 3 steps
@kommundsen
Adds StateMachineFormatter for step-sequence counterexample output
4a82f7c 
- Formats failing runs as pseudocode: InitialState declaration,
  RunCommand per step, then Invariant annotation at the failure point
- StateMachineStrategy static ctor auto-registers the formatter with
  FormatterRegistry so CounterexampleFormatter picks it up automatically
@kommundsen
Adds StateMachineReportingTests to all four framework adapters
0f18188 
- Verifies StateMachineFormatter is auto-registered when StateMachineStrategy
  is instantiated (via FormatterRegistry)
- Verifies formatter output contains step-sequence format:
  "state = InitialState();" and "// <- fails here"
- Verifies seed reproduction line appears in the failure message
- Verifies ShrinkCount is positive after a shrinkable failure
@kommundsen
Adds StackStateMachineTests end-to-end suite for cycle 4.6.1
975a526 
- BuggyStackMachine plants an off-by-one ModelCount decrement on Pop;
  three tests verify Conjecture finds the failure, shrinks to exactly
  2 commands ([Push, Pop]), and records ShrinkCount > 0
- CorrectStackMachine (no bug) verifies the full example budget passes
  without a counterexample
- StateAwareStackMachine exercises state-dependent command availability:
  Pop only yielded when Stack.Count > 0; passing result confirms the
  engine never selects Pop on an empty stack
- Commands is fixed-size (always [Push, Pop]) in the buggy/correct
  machines to avoid a stale OneOf-index shrinker artefact that arises
  when Commands size changes with state
@kommundsen
Adds QueueStateMachineTests end-to-end suite for cycle 4.6.2
9b97c35 
- BuggyQueueMachine plants a value-independent off-by-one in Peek
  (returns front+1 when Count > 1), so [Enqueue(0), Enqueue(0), Peek]
  is the minimal 3-step counterexample after shrinking
- CorrectQueueMachine verifies the passing path across 100 examples
- StateAwareQueueMachine exercises state-dependent command availability:
  Dequeue/Peek only offered when Count > 0; an engine violation would
  throw immediately, causing the test to fail
@kommundsen
Adds StateMachineSelfTests for shrinker invariants on command sequences
259f22d 
- BuggyCounterMachine (Inc/Nop commands, fails when counter ≥ 3) provides
  a planted-bug machine whose minimal counterexample is [Inc, Inc, Inc]
- MachineStrategy uses Gen.Compose to vary the step budget [5, 20], giving
  the shrinker runs of different lengths to reduce
- Three invariants checked: monotone shrinking (step count never increases),
  failure preservation (shrunk run replays as Interesting), and idempotence
  (re-shrinking a fully shrunk result makes zero additional progress)
@kommundsen
Marks cycle 4.8.1 complete in implementation plan
b2091e3
@kommundsen
Adds StateMachineBenchmarks for generation and shrinking throughput
b25adca 
- StateMachineGeneration_Passing: 50-step sequences on a never-failing machine
- StateMachineGeneration_Failing: same path with invariant violation detection
- StateMachineShrinking_Short/Long: full find+shrink via TestRunner with fixed seed
- Inline CounterMachine variants keep domain logic out of engine overhead
@kommundsen
Documents stateful testing guide with StackMachine example
dd4d149 
- Covers IStateMachine<TState, TCommand> implementation pattern
- Shows annotated failure output, state-dependent Commands, shrinking, and seed reproduction
- Registers the guide in the Guides toc
@kommundsen
Documents Generate.StateMachine with returns tag and example block
7a056d9
@kommundsen kommundsen force-pushed the feat/stateful-testing branch from d2bb460 to 7a056d9 Compare April 3, 2026 16:49
@kommundsen
Fixes flaky ShrinkCount > 0 assertions in state machine shrink tests
53abf0f 
StateMachineStrategy draws sequence length from NextInteger(0, maxSteps).
When the first failing example happened to land exactly on the minimum
failing length (3 steps), the shrinker had nothing to reduce, leaving
ShrinkCount = 0. With maxSteps=20 this produced a ~5.6% flake rate.

Pins Seed = 1UL on the five affected tests. With this seed the first
generated sequence is length 14 (maxSteps=20) or 26 (maxSteps=50),
both well above the minimum, so ShrinkCount > 0 is always guaranteed.
@kommundsen kommundsen marked this pull request as ready for review April 3, 2026 17:35
@kommundsen kommundsen merged commit 3d1b575 into main Apr 3, 2026
1 check passed
@kommundsen kommundsen deleted the feat/stateful-testing branch April 3, 2026 17:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

documentation Improvements or additions to documentation enhancement New feature or request

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@kommundsen