Model-based test barely reaches HALF_OPEN: rebalance the rule mix toward probe rounds

[bagowix]

Problem

The RuleBasedStateMachine from #106 / #112 almost never reaches HALF_OPEN,
so the probe round — the part of the machine with the most order-dependent
state (probe budget, generation fencing, out-of-order settles) — is effectively
not explored by the model.

Instrumenting StateMachineModel._transition and running the model exactly as
the suite runs it (max_examples=200, stateful_step_count=50, i.e. ~10 000
steps) gives, per state entered over the whole run:

entered	count
DISABLED	1726
METRICS_ONLY	1474
FORCED_OPEN	1121
CLOSED	908
OPEN	21
HALF_OPEN	7

Seven probe rounds in a whole run is not enough for the interleavings the model
exists to find. The probe_budget_holds invariant — the one that just had to
be scoped in #114 — fires on a handful of steps out of ten thousand.

Why

Hypothesis picks among the applicable rules roughly uniformly, and the rule mix
is stacked against the automatic path:

• Four of the nine rules are operator moves (force_open, disable,
  metrics_only, reset), and three of them jump straight into a terminal
  override state.
• Only reset leads back to CLOSED, and nothing leads out of an override
  automatically. So the walk spends its time bouncing between the three
  overrides and CLOSED.
• Reaching HALF_OPEN needs a long conjunction of the remaining rules with no
  override in between: enough admit/settle pairs to trip the window (each
  outcome costs two steps), then an advance past the open wait, then an
  admit. Any of the four operator rules in that stretch resets the progress.

Direction

Collapsing the three overrides into one rule with a sampled_from state
argument is the obvious first move — it takes the operator share of the rule
mix from 4/9 to 2/7 without losing a single reachable transition. On its own it
was not enough in a trial run (still 0 HALF_OPEN entries), and neither was
hypothesis.target() on the number of probe rounds alone (also 0). Together
they were:

variant	OPEN	HALF_OPEN
today	21	7
collapsed overrides only	6	0
target() only	1	0
collapsed + target()	682	622

(One run each, so treat the exact numbers as an order of magnitude, not a
measurement — but the last row is not noise.)

So the fix is probably: one override(state) rule, plus a teardown that
reports the per-example count of HALF_OPEN entries via target() so
Hypothesis's targeted search steers toward probe rounds. Other levers worth
measuring before settling: a settle_all-style rule that drains the ticket
bundle in one step (an outcome currently costs two), and biasing advance
toward fractions ≥ 1.0.

Acceptance criteria

• The model reaches HALF_OPEN on a substantial fraction of examples rather
  than a handful of times per run, demonstrated by a measurement in the PR
  description (same instrumentation as above, before/after).
• No reachable transition is lost: FORCED_OPEN, DISABLED and METRICS_ONLY
  are all still entered, and the override-authoritative invariant from Make manual controls authoritative for coordinated breakers #79 still
  has something to check.
• The file stays within its runtime budget (tests/CLAUDE.md: "keep the whole
  file near a second").
• tests/CLAUDE.md's description of the model's rules is updated to match.

Non-goals

• Changing what the invariants assert — this is about reaching the states where
  they mean something, not about what they mean.
• Raising max_examples / stateful_step_count as the primary fix: it buys
  coverage linearly at linear cost, while the rule mix is the actual problem.