# Regression guard for the lazy stale-defer prune at the RTC boundary
# in `src/semantics/lts/mod.rs::lts_explore_state` (the `// Handle
# deferred blocks` block). Mirrors dzn's `prune_deferred` from
# `share/dezyne/templates/makreel/defer.mcrl2`, which dzn's `defer_queue`
# process runs on every `defer_skip(s)` action — and `defer_skip` is
# emitted by the `<the-end>` process at end-of-RTC, NOT per assignment
# (scmackerel/makreel.scm). So the prune is END-OF-RTC, not eager-per-
# assignment; an eager-per-assignment fix was attempted 2026-05-30 and
# broke wf-equivalence by eliminating reachable `<queue-full>` paths.
# See [[project_defer_state_blowup]].
#
# Pattern: 1 comp-var v0 + two events e0/f0. e0 sets v0=true AND
# queues a defer; f0 clears v0. After e0;f0 the queued defer's
# captured (v0=true) mismatches current (v0=false) — stale. Without
# the lazy RTC-boundary prune, the BFS would split states on stale
# queue contents.
#
# Counts (queue-size-defer=2 default):
#   - dzn:                                 71 states (golden)
#   - ours (lazy RTC prune):               19 states — wf-EQUAL to dzn
#   - ours with prune disabled (sentinel): 28 states
# `max-state-factor 0.30` → budget = ceil(0.30 × 71) = 22. ours-with-
# prune 19 ≤ 22 → PASS; without-prune 28 > 22 → FAIL.
((max-state-factor 0.30))
skip simulate
skip c
skip cs
skip scheme
skip javascript
