Acacia-Bonsai

This is a modern implementation of universal co-Buchi reactive synthesis algorithms using antichain data structures. The theory and practice is described in:

https://arxiv.org/abs/2204.06079

Docker images

Two images are published on the GitHub Container Registry. Boomslang bundles Spot's Python bindings, acacia_boomslang, and Jupyter:

docker pull ghcr.io/gaperez64/acacia-boomslang:latest
docker run --rm -p 8888:8888 ghcr.io/gaperez64/acacia-boomslang:latest

The CLI image contains the dependencies and sources. It compiles inside the container so -march=native can target the host:

docker pull ghcr.io/gaperez64/acacia-bonsai:latest
docker run --name acacia -it ghcr.io/gaperez64/acacia-bonsai:latest
./scripts/compile.sh
./scripts/acacia-bonsai.sh best_decomp_rank_bucketed_mona \
  -f 'G F req -> G F grant' -i req -o grant
cat examples/realizable.tlsf | \
  ./scripts/acacia-bonsai.sh best_decomp_rank_bucketed_mona --tlsf
cat examples/realizable.tlsf | \
  ./scripts/acacia-synthesis.sh best_decomp_rank_bucketed_mona --tlsf > controller.aag

The CLI example intentionally omits --rm: compilation happens inside the named container, so removing it on exit would discard the binaries. Re-enter it with docker start -ai acacia. Run the wrapper without arguments to list the configurations it accepts.

Dependencies

This program depends on:

• A modern C++ compiler (C++23 is used)
• The Meson Build System
• The Downset Manipulation Library
• The Spot Library: You will need to compile and install spot separately. The downset manipulation library requires compilation with g++ so to link against spot you need to compile it with g++ too (set CXX before configuring, compiling, and installing).
• The Z shell, for some scripts.

Initialize the vendored Posets and TLSF-tools dependencies after cloning:

git submodule update --init

This is deliberately non-recursive; Acacia disables TLSF-tools' optional OxiDD backend.

Some of the tests also depend on:

• Valgrind

Installing dependencies on macOS

Note that on macOS the compilation has to happen via GCC. GCC can be installed using Homebrew: brew install gcc. Once installed, meson needs to be told to use GCC instead of built-in Clang. This can be done using the meson-native file, or by setting the CXX and CC environment variables. For instance, do export CXX=$(brew --prefix)/bin/g++-XX before starting with meson.

Spot has to be manually compiled using GCC and installed. After compiling it and installing it, you still need to ensure that meson can find Spot using pkgconfig. This can be done, for example, by setting the pkg_config_path in a meson-native file or by issuing export PKG_CONFIG_PATH=/usr/local/lib/pkgconfig before starting with meson (this works if you installed spot in the default location).

Compiling, running, benchmarking

To compile and run, use Meson:

meson setup build
cd build
meson compile
src/acacia-bonsai -h
  [...]
src/acacia-bonsai -f '((G (F (req))) -> (G (F (grant))))' -i req -o grant
REALIZABLE

This produces a debug build. Build an optimized registered preset with:

./self-benchmark.sh -c best_decomp_mona -R

The -c option selects a configuration and the -R option disables the benchmarking step, so that only setup and compilation are done. If compilation memory is tight, add -L to use the low-memory compile profile.

The Meson option acacia_enable_tlsf_frontend is off by default, so a bare meson setup build does not require Flex and Bison. Every configuration preset enables the frontend, so any self-benchmark.sh -c NAME build includes it:

./self-benchmark.sh -L -R -c best_decomp_mona
build_best_decomp_mona/src/acacia-bonsai -T spec.tlsf

-T/--tlsf FILE parses TLSF natively. The wrapper accepts TLSF on standard input with --tlsf through the linked frontend; no external TLSF converter or metadata binary is used at runtime. Moore-target controller conversion is likewise performed inside Acacia.

Correctness and performance gates, including the sequential measurement protocol, are documented in benchmarking/README.md. The current comparison with ltlsynt, residual gap analysis, and durable experiment record are in benchmarking/LTLSYNT-GAP.md.

Compile-time configurations

The experimental Spot paths require -Dacacia_spot_guarded_backend=true; the TAA providers also require -Dacacia_spot_lazy_provider=true. --arms real:small:spot-guarded:spot-lazy,unreal:formula:spot-guarded:spot-lazy selects a lazy worker for each polarity. spot-eager is the fully enumerated control of the same TAA/cursor construction. With the default frozen-graph provider, spot-guarded uses dense ranks and spot-guarded-sparse preserves the same mixed numeric/Boolean domain in sparse storage. Automaton-unreal requires frozen-graph.

These paths verify decisions before returning them. Candidate limits produce an inconclusive result; --candidate-mode fallback explicitly rebuilds the existing frozen/backward path after a candidate failure. Synthesis uses the existing frozen/backward implementation. For diagnostic runs, ACACIA_SPOT_CAPTURE_DIR enables JSON records of the actual transformed worker formulas, AP partitions, phases, and measured counters.

