Small, fast, Unix-style command-line tools for working with TLSF (Temporal Logic Synthesis Format) specifications, sharing a common C library.
The tools fully expand parameterised TLSF (parameters, definitions including
recursive case definitions, sets and reductions, structural pattern guards,
bus unrolling, bounded temporal operators, enum types, and SIZEOF) and emit
a ground 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 or acacia-bonsai.
| Tool | Purpose |
|---|---|
tlsf2ltl |
Convert expanded TLSF to LTL. |
tlsf2tlsf |
Emit expanded/basic TLSF. |
tlsfinfo |
Inspect metadata, signals, and GR level. |
tlsfnorm |
Normalize/split/simplify TLSF before synthesis. |
mealy2moore |
Delay AIGER strategy outputs for Moore-target specs. |
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-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 similarity or approximate matching in the synthesis path.
flowchart LR
tlsf["TLSF file"] -->|"parse<br/>flex + bison"| raw["Raw AST"]
raw -->|"expand<br/>parameters, definitions, sets, buses, reductions"| ground["Ground AST"]
ground --> basic["tlsf2tlsf<br/>basic TLSF"]
ground --> ltl["tlsf2ltl<br/>LTL"]
ground --> norm["tlsfnorm<br/>normalized TLSF"]
ground --> residual["tlsfresidual<br/>residual clusters"]
ground --> compose["tlsfcompose<br/>clusters + controllers.aag → plan"]
Requires a C23 compiler, meson,
ninja, flex, and bison. OxiDD-enabled research
builds also require Rust/cargo and cbindgen.
Release-quality stable build:
meson setup build --buildtype=release
ninja -C buildResearch/diagnostic tools, including tlsfresidual, tlsfcompose, and
tlsfsolve:
git submodule update --init --recursive
scripts/build_oxidd.sh
meson setup build-research -Doxidd=enabled -Dresearch_tools=true --buildtype=release
ninja -C build-researchSanitizers are available for development builds with
-Dsanitize=address,undefined.
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 and acacia-bonsai are
optional executables used by scripts/solve.sh and by wrapper/benchmark flows.
Each tool reads a FILE argument or stdin, writes to stdout or --output FILE,
and accepts --version/--help. Options are long (--) only.
# convert
tlsf2ltl spec.tlsf # spec's LTL (ltlxba, minimal parens)
tlsf2ltl --format ltl|latex spec.tlsf # plain LTL / LaTeX math
tlsf2ltl --strong-simplify spec.tlsf # NNF + push/pull simplification, etc.
tlsf2ltl --safety | --liveness spec.tlsf # syntactic split of the formula
tlsf2ltl --fair-environment spec.tlsf # assume every input toggles forever
tlsf2tlsf --fair-environment spec.tlsf # add scalar/quantified fairness
tlsf2tlsf --basic spec.tlsf # fully expanded basic TLSF
mealy2moore strategy.aag > strategy.moore.aag # delay Mealy outputs one step
# inspect
tlsfinfo spec.tlsf # all metadata (--semantics, --title, …)
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"
# research / diagnostics
tlsftemplates --certify --solve --format csnf spec.tlsf # certified controllers
tlsfbenchgraph --input-dir specs/ --split --summary # corpus shape census
tlsfbenchgraph --source-features spec.tlsf # leakage-free selector row
scripts/automata_study.py --file-list panel.list --output run/ \
--tlsfnorm build/tlsfnorm --tlsf2ltl build/tlsf2ltl \
--tlsfinfo build/tlsfinfo --tlsfbenchgraph build/tlsfbenchgraph \
--automata-generator ../acacia-bonsai/build/src/acacia-automata-study
scripts/evaluate_automata_study.py --bundle run/ --output results/ \
--acacia-replay ../acacia-bonsai/build/src/acacia-hoa-replay
# normalize / decompose / synthesize
tlsfnorm --passes split,nnf,boolean spec.tlsf # re-emit normalized TLSF
tlsfnorm --pre-passes pre-safe --passes match-safe:1 spec.tlsf # exact-recognition normalization
tlsfnorm --passes route-safe:1 spec.tlsf # routing normalization
tlsfnorm --passes sickert-stage2:1 --norm-max-growth 300 spec.tlsf # experimental, infinite-word-only
tlsfnorm --norm-stats --passes match-safe:1 spec.tlsf # per-rule normalization stats
tlsfresidual --split --output-dir out/ spec.tlsf # one residual.k.ltl per cluster
tlsfresidual --split --lowercase spec.tlsf # lowercase formulas + interfaces
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 # 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) gametlsfbenchgraph --source-features emits a versioned TSV selector schema
(--schema-version). Columns prefixed guard_ are derived only from the
expanded source TLSF AST: operator occurrences and maximum syntax/temporal
depth. The mode rejects splitting and normalization options and excludes
automata, recognizer results, and solver outcomes. Only these fields plus the
declared interface sizes are supported for offline routing experiments.
tlsfsolve reads an AbsSynthe-style AIGER game: uncontrollable inputs are
ordinary inputs, controllable inputs are prefixed controllable_, safety games
use a bad output, and GR(1) games may use AIGER 1.9 justice/fairness
records. Exit status 0 means realizable and writes the strategy AAG to stdout;
status 1 means proven unrealizable and writes UNREALIZABLE to stderr; status
2 reports an input, usage, or internal OxiDD solver failure.
The installed library exposes decomposition/preprocessing without AIGER structs or internal AST layouts:
- C header:
#include <tlsf/decompose.h> - C++ wrapper:
#include <tlsf/decompose.hpp> - opaque AST:
#include <tlsf/ast_api.h> - typed C++ visitor:
#include <tlsf/ast_api.hpp> - Meson:
dependency('tlsf') - pkg-config:
pkg-config --cflags --libs tlsf
tlsf_decompose_string() / tlsf_decompose_file() return duplicated strings:
preprocessed LTL, global inputs/outputs, residual clusters
{ltl, inputs, outputs}, semantics/target, GR level, a fast pre-check verdict,
and trust tags. Free the C result with tlsf_decompose_result_free(). The C++
wrapper returns std::string / std::vector values and frees the C handle via
RAII.
TlsfAst retains the expanded specification, residual plan, cluster roots,
and the same TlsfDecomposeResult metadata under one lifetime. Consumers can
walk the opaque 16-kind post-expansion tree manually or use
tlsf_ast_accept()'s children-first callback table. The header-only C++ API
provides tlsf::ast::Ast, non-owning Tree values, and an ANTLR-style
Visitor<T> whose methods build any consumer-defined result type.
#include <tlsf/decompose.hpp>
#include <tlsf/ast_api.hpp>
tlsf::Options opt;
opt.split = true;
tlsf::Result r = tlsf::decompose(spec_text, opt);
for (const tlsf::Cluster &c : r.clusters) {
// c.ltl, c.inputs, c.outputs
}
tlsf::ast::Ast ast(spec_text, opt);
MyFormulaBuilder builder; // derives from tlsf::ast::Visitor<MyFormula>
MyFormula formula = builder.visit(ast.root());
for (tlsf::ast::Tree cluster : ast.clusters()) {
MyFormula residual = builder.visit(cluster);
}No Aig, OxiDD, internal Node, cover, CSNF, or arena type crosses this API.
The visitor-based ast_api Spot example builds each
tree directly as a spot::formula and checks it against the string API.
Configure a local /usr/local Spot installation with
meson setup build -Dpkg_config_path=/usr/local/lib/pkgconfig.
Decompose first: certify the combinational controllers and hand only the
residual to a backend. Each cluster.k.ltl carries its own interface in
header comments (c ins=…, c outs=…), and disjoint-output clusters are
independent — several small ltlsynt/strix calls instead of one giant one.
mkdir out && tlsfcompose --split --output-dir out/ spec.tlsf
sh out/compose.sh # ltlsynt per cluster -> verdict
# or drive a backend yourself, per cluster (strip the 'c ' header lines to a
# file and read it with -F; a large cluster overflows ltlsynt's --formula= arg):
grep -v '^c ' out/cluster.0.ltl > out/cluster.0.f
ltlsynt --ins=… --outs=… -F out/cluster.0.f--output-dir also writes controllers.aag, a mergeable AIGER strategy for
the certified part. Trusted OxiDD-eligible residual outcomes are handled in
process with one persistent BDD session: exact routes and strengthened/UNDER
routes can emit cluster.k.aag, while weakened/OVER routes can stop early on
trusted UNREAL. The remaining clusters stay as cluster.k.ltl.
scripts/solve.sh automates the full flow:
scripts/solve.sh --solver ltlsynt --output ctrl.aag spec.tlsfFor the ltlsynt backend the script passes --lowercase so the emitted
cluster formulas, c ins=, c outs=, and AIGER symbols agree. The acacia
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.
The supported controller flow is file-based: decompose, solve every emitted cluster with the backend of your choice, then merge those AIGER strategies with the certified part.
scripts/solve.sh --solver ltlsynt --output ctrl.aag spec.tlsf
# verify it against the spec (Spot):
python3 scripts/verify_aiger_ltl.py --aiger ctrl.aag \
--tlsf2ltl build/tlsf2ltl --tlsf spec.tlsftlsfnorm re-emits clean TLSF (split conjunctions, NNF, boolean simplify);
tlsf2ltl gives the formula and tlsfinfo --expanded-ins/--expanded-outs the
scalar interface, so any Spot/Strix-style tool can take over. The ltlxba
dialect follows the historical SyFCo/classic-ltl2ba convention of lowercasing
atoms, so lowercase the interface to match; the faithful ltl dialect keeps
the original case. Spot accepts uppercase TLSF identifiers. tlsfcompose and
tlsfresidual keep original case by default and apply lowercasing to formulas
and interfaces only with --lowercase; all lowercase exports reject collisions.
tlsfnorm --passes split,nnf,boolean spec.tlsf > spec.norm.tlsf
lc() { tr 'A-Z' 'a-z'; } # ltlxba lowercases atoms
ins=$(tlsfinfo --expanded-ins spec.norm.tlsf | lc) # scalar CSV, buses unrolled
outs=$(tlsfinfo --expanded-outs spec.norm.tlsf | lc)
tlsf2ltl spec.norm.tlsf > spec.norm.ltl # read via -F (a big
ltlsynt --ins="$ins" --outs="$outs" -F spec.norm.ltl # formula overflows -f)Census the structural shapes across a corpus.
# per-spec shape/template metrics + an aggregate distribution (mutex/response/…)
tlsfbenchgraph --input-dir benchmarks/tlsf --split --summary > shapes.tsv
# look at one spec's certified templates (response / mutex / arbiter / …)
tlsftemplates --certify --solve --format csnf spec.tlsfHow much does decomposition change the residual shape, and how does the wrapper
pipeline compare with acacia-bonsai alone? scripts/benchgraph.py writes the
BENCHGRAPH.md head-to-head section (solved counts, net gain,
and a survival plot). scripts/collect_route_stats.py records route diagnostics
without running a solver.
# full corpus speed + complexity (rerunnable; --from-data re-renders the report)
scripts/benchgraph.py --corpus benchmarks/tlsf \
--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-research/tlsfcompose \
--timeout 5 --out route_stats.tsv benchmarks/tlsfThe preprocessor works on TLSF structure — the expanded constraint cover,
before flattening to one LTL formula: each section formula keeps its role, side,
invariant wrapping, syntactic safety/liveness class, and signal support. Over it,
exact syntactic template candidates are recognized (response G(r→F g),
mutex, recurrence G F x, persistence F G x, reaction, definition,
guarded-next, arbiter, …). --split first decomposes each constraint into its
top-level && conjuncts (distributing G/X along the spine,
equivalence-preserving), which is what makes most templates visible. Optional
equivalence-preserving normalization (tlsfnorm or --match-normalize) can
expose more of these exact shapes before
recognition without changing the spec's meaning.
tlsftemplates promotes candidates to a Certified Strategy Normal Form
(CSNF) along the ladder candidate → checked → certified → solved: a block is
solved only behind a sound, conservative side condition (usually free-output:
the target output occurs in no other constraint). Certified families cover the
combinational/finite slice — decoders (o:=θ), set/reset/toggle/delay registers,
reaction logic, and liveness schedulers (response/round-robin/arbiter). Stateful
safety games and GR(1)-style reactivity need a real solver, not a syntactic
certificate, and stay candidate.
tlsfresidual then substitutes the solved combinational outputs away and emits
the residual over a smaller alphabet, clustering it by shared output
(E → ⋀ᵢ Gᵢ ≡ ⋀ᵢ (E → Gᵢ) when output sets are disjoint) into independent,
parallelisable sub-problems. Reached assumptions are kept regardless of
safety/liveness class; pruning drops only assumptions over disjoint signals, so
the residual decomposition is labelled TRUST_EXACT. The emitted cluster
formula is the formula solved and trusted.
tlsfcompose turns that into a runnable plan: controllers.aag carries the
certified part; trusted OxiDD residual controllers may also appear as
cluster.k.aag; each cluster.k.ltl carries an exact residual formula plus
c ins=/c outs= comments; and --merge recombines AIGER strategy files. The
spec is realizable iff every cluster is, so the certified controllers ⊕ one
trusted controller per cluster realise the whole spec. The machine format
(csnf) is DIMACS-style line records (fgets/strtok, no JSON).
tlsfcompose --realizability is a fast verdict-only oracle. The always-on
UNREAL pre-check is TRUST_OVER: it refutes a weakening, so UNREAL is trusted
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.
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. Exact recognizers plus conservative
certification are the proof — there is no approximate matching in the synthesis
path.
The single LTL formula defined by the TLSF semantics:
INITIALLY → ( PRESET ∧ ( (G REQUIRE ∧ ASSUME) → (G ASSERT ∧ GUARANTEE) ) )
REQUIRE/ASSERT are wrapped in G; PRESET sits outside the
assumption→guarantee implication; empty sections drop out. The
shape then follows the (possibly overwritten) SEMANTICS/TARGET:
- Strict (
Strict,*) — the TLSF v1.1 section 3.2 formINITIALLY → (PRESET ∧ (ASSERT W ¬REQUIRE) ∧ (G REQUIRE ∧ ASSUME → GUARANTEE));--overwrite-semantics Mealyrelaxes it to the standard implication. - Finite-word (
Finite,*) — emitsltlxba-fin: strong-next printsX[!], andWplus any internally derived strong release are rewritten with LTLf-valid identities so spot'sltlfsyntaccepts them. - Mealy/Moore — from
SEMANTICS; aTARGETmismatch is converted (Moore→Mealy delays inputsi↦X i, Mealy→Moore delays outputso↦X o).
Output is minimally parenthesised by the spot/ltl2ba precedence
(! X F G > U R W > && > || > -> <->). --parenthesize fully
parenthesises; --format picks the spelling (ltlxba/ltl/latex).
Equivalence-preserving rewrites are exposed as flags
(--weak-simplify=-s0, --strong-simplify=-s1, --nnf,
--no-{weak-until,release,strong-release,finally,globally},
--{push,pull}-{globally,finally,next}-{in,out});
every result is ltlfilt --equivalent-to the input.
--fair-environment adds G F i and G F !i assumptions for every Boolean
environment input, requiring each input to visit both values infinitely often.
For input buses, normal tlsf2tlsf output keeps two inclusive quantified
assumptions over the declared bounds; tlsf2tlsf --basic and tlsf2ltl
expand them into one pair per bit. Existing assumptions are preserved, specs
without inputs are unchanged, and the option is rejected under effective
finite-word semantics (including semantics selected by an override). Generated
assumptions participate in the usual Mealy/Moore conversion, rewrites, and
safety/liveness output modes.
The
--safety/--livenesssplit is syntactic: after NNF, safety iff the tree has noF,U, or internally derived strong-release node. A safety property written with liveness operators is classified as liveness.
meson test -C build # fast golden-output suite
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 guardCI (.github/workflows/ci.yml) checks formatting, builds with gcc and clang,
runs the suite + a valgrind no-leak check, gates line coverage at 75 %, and runs
the bench.sh --check regression guard.
MIT.