Codex/move compose residual research

.github/workflows/ci.yml

@@ -25,10 +25,9 @@ jobs:
           clang-format --dry-run --Werror src/*.c include/tlsf/*.h
 
   # Build the vendored OxiDD C FFI (Rust staticlib + cbindgen header) exactly
-  # once and share it with the OxiDD-enabled jobs as an artifact, so cargo runs
-  # a single time per CI run. The frontend-only jobs (build-test, build-clang,
-  # coverage, perf-regression) pass -Doxidd=disabled deliberately to keep
-  # proving the reduced no-Rust developer build path stays alive.
+  # once and share it with the explicit OxiDD research job as an artifact, so
+  # cargo runs a single time per CI run. The stable jobs stay on the default
+  # no-Rust production path.
   oxidd:
     runs-on: ubuntu-24.04
     steps:
@@ -142,7 +141,7 @@ jobs:
 
   # OxiDD-enabled build: links the shared FFI artifact, compiles the in-process
   # safety + GR(1) solvers (src/safety_oxidd.c, src/gr1_oxidd.c, src/aiger.c via
-  # tlsfcompose/tlsfsolve) and runs the full suite. The Spot-verified
+  # tlsfcompose/tlsfsolve) and runs the full research suite. The Spot-verified
   # verify_aiger_oxidd* tests auto-gate on Spot (absent here) and run locally;
   # bounded_synthesis_harness still exercises a real in-process solve.
   build-oxidd:
@@ -166,7 +165,7 @@ jobs:
         run: |
           # GitHub x86 runners are Haswell+ (AVX2-safe); exercises the
           # compile-time SIMD path in include/tlsf/simd.h.
-          meson setup build-oxidd -Doxidd=enabled -Dcpu=avx2
+          meson setup build-oxidd -Doxidd=enabled -Dresearch_tools=true -Dcpu=avx2
           ninja -C build-oxidd
           meson test -C build-oxidd --print-errorlogs
 

.github/workflows/release.yml

@@ -23,8 +23,6 @@ jobs:
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v5
-        with:
-          submodules: recursive
 
       - name: Verify runner platform
         run: |
@@ -48,34 +46,21 @@ jobs:
             echo "$(brew --prefix bison)/bin" >> "$GITHUB_PATH"
           fi
 
-      - name: Install Rust and cbindgen
-        run: |
-          rustup toolchain install stable --profile minimal
-          rustup default stable
-          command -v cbindgen >/dev/null || cargo install cbindgen --locked --force
-
-      - name: Build OxiDD FFI
-        run: scripts/build_oxidd.sh
-
-      - name: Configure and build all tools
+      - name: Configure and build stable tools
         run: |
           meson setup build-release \
-            -Doxidd=enabled \
-            -Dresearch_tools=true \
+            -Doxidd=disabled \
+            -Dresearch_tools=false \
             -Dcpu=${{ matrix.cpu }} \
             --buildtype=release
           ninja -C build-release
 
-      - name: Smoke test release binaries
+      - name: Smoke test stable release binaries
         run: |
           ./build-release/tlsf2ltl --version
           ./build-release/tlsf2tlsf --version
           ./build-release/tlsfinfo --version
           ./build-release/tlsfnorm --version
-          ./build-release/tlsfresidual --version
-          ./build-release/tlsfcompose --version
-          ./build-release/tlsfsolve --help
-          ./build-release/tlsfsolve test/cases/solve_real.aag >/tmp/strategy.aag
 
       - name: Package archive
         run: |
@@ -89,7 +74,7 @@ jobs:
           stage="dist/${archive}"
           mkdir -p "$stage"
 
-          tools="tlsf2ltl tlsf2tlsf tlsfinfo tlsfnorm tlsfresidual tlsfcompose tlsfsolve tlsftemplates tlsfbenchgraph"
+          tools="tlsf2ltl tlsf2tlsf tlsfinfo tlsfnorm"
           for tool in $tools; do
             cp "build-release/${tool}" "$stage/"
           done
@@ -98,8 +83,8 @@ jobs:
             printf 'version=%s\n' "$version"
             printf 'commit=%s\n' "$GITHUB_SHA"
             printf 'platform=%s\n' "${{ matrix.platform }}"
-            printf 'oxidd=enabled\n'
-            printf 'research_tools=true\n'
+            printf 'oxidd=disabled\n'
+            printf 'research_tools=false\n'
             printf 'cpu=%s\n' "${{ matrix.cpu }}"
           } > "$stage/BUILD_INFO.txt"
 

BENCHGRAPH.md

@@ -40,3 +40,32 @@ Head-to-head synthesis: standalone **acacia-bonsai** vs the **preprocessor** (`-
 
 ![Survival: acacia-bonsai vs preprocessor + acacia-bonsai](docs/benchgraph/survival.png)
 <!-- BENCHGRAPH:PREPROCESSOR END -->
+
+## Diagnosis
+
+The current preprocessor is slower than standalone acacia-bonsai overall.  The
+main cause is not a verdict-soundness problem: among the 1262 specs where both
+engines produced a definitive verdict, there were **0 verdict disagreements**.
+
+The dominant performance issue is that the residual sent to acacia is usually
+not meaningfully smaller than the original problem.  In this run, **2062/2545**
+specs left exactly one external residual cluster, and external residuals had a
+median residual/full node ratio of **1.0**.  That means the preprocessor often
+pays decomposition, routing, and merge overhead and then still asks acacia to
+solve essentially the same formula.
+
+Coverage is the second issue.  Only **454/2545** specs finished without an
+external residual solver, and most unsupported residuals are still liveness
+heavy, especially `liveness: nested_unsupported`.  More useful template/OxiDD
+coverage would matter most when it shrinks or eliminates these residuals, not
+when it only recognizes easy fragments that acacia already solves quickly.
+
+The local routes also need to be cost-aware.  Some fully-local OxiDD cases are
+much slower than standalone acacia on the original spec; for example large
+`shift_pb_*` instances create many local OxiDD clusters and lose by orders of
+magnitude.  Fully-local solving is therefore not automatically a speed win.
+
+The practical conclusion is: prioritize residual reduction and valuable
+fragment coverage first, add routing cutoffs for expensive low-value local
+plans second, and treat wrapper micro-optimization as secondary until the
+external residual is usually smaller than the original problem.

README.md

@@ -4,18 +4,19 @@ Small, fast, Unix-style command-line tools for working with
 [TLSF](https://github.com/reactive-systems/syfco) (Temporal Logic Synthesis
 Format) specifications, sharing a common C library.
 
-The normal release build uses OxiDD (<https://github.com/OxiDD/oxidd>) as the
-in-process BDD backend for safety and GR(1) games. 
-[ltlsynt](https://spot.lre.epita.fr/ltlsynt.html) is mentioned below, but it is
-not a library dependency of this project; it is an optional executable used by
-`scripts/solve.sh` and by the Docker wrapper image.
+The default production build is OxiDD-free and packages only the stable TLSF
+preprocessing tools. OxiDD (<https://github.com/OxiDD/oxidd>) is an explicit
+research-build dependency for the in-process safety/GR(1) solver tools.
+[ltlsynt](https://spot.lre.epita.fr/ltlsynt.html) and acacia-bonsai are
+optional executables used by `scripts/solve.sh` and by wrapper/benchmark flows.
 
 The tools fully expand parameterised TLSF (parameters, definitions including
 recursive case definitions, bus unrolling, bounded `&&[..]`/`||[..]`, indexed
 `X[n]` and bounded `G[i:j]`/`F[i:j]`, `enum` types, `SIZEOF`) and emit a ground
-TLSF spec or equivalent LTL. The synthesis layer adds structure-aware
+TLSF spec or equivalent LTL. The optional research synthesis layer adds structure-aware
 decomposition, certified local controllers, exact OxiDD-backed safety/GR(1)
-routes, and an external residual-solving wrapper for `ltlsynt`.
+routes, and an external residual-solving wrapper for `ltlsynt` or
+acacia-bonsai.
 
 ## Status
 
@@ -27,19 +28,19 @@ routes, and an external residual-solving wrapper for `ltlsynt`.
 | `tlsf2tlsf` | Emit expanded/basic TLSF. |
 | `tlsfinfo` | Inspect metadata, signals, and GR level. |
 | `tlsfnorm` | Normalize/split/simplify TLSF before synthesis. |
-| `tlsfresidual` | Emit residual clusters after sound decomposition. |
-| `tlsfcompose` | Build a decomposed synthesis plan; merge AIGER strategy files. |
-| `tlsfsolve` | Solve [AbsSynthe](https://github.com/gaperez64/AbsSynthe)-style AIGER safety/GR(1) games with OxiDD. |
 
 ### Research and diagnostic tools
 
-Built with `-Dresearch_tools=true`; included in release archives for
-reproducibility, but not part of the stable preprocessing API.
+Built with `-Dresearch_tools=true`; not included in stable release archives and
+not part of the stable preprocessing API.
 
 | Tool | Purpose |
 |---|---|
 | `tlsftemplates` | Inspect template certificates and CSNF output. |
 | `tlsfbenchgraph` | Generate corpus-level benchmark/shape reports. |
+| `tlsfresidual` | Emit residual clusters after sound decomposition. |
+| `tlsfcompose` | Build a decomposed synthesis plan; merge AIGER strategy files. |
+| `tlsfsolve` | Solve [AbsSynthe](https://github.com/gaperez64/AbsSynthe)-style AIGER safety/GR(1) games with OxiDD. |
 
 The preprocessor uses equivalence-preserving normalization followed by exact
 syntactic recognizers and conservative certification. It does not use graph
@@ -56,26 +57,18 @@ ground AST ──► tlsfnorm      (normalized TLSF)
 ## Building
 
 Requires a C23 compiler, [meson](https://mesonbuild.com/),
-[ninja](https://ninja-build.org/), `flex`, `bison`, Rust/cargo, and
-`cbindgen` for release-quality OxiDD-enabled builds.
+[ninja](https://ninja-build.org/), `flex`, and `bison`. OxiDD-enabled research
+builds also require Rust/cargo and `cbindgen`.
 
-Release-quality build:
+Release-quality stable build:
 
 ```sh
-git submodule update --init --recursive
-scripts/build_oxidd.sh
-meson setup build -Doxidd=enabled --buildtype=release
+meson setup build --buildtype=release
 ninja -C build
 ```
 
-Reduced developer/frontend-only build:
-
-```sh
-meson setup build-min -Doxidd=disabled
-ninja -C build-min
-```
-
-Research/diagnostic tools:
+Research/diagnostic tools, including `tlsfresidual`, `tlsfcompose`, and
+`tlsfsolve`:
 
 ```sh
 git submodule update --init --recursive
@@ -106,7 +99,7 @@ tlsfinfo  --input-signals|--output-signals spec.tlsf    # declared (bus notation
 tlsfinfo  --expanded-ins|--expanded-outs   spec.tlsf    # scalar CSV for ltlsynt --ins/--outs
 tlsfinfo  --generalized-reactivity spec.tlsf   # GR(k) level, or "NOT in GR"
 
-# structure / templates
+# research / diagnostics
 tlsftemplates --certify --solve --format csnf spec.tlsf   # certified controllers
 tlsfbenchgraph --input-dir specs/ --split --summary       # corpus shape census
 
@@ -121,7 +114,9 @@ tlsfresidual --split --lowercase spec.tlsf                # lowercase formulas +
 tlsfcompose --split --output-dir out/ spec.tlsf           # controllers.aag + clusters + exact OxiDD solves
 tlsfcompose --split --realizability spec.tlsf             # fast REAL/UNREAL/UNKNOWN oracle
 tlsfcompose --merge out/controllers.aag out/cluster.*.aag # recombine external strategies
-scripts/solve.sh --solver ltlsynt --output ctrl.aag spec.tlsf  # external-solver flow
+scripts/solve.sh --solver ltlsynt --output ctrl.aag spec.tlsf  # ltlsynt backend
+scripts/solve.sh --backend acacia --solver acacia-bonsai \
+        --output ctrl.aag spec.tlsf                            # acacia backend
 tlsfsolve game.aag > strategy.aag                         # solve an AIGER safety/GR(1) game
 ```
 
@@ -193,9 +188,9 @@ scripts/solve.sh --solver ltlsynt --output ctrl.aag spec.tlsf
 
 For the `ltlsynt` backend the script passes `--lowercase` so the emitted
 cluster formulas, `c ins=`, `c outs=`, and AIGER symbols agree. The `acacia`
-backend block is explicit in the script and is the intended swap-in point for
-an acacia-bonsai invocation. Pre-solved and external strategies are recombined
-with `tlsfcompose --merge`.
+backend uses the same lowercase convention and calls acacia-bonsai with
+`-F/-i/-o/-s`. Pre-solved and external strategies are recombined with
+`tlsfcompose --merge`.
 
 ### 2 · One merged controller circuit (AIGER)
 
@@ -252,11 +247,11 @@ without running a solver.
 ```sh
 # full corpus speed + complexity (rerunnable; --from-data re-renders the report)
 scripts/benchgraph.py --corpus benchmarks/tlsf \
-        --tlsfcompose build-oxidd/tlsfcompose \
+        --tlsfcompose build-research/tlsfcompose \
         --solver ../acacia-bonsai/build_best_decomp_mona/src/acacia-bonsai
 
 # route-only corpus census; writes rows incrementally and skips slow specs
-scripts/collect_route_stats.py --compose build-oxidd/tlsfcompose \
+scripts/collect_route_stats.py --compose build-research/tlsfcompose \
         --timeout 5 --out route_stats.tsv benchmarks/tlsf
 ```
 
@@ -305,8 +300,10 @@ and REAL is never claimed. The REAL pre-check is **TRUST_UNDER**: it proves a
 strengthening, so REAL is trusted and UNREAL is never claimed. If neither fires,
 the command exits `2` with `UNKNOWN`.
 
-Corpus shape distributions and the templates+OxiDD solve-rate / speed numbers
-live in [`BENCHGRAPH.md`](BENCHGRAPH.md); exact recognizers plus conservative
+Route and shape diagnostics come from `tlsfbenchgraph`,
+`scripts/collect_route_stats.py`, and the per-run TSVs.  The maintained
+head-to-head wrapper numbers and benchmark diagnosis live in
+[`BENCHGRAPH.md`](BENCHGRAPH.md). Exact recognizers plus conservative
 certification are the proof — there is no approximate matching in the synthesis
 path.
 
@@ -347,7 +344,7 @@ every result is `ltlfilt --equivalent-to` the input.
 
 ```sh
 meson test -C build                                  # fast golden-output suite
-meson setup build-cov -Doxidd=disabled -Db_coverage=true && meson test -C build-cov
+meson setup build-cov -Dresearch_tools=true -Doxidd=disabled -Db_coverage=true && meson test -C build-cov
 clang-format -i src/*.c include/tlsf/*.h             # style (LLVM, 2-space, 80col)
 clang-tidy -p build src/*.c                          # lint
 bench/bench.sh [--baseline|--check]                  # wall/RSS perf-regression guard