-Dacacia_default_candidate_mode=only|fallback sets the build's default; --candidate-mode still overrides it. Both TAA providers use -Dacacia_spot_taa_max_rank_nodes=200000 by default, independently of frozen guarded search. The common ACACIA_SPOT_MAX_RANK_NODES environment override applies to both; ACACIA_SPOT_TAA_MAX_RANK_NODES takes precedence for TAA only. The experimental otf_taa_fallback_lazy and otf_taa_fallback_eager presets use a 1,000-node TAA cap and backward fallback, alongside forward real and both original forward unreal workers. They remain outside the shipping group. The otf_mix_formula_lazy and otf_mix_formula_eager presets instead use sparse guarded formula-unreal solving alongside forward automaton-unreal, forward real, and bounded TAA real with backward fallback. Their 1,000-node TAA cap leaves frozen guarded search's 200,000-node budget unchanged. These four-worker mixtures are experimental configurations under evaluation. The node cap is not a deadline: TAA construction or a row/query operation can exhaust the external timeout before backward fallback starts. The mixed TAA presets currently fail the panel coverage gate on some fast backward-real cases.

Acacia-Bonsai's optimized variants are compile-time configurations. The configuration registry lives in config/acacia-options.json and config/acacia-presets.json; scripts/acacia-config.py validates presets and translates them to Meson options.

Inspect and validate the registry with:

python3 scripts/acacia-config.py validate
python3 scripts/acacia-config.py list-presets
python3 scripts/acacia-config.py list-presets --long
python3 scripts/acacia-config.py show best_decomp_mona
python3 scripts/acacia-config.py show best_decomp_mona --describe
python3 scripts/acacia-config.py meson-args best_decomp_mona

meson.build writes these choices into acacia_build_config.hh. The Spot translator preference is registry-backed as acacia_translation_pref; the default is small. The values any and small+any are available for ablation and racing presets such as best_decomp_mona_any and best_decomp_mona_race.

The configurations we ship are whichever ones the docker_default group names:

python3 scripts/acacia-config.py list-group docker_default

That group is the pointer, and it is repointed when the measurements say so -- the Docker image, the TLSF examples above and CI all read it rather than naming a preset. A preset name is a historical label, not a claim about which configuration is currently best. The best in existing names was accurate when those presets were chosen and silently stopped being so; that is why the group is the pointer and the name is not. scripts/acacia-config.py list-presets --long lists each preset's role and purpose. scripts/acacia-config.py show <preset> reports its complete resolved options; add --describe to include role and description as siblings of the options object. Plain show remains the build staleness fingerprint, and plain list-presets prints only names for scripts. best_decomp_mona is the plain vector-backed downset configuration, kept as the reference point for downset comparisons.

All four shipped configurations enable the exact equivariant solver. It automatically declines to the classic solver when no verified profitable symmetry is available, or when fewer than acacia_equivariant_min_blocks client-state blocks are found (default 2). Use best_decomp_rank_bucketed_mona_noequivariant for the explicit classic-only escape hatch and performance ablation. New presets should inherit from the nearest existing configuration and override only the values being tested. Each preset declares a one-line description and a role: shipping exactly for docker_default members, reference for measurement controls, sweep for comparison arms, diagnostic for instrumented builds, or legacy for historical configurations. Metadata does not affect resolved options or configuration hashes. New names are limited to 40 characters and cannot contain the token best; all existing names are grandfathered and remain unchanged. The registry's currently empty aliases map can map an old name directly to a current preset after a future rename; lookup reports the alias on stderr and resolves to the current preset's options and hash.

Documentation

This project comes with a doxygen configuration file. Execute the following command to generate documentation:

doxygen Doxyfile

Citing

If you use this tool for your academic work, please make sure to cite the paper we wrote about it.

@inproceedings{DBLP:conf/tacas/CadilhacP23,
  author       = {Micha{\"{e}}l Cadilhac and
                  Guillermo A. P{\'{e}}rez},
  editor       = {Sriram Sankaranarayanan and
                  Natasha Sharygina},
  title        = {Acacia-Bonsai: {A} Modern Implementation of Downset-Based {LTL} Realizability},
  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems
                  - 29th International Conference, {TACAS} 2023, Held as Part of the
                  European Joint Conferences on Theory and Practice of Software, {ETAPS}
                  2022, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
  series       = {Lecture Notes in Computer Science},
  volume       = {13994},
  pages        = {192--207},
  publisher    = {Springer},
  year         = {2023},
  url          = {https://doi.org/10.1007/978-3-031-30820-8\_14},
  doi          = {10.1007/978-3-031-30820-8\_14},
  timestamp    = {Sat, 29 Apr 2023 19:25:03 +0200},
  biburl       = {https://dblp.org/rec/conf/tacas/CadilhacP23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}