FreeBSD Manual Pages
LTLSYNT(1) User Commands LTLSYNT(1) NAME ltlsynt - reactive synthesis from LTL specifications SYNOPSIS ltlsynt [OPTION...] DESCRIPTION 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[/VAR=VAL[,VAR=VAL...]] Read a TLSF specification from FILENAME, and call syfco to con- vert it into LTL. Any parameter assignment specified after a slash is passed as '-op VAR=VAL' to syfco. 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-dis- joint 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 decom- position) --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 reduc- tion with output assignment, (sat) SAT-based minimization, (bisim-sat) SAT after bisim, (bwoa-sat) SAT after bwoa. De- faults 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. De- faults 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 out- put) --csv-with-formula[=[>>]FILENAME] like --csv, but with an additional 'formula' 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 ba- sis if >=2 AP are used, (i) use implicit labels for complete de- terministic 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: --help print this help --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: 0 if all input problems were realizable 1 if at least one input problem was not realizable 2 if any error has been reported BIBLIOGRAPHY If you would like to give a reference to this tool in an article, we suggest you cite the following papers: • Florian Renkin, Philipp Schlehuber-Caissier, Alexandre Duret- Lutz, and Adrien Pommellet. Dissecting ltlsynt. In Formal Methods in System Design, 2023. • Thibaud Michaud and Maximilien Colange. Reactive Synthesis from LTL Specification with Spot. In proceedings of SYNT@CAV'18. REPORTING BUGS Report bugs to <spot@lrde.epita.fr>. COPYRIGHT Copyright (C) 2025 by the Spot authors, see the AUTHORS File for de- tails. License GPLv3+: GNU GPL version 3 or later <http://gnu.org/li- censes/gpl.html>. This is free software: you are free to change and redistribute it. There is NO WARRANTY, to the extent permitted by law. SEE ALSO ltlfsynt(1) ltlsynt (spot) 2.14.5 January 2026 LTLSYNT(1)
NAME | SYNOPSIS | DESCRIPTION | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=ltlsynt&sektion=1&manpath=FreeBSD+Ports+15.0.quarterly>