FreeBSD Manual Pages
LTLF2DFA(1) User Commands LTLF2DFA(1) NAME ltlf2dfa - translate LTLf formulas into DFA SYNOPSIS ltlf2dfa [OPTION...] [FORMULA...] DESCRIPTION Convert LTLf formulas to transition-based deterministic finite au- tomata. If multiple formulas are supplied, several automata will be output. Input options: -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 --lbt-input read all formulas using LBT's prefix syntax --lenient parenthesized blocks that cannot be parsed as subformulas are considered as atomic properties --negate negate each formula --tlsf=FILENAME[/VAR=VAL[,VAR=VAL...]] Read a TLSF specification from FILENAME, and call syfco to con- vert it into LTLf. Any parameter assignment specified after a slash is passed as '-op VAR=VAL' to syfco. Processing options: --composition=size|ap How to order n-ary compositions in the compositional transla- tion. By increasing size, or trying to group operands based on their APs. --keep-names Keep the names of formulas that label states in the output au- tomaton. --minimize=yes|no Minimize the automaton (enabled by default). --simplify-formula=yes|no simplify the LTLf formula with cheap rewriting rules (disabled by default) --translation=direct|compositional Whether to translate the formula directly as a whole, or to as- semble translations from subformulas. Default is compositional. Output options: -d, --dot[=options] print the automaton in DOT format -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 --mtdfa-dot print the MTDFA in DOT format --mtdfa-stats[=basic|nodes|paths] print statistics about the MTDFA: 'basic' (the default) displays only the number of states and atomic propositions (this is ob- tained in constant time), 'nodes' additionally displays nodes counts (computing those is proportional to the size of the BDD) 'paths' additionally displays path counts (this can be exponen- tial in number of atomic propositions -q, --quiet suppress all normal output Miscellaneous options: --help print this help --version print program version Mandatory or optional arguments to long options are also mandatory or optional for any corresponding short options. NOTE ON OUTPUT FORMATS Spot currently has little support for finite automata, and does not re- ally support any DFA output format at the moment. When the --dot or --hoaf opetions are used, the DFA is converted into a Bchi automaton before being displayed. BIBLIOGRAPHY The following paper describes how direct translation from LTLf to MTDFA works. • Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman, Giuseppe De Gi- acomo, and Moshe Y. Vardi: Engineering an LTLf Synthesis Tool. Proceedings of CIAA'25. To appear. 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) ltlf2dfa (spot) 2.14.5 January 2026 LTLF2DFA(1)
NAME | SYNOPSIS | DESCRIPTION | NOTE ON OUTPUT FORMATS | BIBLIOGRAPHY | REPORTING BUGS | COPYRIGHT | SEE ALSO
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=ltlf2dfa&sektion=1&manpath=FreeBSD+Ports+15.0.quarterly>