test: model the state machine as a hypothesis RuleBasedStateMachine - #112
Merged
Conversation
The four properties in test_state_machine_properties.py generate a config and then drive a fixed, hand-written sequence. That finds arithmetic errors at the boundaries it is pointed at, but not order-dependent corruption: an override during a probe round, a probe settling an era late, a manual reset while the open wait elapses. Add a RuleBasedStateMachine that generates the sequence too. Rules: advance the FakeClock, admit, settle, release, auto-transition, force_open, disable, metrics_only, reset. An admitted call yields a ticket (the generation the call layer captures) into a bundle, and settling consumes one — so probes can settle out of order or long after their era ended. The model carries its own prediction of the state, the generation, the window aggregates and the probe budget, derived from the documented contract, and @invariants compare it against the machine after every step — including the #79 contract that no automatic transition undoes an operator override, and the retry_after estimate in OPEN. The shared Config strategy moves to conftest as configs(); the model narrows minimum_number_of_calls so a bounded run reaches the probe round instead of spending every step in CLOSED. Bounded by max_examples / stateful_step_count: the file runs in ~1s. No counterexample against the current implementation. Verified it bites by mutation: loosening the concurrency cap, dropping the generation fence in record(), and dropping the guard in release_probe() each fail the model. Closes #106
Coverage report
This PR does not seem to contain any modification to coverable code. |
Contributor
CI has run the whole suite on free-threaded 3.14t since #111, and tests/test_concurrency.py is what backs the thread-safety claim, but the package metadata said nothing about it. There is no `3.14t` classifier — free-threading is a separate trove axis — so declare `Free Threading :: 3 - Stable` alongside the version classifiers. Verified with `twine check`.
The 3.14t entry said free-threaded builds are "not a distribution target (no wheels, no classifiers)". The wheel half still holds — the package is pure Python, so one wheel serves both flavours — but the classifier is now declared, so the entry can no longer claim otherwise.
5 tasks
bagowix
added a commit
that referenced
this pull request
Aug 1, 2026
## Summary The `RuleBasedStateMachine` from #106 (#112) shrank a counterexample on `main`. It reproduces locally but not in CI — hypothesis found it on a seed CI has not drawn yet, so today it is a latent flake rather than a red build: ``` config: minimum_number_of_calls=1, failure_rate_threshold=1.0, permitted_calls_in_half_open=1, max_concurrent_probes=1 admit → settle(FAILURE) # CLOSED → OPEN advance(1.0) # the open wait elapses admit → settle(FAILURE) # HALF_OPEN probe fails → OPEN ``` At the last step the machine still holds `_probes_admitted == 1` while the model predicted `0`: the model forgets the probe round on *every* transition, and the machine clears it on entry to `HALF_OPEN` (`_to_half_open`) and `CLOSED` (`_close`), not on `_open()`. **The machine is right.** The counters are read only by `_admits_probe`, which is reachable only in `HALF_OPEN`, and `HALF_OPEN` is only ever entered through `_to_half_open()` — which resets them. Adding a reset to `_open()` would be defensive code written for a test, not for a caller. What the model asserted there was an internal detail the contract does not promise. So `probe_budget_holds` now compares the machine's counters against the model only in `HALF_OPEN`, where the budget is spent and the contract defines it; the cap assertions (`max_concurrent_probes`, `permitted_calls_in_half_open`) stay unconditional. No production code changes. ## Test plan - [x] `uv run pytest tests/test_state_machine_model.py` passes, plus 6 explicit `--hypothesis-seed` runs - [x] **Mutation check — the invariant still bites.** With the `self._probes_in_flight -= 1` line deleted from `StateMachine._record_probe` (a leaked probe slot), the scoped invariant fails within one run at the same assertion. Scoping removed the false alarm, not the sensitivity. - [x] The shrunk sequence is pinned as `test__probe_budget__failed_probe_reopens__next_round_starts_full`, as `tests/CLAUDE.md` requires — it asserts what *is* promised: the next probe round starts from a full budget. - [x] `uv run pytest --cov` — 549 passed, 100.00% - [x] `uv run prek run --all-files` clean ## Related issues Follow-up to #106 / #112. Independent of #113.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
tests/test_state_machine_properties.pygenerates a config and then drives afixed, hand-written sequence — good at the boundaries it is pointed at, blind
to order-dependent corruption. This adds
tests/test_state_machine_model.py: ahypothesis
RuleBasedStateMachinethat generates the sequence as well, so anoverride during a probe round or a probe settling an era late has somewhere to
show up.
advance(fractions of the open wait, so1.0lands exactly onthe boundary),
admit,settle,release,auto_transition,force_open,disable,metrics_only,reset.captures — and
settle/releaseconsume one, so probes settle out oforder, or an era late.
than values read back from the machine: state, generation (the stale-outcome
fence), the Make manual controls authoritative for coordinated breakers #79 contract that no automatic transition undoes an operator
override, the probe budget cross-checked against the machine's own
accounting, window aggregates vs. the recorded history, and
retry_after()as the remaining wait in OPEN.
FakeClock.The
Configstrategy moves toconftest.pyasconfigs(), now shared by bothhypothesis suites. The model narrows
minimum_number_of_callson top of it —every recorded outcome costs two steps, so an unnarrowed run spends all 50
steps inside CLOSED and never reaches a probe round. The existing four
properties stay unchanged (bar the import).
No counterexample against the current implementation, so there is no regression
test to pin yet. Verified the model actually bites, by mutation:
_admit_probe:>=→>on the concurrency capadmitpredicted a rejection)record(): drop the generation fencewindow_matches_history)release_probe(): drop the generation/state guardprobe_budget_holds,-1 == 0)Also here, since it is the same free-threading thread:
pyproject.tomlnowdeclares
Programming Language :: Python :: Free Threading :: 3 - Stable.There is no
3.14tversion classifier — free-threading is a separate troveaxis. CI has run the whole suite on 3.14t since #111 and
tests/test_concurrency.pybacks the claim, but the metadata said nothingabout it. The #111 changelog entry asserted the opposite ("no wheels, no
classifiers"), so it is corrected in the same commit: the wheel half still
holds (pure Python — one wheel serves both flavours), the classifier half no
longer does. Verified with
twine checkon the built sdist and wheel.Checklist
coverage 100%; the model file runs in ~1.0s (
max_examples=200,stateful_step_count=50)uv run ruff format --checkanduv run ruff checkpassuv run mypyanduv run pyrightpassdocs/) for user-facing changes — n/a: no public APIsurface changed (the test-suite side is documented in
tests/CLAUDE.md)CHANGELOG.md[Unreleased]updatedRelated issues
Closes #106.