Add boolean-fragment UNREALIZABLE pre-check via BDD - #14
Merged
Conversation
Add a fast, sound structural pre-check for trivially unrealizable specs at the TLSF level (the analog of ltlsynt's try_create_direct_strategy input-only-G shortcut; acacia-bonsai issue #109's idea, here over OxiDD). It runs right after cover_build (whole-spec, pre-cluster) and decides UNREAL via a one-step environment win over the propositional fragment: G = conj of step-0 boolean guarantee bodies A = conj of step-0 boolean assumption bodies EnvWin = NOT exists outputs. NOT(A and NOT G) -> UNREAL iff EnvWin != empty Catches input-only-G (Light/Warnlight), output-can't-rescue, and UNSAT guarantees (G(o) and G(!o)). Verdict-trust class TRUST_OVER (new enum value): it refutes a *weakening* of the spec (drops temporal guarantees, keeps every assumption, bails on any temporal assumption), so its UNREALIZABLE is trustworthy, it never claims REALIZABLE, and it needs no re-validation -- the temporal-assumption bail is a strict superset of the cover_has_liveness_assumption UNREAL-trust concern. Surfaced under --route-stats as unreal_precheck=1. Tests (all OxiDD-gated; soundness guards): fires on input-only without ltlsynt, route-stats counter, output-rescue and assume-rescue stay silent (false-UNREAL guards), temporal-assume bails to the downstream path. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV
README: remove the syfco comparison/benchmarking references (the tlsf2ltl-vs-syfco perf claim, the check-against-syfco command, the syfco-style descriptive notes); keep only the canonical TLSF-format link. Drop the Limitations section. Make the scripts syfco-free: bench/bench.sh loses the syfco comparison columns but keeps the self-regression guard (--baseline/--check); benchgraph.py drops the syfco baseline mode and resolves the standalone-ltlsynt baseline to the tlsf-tools translation. benchgraph plots: only the head-to-head survival plot is current. Delete the 7 structural-census plots (built from tlsf-selection-2026 / tlsf-fin-selection-2026 + build-release-local, all no longer present) and mark scripts/benchgraph_plots.py stale; add a STALE banner to the BENCHGRAPH.md structural section (prose kept for design rationale, dead embeds removed). 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.
Implements a fast, sound structural pre-check for unrealizability that runs before the main synthesis pipeline. This catches trivially unrealizable specs where the controller has no influence over a boolean guarantee.
Summary
Adds
precheck_trivially_unreal(), a TRUST_OVER (over-approximation) pre-check that proves unrealizability by analyzing the propositional safety fragment of the expanded cover. It uses BDDs to test whether the environment has a winning one-step strategy: an input assignment that satisfies all boolean assumptions while making all boolean guarantees false.Key Changes
New module
src/precheck_unreal.c/include/tlsf/precheck_unreal.h: Implements the boolean-fragment UNREALIZABLE pre-check using OxiDD BDDs. The check:G(boolean)patterns)EnvWin = ¬∃outputs. ¬(A ∧ ¬G)where A is the assumption conjunction and G is the guarantee conjunctionIntegration into
src/main_tlsfcompose.c: Calls the pre-check immediately after cover expansion, before the expensive recognize/certify/residual stages. Matches ltlsynt's fast-path behavior for input-only guarantees.Test cases: Four new TLSF specs validating the pre-check:
precheck_input_only.tlsf: Input-only guarantee (must fire)precheck_outputs_rescue.tlsf: Output can satisfy guarantee (must not fire)precheck_assume_rescues.tlsf: Assumption forces input (must not fire, spec is REALIZABLE)precheck_temporal_assume_bail.tlsf: Temporal assumption present (must bail, downstream ltlsynt decides)Build integration: Added
src/precheck_unreal.cto thetlsfcomposetarget inmeson.buildDocumentation updates: Clarified benchmark scripts and README to reflect removal of syfco baseline comparisons; marked structural census plots as stale
Verdict Trust Model
The pre-check is an OVER-approximation that refutes a weakening of the spec:
Therefore: UNREALIZABLE verdict is sound and trustworthy; it never claims REALIZABLE.
https://claude.ai/code/session_01KvbjHkBHLYwxrFrvHae2xV