LTLSYNT

ltlsynt - reactive synthesis from LTL specifications

ltlsynt [OPTION...]

Synthesize a controller from its LTL specification.

Input options:

--from-pgame=FILENAME

Read a parity game in Extended HOA format instead of building it.

-f, --formula=STRING

process the formula STRING

-F, --file=FILENAME[/COL]

process each line of FILENAME as a formula; if COL is a positive integer, assume a CSV file and read column COL; use a negative COL to drop the first line of the CSV file

--ins=PROPS

comma-separated list of uncontrollable (a.k.a. input) atomic propositions, interpreted as a regex if enclosed in slashes

--lbt-input

read all formulas using LBT’s prefix syntax

--lenient

parenthesized blocks that cannot be parsed as subformulas are considered as atomic properties

--outs=PROPS

comma-separated list of controllable (a.k.a. output) atomic propositions, , interpreted as a regex if enclosed in slashes

--part-file=FILENAME

read the I/O partition of atomic propositions from FILENAME

--tlsf=FILENAME

Read a TLSF specification from FILENAME, and call syfco to convert it into LTL

Fine tuning:

--algo=sd|ds|ps|lar|lar.old|acd

choose the algorithm for synthesis:

sd: translate to TGBA, split, determinize

ds: translate to TGBA, determinize, split ps: translate to DPA, split lar: translate to a deterministic TELA, convert

to DPA with LAR, split (default)

lar.old: old version of LAR, for benchmarking; acd: translate to a deterministic TELA, convert

to DPA with ACD, split

--bypass=yes|no

whether to try to avoid to construct a parity game (enabled by default)

--decompose=yes|no

whether to decompose the specification as multiple output-disjoint problems to solve independently (enabled by default)

--global-equivalence=yes|no|before-decompose

whether to remove atomic propositions that are always equivalent to another one (enabled by default, both before and after decomposition)

--polarity=yes|no|before-decompose

whether to remove atomic propositions that always have the same polarity in the formula to speed things up (enabled by default, both before and after decomposition)

--simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat

simplification to apply to the controller (no) nothing, (bisim) bisimulation-based reduction, (bwoa) bisimulation-based reduction with output assignment, (sat) SAT-based minimization, (bisim-sat) SAT after bisim, (bwoa-sat) SAT after bwoa. Defaults to ’bwoa’.

--splittype=expl|semisym|fullysym|auto

Selects the algorithm to use to transform the automaton into a game graph. Defaults to ’auto’.

Output options:

--aiger[=ite|isop|both[+ud][+dc][+sub0|sub1|sub2]]

encode the winning strategy as an AIG circuit and print it in AIGER format. The first word indicates the encoding to used: "ite" for If-Then-Else normal form; "isop" for irreducible sum of products; "both" tries both and keeps the smaller one. Other options further refine the encoding, see aiger::encode_bdd. Defaults to "ite".

--csv[=[>>]FILENAME], --csv-without-formula[=[>>]FILENAME]

output statistics as CSV in FILENAME or on standard output (if ’>>’ is used to request append mode, the header line is not output)

--csv-with-formula[=[>>]FILENAME]

like --csv, but with an additional ’fomula’ column

-d, --dot[=options]

Use dot format when printing the result (game, strategy, or AIG circuit, depending on other options). The options that may be passed to --dot depend on the nature of what is printed. For games and strategies, standard automata rendering options are supported (e.g., see ltl2tgba --dot). For AIG circuit, use (h) for horizontal and (v) for vertical layouts.

--hide-status

hide the REALIZABLE or UNREALIZABLE line (The exit status is enough of an indication.)

-H, --hoaf[=1.1|b|i|k|l|m|s|t|v]

Output the automaton in HOA format (default). Add letters to select (1.1) version 1.1 of the format, (b) create an alias basis if >=2 AP are used, (i) use implicit labels for complete deterministic automata, (s) prefer state-based acceptance when possible [default], (t) force transition-based acceptance, (m) mix state and transition-based acceptance, (k) use state labels when possible, (l) single-line output, (v) verbose properties

--print-game-hoa[=options]

print the parity game in the HOA format, do not solve it

--print-pg

print the parity game in the pgsolver format, do not solve it

-q, --quiet

suppress all normal output

--realizability

realizability only, do not compute a winning strategy

Miscellaneous options:

--verbose

verbose mode

--verify

verify the strategy or (if demanded) AIG against the formula

--version

print program version

-x, --extra-options=OPTS

fine-tuning options (see spot-x (7))

Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options.

Exit status:

If you would like to give a reference to this tool in an article, we suggest you cite the following papers:

Report bugs to <spot@lrde.epita.fr>.

Copyright © 2025 by the Spot authors, see the AUTHORS File for details. License GPLv3+: GNU GPL version 3 or later.
This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law.