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 automata. 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 in- teger, 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 con- sidered as atomic properties --negate negate each formula --tlsf=FILENAME[/VAR=VAL[,VAR=VAL...]] Read a TLSF specification from FILENAME, and call syfco to convert 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 translation. 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 automa- ton. --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 assemble 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 basis if >=2 AP are used, (i) use implicit labels for complete deterministic au- tomata, (s) prefer state-based acceptance when possible [default], (t) force transition-based acceptance, (m) mix state and transi- tion-based acceptance, (k) use state labels when possible, (l) sin- gle-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 obtained in constant time), 'nodes' additionally displays nodes counts (com- puting those is proportional to the size of the BDD) 'paths' addi- tionally displays path counts (this can be exponential 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 op- tional for any corresponding short options. NOTE ON OUTPUT FORMATS Spot currently has little support for finite automata, and does not really support any DFA output format at the moment. When the --dot or --hoaf opetions are used, the DFA is converted into a BA1/4chi 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 Gia- como, and Moshe Y. Vardi: Engineering an LTLf Synthesis Tool. Pro- ceedings 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 details. 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.1.quarterly>