benchgraph: survival plot + trimmed head-to-head report - #13
Merged
Conversation
Reframe the preprocessor section of BENCHGRAPH.md around the direct head-to-head: ltlsynt vs preprocessor+ltlsynt. - Add a cactus/survival plot (docs/benchgraph/survival.png): per engine, the i-th fastest definitive solve (SOLVED or UNREAL), log-time, timeout line, solved counts in the legend. Curve further right = solves more; lower = faster. - Trim write_report to the essentials: run params, self-contained %, a solved-within-timeout table with the net gain, both-solved speedup, the embedded plot, and a correctness line (false-UNREAL / false-REAL vs the ltlsynt oracle). Drops the verbose residual-reduction/complexity prose. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
Both bugs are under-approximations (strengthenings): sound for a REALIZABLE verdict, but their UNREALIZABLE verdict is not trustworthy. Found via lily/lilydemo19 and lily/lilydemo23 in the corpus benchgraph. 1. certify_reachability / certify_persistence pinned a controllable output to a constant (o:=true) for `F o` / `FG o` even when the output was NOT free — despite the comment saying "free controllable output". For an output coupled via a mutex `!(hl&&fl)`, pinning `hl:=true` collapsed it to `!fl`, falsely making the `fl` response cluster UNREALIZABLE. They now decline when the output is referenced by any other constraint (output_constrained_elsewhere). The mutex there is an INVARIANT (no explicit G), so a CAND_MUTEX check would miss it — the direct support check is the right level. Updates the reach_blocked golden, which had documented the bug (its own description says "not free -> residual" yet it certified). 2. cluster_assumption_mask drops a liveness assumption from a safety-only cluster; its comment proves that sound for REALIZABLE only. So when a SAFETY cluster reports UNREAL and the spec has a liveness assumption, re-solve the cluster with all assumptions kept (prune=false) via the authoritative ltlsynt; flip to REAL only if ltlsynt produces a controller (cannot introduce a false-REAL). Gated on !has_liveness so it never re-runs the slow liveness tail. lilydemo19/lilydemo23 now SOLVE; inv_decline/cluster_assume/amba_unreal stay UNREAL; 194/194 tests green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
Audit and classify every certifier by which verdict it is sound for, so the
under-approximations are explicit and the composition can flag them.
- VerdictTrust { TRUST_EXACT, TRUST_UNDER } + block_trust(Block*) registry.
UNDER (strategy commitment, strengthens the residual; REAL sound, UNREAL not):
reachability, persistence, response/server, arbiter, round-robin,
global-recurrence-switch, safety-invariant. EXACT (forced-value substitution,
equivalence-preserving): definition, delayed-definition, reaction, set-reset,
toggle, fixed-delay, guarded-next, and the mutex safety invariant. No
certifier OVER-approximates (false-REALs would be an OVER path; the --verify
controller model-check is their guard).
- CsnfComposition.may_strengthen: set when an accepted block is UNDER.
Audit result: every UNDER certifier is soundly guarded against output coupling —
reachability/persistence by output_constrained_elsewhere (the false-UNREAL fix),
safety-invariant by output_is_free, and the (non-combinational) scheduler
families by the compose CONFLICT_SHARED_OUTPUT ejection. The marking documents
this and gives a hook for future under-approximations.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
The OxiDD W/R-safety game encoding is NOT exact — it can WEAKEN the spec and so emit a wrong controller (false-REAL), surfaced by the corpus benchgraph on the robot-motion family (box/evasion/follow/square): tlsfcompose called them realizable while ltlsynt (and Spot) say unrealizable. Verdict-trust: an over-approximation's REALIZABLE verdict is not trustworthy. - ComposeRoute.over_approx + exact=false on ROUTE_WR_SAFETY (the marking). - When the W/R OxiDD path returns a controller and no --verify model-check is configured, confirm it with the authoritative ltlsynt before trusting it: if ltlsynt produces a controller use that, if ltlsynt says UNREAL report UNREAL, and if ltlsynt is unavailable/inconclusive keep the OxiDD controller (so the Spot-verified /bin/false W/R tests still solve self-contained). With --verify set, the existing self-verification gate already covers it. box0/box1/evasion0/square5x5* now correctly report UNREALIZABLE; correct W/R specs still solve; 194/194 tests green (route-stats goldens updated for exact 1->0). (follow0/follow1 remain REAL in BOTH split and non-split and ltlsynt agrees on the cluster — a separate tlsfcompose-vs-syfco translation discrepancy, not this bug.) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
Full 2545-spec head-to-head, ltlsynt vs preprocessor+ltlsynt, 30s/run. With the verdict-trust fixes: 0 false-UNREAL across the corpus. At a 30s budget the preprocessor net-loses on completeness (the decomposition/OxiDD overhead costs the timeout race), so this captures the no-verify pipeline before the W/R over-approx fix (which removes the false-REALs it shows). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
A large cluster's LTL formula (hundreds of KB) exceeds the per-argument exec limit (Linux MAX_ARG_STRLEN, 128 KiB), so a `--formula=<huge>` spawn fails with E2BIG. That silently disabled the ltlsynt fallback / re-validation / verifier on big specs, so tlsfcompose kept whatever the (possibly wrong) in-process backend produced — surfacing as false-REALs on the big robot-motion specs (follow0/follow1) where the W/R over-approx re-validation could not reach ltlsynt to refute the bogus controller. Switch every formula-to-subprocess path to a file: - run_ltlsynt: write the formula to a temp file, invoke `ltlsynt -F FILE`. - controller_violates_spec (--verify gate): `--formula-file FILE`. - the generated compose.sh driver: `ltlsynt -F FILE`. follow0/follow1 now correctly report UNREALIZABLE; 194/194 tests green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
The existing --input-signals/--output-signals print the *declared* signals (bus notation like g[0..0], parameters unresolved) on the raw spec — not the scalar atoms a synthesizer needs. Add --expanded-ins/--expanded-outs, which expand() the spec (buses unrolled, parameters resolved) and emit a comma-separated, space-free list ready to paste into `ltlsynt --ins=…/--outs=…`, matching syfco --print-*-signals. tlsfinfo --expanded-outs full_arbiter.tlsf -> g_0,g_1 Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
…section)
- Replace the command-line `ltlsynt --formula=…` / `-f "$(…)"` examples with the
file-based `-F` form: a large cluster formula overflows the exec arg limit
(E2BIG), matching the in-tool fix.
- Use the new `tlsfinfo --expanded-ins/--expanded-outs` for the synthesizer
interface (the old `--input-signals | lc` left bus notation like g[0..0]
unexpanded, breaking parametric specs); document the flags under "inspect".
- Point the benchgraph reference at the actual section name
("ltlsynt vs preprocessor + ltlsynt"); the old "Preprocessor speed &
complexity" heading no longer exists.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
# Conflicts: # src/templates.c # test/cases/reach_blocked.residual
…nded-* - clang-format the merged compose_*/templates/main_tlsfcompose sources. - Regenerate test/cases/reach_blocked.csnf: the false-UNREAL fix makes the reachability certifier skip an output constrained elsewhere, so the block is now `candidate safety-invariant`, not `solved reachability` (the old golden predated the fix; it only runs in the research-tools build, which build-oxidd doesn't enable, so the local suite missed it). - Add info_expanded_ins/info_expanded_outs golden tests covering the new tlsfinfo --expanded-ins/--expanded-outs flags. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
The verdict-trust additions (may_strengthen, VerdictTrust/block_trust) were not clang-formatted; format only checked the .c files locally. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
Replace the old 31.8%/×35/151 baseline with the current run (16.5% self-contained, 0 false-UNREAL, 0 false-REAL, net +12) and add the verdict-trust framework, W/R over-approx false-REAL fix, E2BIG file-based formula passing, and tlsfinfo --expanded-ins/--expanded-outs to the Done list. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
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.
Reframe the preprocessor section of BENCHGRAPH.md around the direct
head-to-head: ltlsynt vs preprocessor+ltlsynt.
i-th fastest definitive solve (SOLVED or UNREAL), log-time, timeout line,
solved counts in the legend. Curve further right = solves more; lower = faster.
solved-within-timeout table with the net gain, both-solved speedup, the
embedded plot, and a correctness line (false-UNREAL / false-REAL vs the
ltlsynt oracle). Drops the verbose residual-reduction/complexity prose.
Co-Authored-By: Claude Opus 4.8 noreply@anthropic.com
Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV