FreeBSD Manual Pages
GENLTL(1) User Commands GENLTL(1) NAME genltl - generate LTL formulas from scalable patterns SYNOPSIS genltl [OPTION...] DESCRIPTION Generate temporal logic formulas from predefined patterns. Pattern selection: --and-f=RANGE, --gh-e=RANGE F(p1)&F(p2)&...&F(pn) --and-fg=RANGE FG(p1)&FG(p2)&...&FG(pn) --and-gf=RANGE, --ccj-phi=RANGE, --gh-c2=RANGE GF(p1)&GF(p2)&...&GF(pn) --ccj-alpha=RANGE F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn)))) --ccj-beta=RANGE F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q)))) --ccj-beta-prime=RANGE F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q))) --chomp-mealy=RANGE[,RANGE] LTL/LTLf formula for NxM Chomp game, with Mealy semantics --dac-patterns[=RANGE], --spec-patterns[=RANGE] Dwyer et al. [FMSP'98] Spec. Patterns for LTL (range should be in- cluded in 1..55) --eh-patterns[=RANGE] Etessami and Holzmann [Concur'00] patterns (range should be included in 1..12) --eil-gsi=RANGE G[0..n]((a S b) -> c) rewritten using future operators --fxg-or=RANGE F(p0 | XG(p1 | XG(p2 | ... XG(pn)))) --gf-equiv=RANGE (GFa1 & GFa2 & ... & GFan) <-> GFz --gf-equiv-xn=RANGE GF(a <-> X^n(a)) --gf-implies=RANGE (GFa1 & GFa2 & ... & GFan) -> GFz --gf-implies-xn=RANGE GF(a -> X^n(a)) --gh-q=RANGE (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1})) --gh-r=RANGE (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1})) --go-theta=RANGE !((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r))) --gxf-and=RANGE G(p0 & XF(p1 & XF(p2 & ... XF(pn)))) --hkrss-patterns[=RANGE], --liberouter-patterns[=RANGE] HoleAek et al. patterns from the Liberouter project (range should be included in 1..55) --kr-n=RANGE linear formula with doubly exponential DBA --kr-nlogn=RANGE quasilinear formula with doubly exponential DBA --kv-psi=RANGE, --kr-n2=RANGE quadratic formula with doubly exponential DBA --lily-patterns[=RANGE], --jb-patterns[=RANGE] LTL synthesis specification examples from Lily 1.0.2 [Jobstmann & Bloem, FMCAD'06] (range should be included in 1..23) --ms-example=RANGE[,RANGE] GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm))) --ms-phi-h=RANGE FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) --or-fg=RANGE, --ccj-xi=RANGE FG(p1)|FG(p2)|...|FG(pn) --or-g=RANGE, --gh-s=RANGE G(p1)|G(p2)|...|G(pn) --or-gf=RANGE, --gh-c1=RANGE GF(p1)|GF(p2)|...|GF(pn) --p-patterns[=RANGE], --beem-patterns[=RANGE], --p[=RANGE] PelA!nek [Spin'07] patterns from BEEM (range should be included in 1..20) --pps-arbiter-standard=RANGE Arbiter with n clients that sent requests (iN) and receive grants (oN). Standard semantics. --pps-arbiter-strict=RANGE Arbiter with n clients that sent requests (iN) and receive grants (oN). Strict semantics. --r-left=RANGE (((p1 R p2) R p3) ... R pn) --r-right=RANGE (p1 R (p2 R (... R pn))) --rv-counter=RANGE n-bit counter --rv-counter-carry=RANGE n-bit counter w/ carry --rv-counter-carry-linear=RANGE n-bit counter w/ carry (linear size) --rv-counter-linear=RANGE n-bit counter (linear size) --sb-patterns[=RANGE] Somenzi and Bloem [CAV'00] patterns (range should be included in 1..27) --sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U G(f(i-1,j))) --sejk-j=RANGE (GFa1&...&GFan) -> (GFb1&...&GFbn) --sejk-k=RANGE (GFa1|FGb1)&...&(GFan|FGbn) --sejk-patterns[=RANGE] Ia,Ia,Ia from Sikert et al's [CAV'16] paper (range should be in- cluded in 1..3) --tv-counter-mealy=RANGE LTLf formula for Single Counter game, with Mealy semantics --tv-double-counters-mealy=RANGE LTLf formula for Double Counters game, with Mealy semantics --tv-f1=RANGE G(p -> (q | Xq | ... | XX...Xq) --tv-f2=RANGE G(p -> (q | X(q | X(... | Xq))) --tv-g1=RANGE G(p -> (q & Xq & ... & XX...Xq) --tv-g2=RANGE G(p -> (q & X(q & X(... & Xq))) --tv-nim-mealy=RANGE[,RANGE] LTLf formula specifying a Nim game, with Mealy semantics. Uses N heaps of M tokens, with M defaulting to N if not supplied. --tv-uu=RANGE G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...)))))) --u-left=RANGE, --gh-u=RANGE (((p1 U p2) U p3) ... U pn) --u-right=RANGE, --gh-u2=RANGE, --go-phi=RANGE (p1 U (p2 U (... U pn))) RANGE may have one of the following forms: 'INT', 'INT..INT', or '..INT'. In the latter case, the missing number is assumed to be 1. Output options: -0, --zero-terminated-output separate output formulas with \0 instead of \n (for use with xargs -0) -8, --utf8 output using UTF-8 characters --format=FORMAT, --stats=FORMAT specify how each line should be output (default: "%f") -l, --lbt output in LBT's syntax --latex output using LaTeX macros --negative, --negated output the negated versions of all formulas -o, --output=FORMAT send output to a file named FORMAT instead of standard output. The first formula sent to a file truncates it unless FORMAT starts with '>>'. --positive output the positive versions of all formulas (done by default, un- less --negative is specified without --positive) -p, --full-parentheses output fully-parenthesized formulas -s, --spin output in Spin's syntax --spot output in Spot's syntax (default) --wring output in Wring's syntax The FORMAT string passed to --format may use the following interpreted se- quences: %% a single % %b the Boolean-length of the formula (i.e., all Boolean subformulas count as 1) %f the formula (in the selected syntax) %F the name of the pattern %h, %[vw]h the class of the formula is the Manna-Pnueli hierarchy ([v] replaces abbreviations by class names, [w] for all compatible classes) %l serial number of the output formula (0-based) %L the argument of the pattern %[OP]n the nesting depth of operator OP. OP should be a single letter de- noting the operator to count, or multiple letters to fuse several operators during depth evaluation. Add '~' to rewrite the formula in negative normal form before counting. %s the length (or size) of the formula %x, %[LETTERS]X, %[LETTERS]x number of atomic propositions used in the formula; add LETTERS to list atomic propositions with (n) no quoting, (s) occasional double-quotes with C-style escape, (d) double-quotes with C-style escape, (c) dou- ble-quotes with CSV-style escape, (p) between parentheses, any extra non-alphanumeric character will be used to separate propositions 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. BIBLIOGRAPHY If you would like to give a reference to this tool in an article, we sug- gest you cite the following paper: * Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0. Proceedings of ATVA'13. LNCS 8172. Prefixes used in pattern names refer to the following papers: ccj J. CichoA, A. Czubak, and A. JasiAski: Minimal BA1/4chi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS'09. dac M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property Specifica- tion Patterns for Finite-state Verification. Proceedings of FMSP'98. eh K. Etessami and G. J. Holzmann: Optimizing BA1/4chi Automata. Pro- ceedings of Concur'00. LNCS 1877. gh J. Geldenhuys and H. Hansen: Larger automata and less work for LTL model checking. Proceedings of Spin'06. LNCS 3925. go P. Gastin and D. Oddoux: Fast LTL to BA1/4chi Automata Translation. Proceedings of CAV'01. LNCS 2102. hkrss J. HoleAek, T. Kratochvila, V. AehA!k, D. A afrA!nek, and P. A imeAek: Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004. jb, lily B. Jobstmann, and R. Bloem: Optimizations for LTL Synthesis. Pro- ceedings of FMCAD'06. IEEE. kr O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to De- terministic Automata. Proceedings of MoChArt'10. LNAI 6572. kv O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. ACM Transactions on Computational Logic, 6(2):273-294, 2005. ms D. MA1/4ller and S. Sickert: LTL to Deterministic Emerson-Lei Au- tomata. Proceedings of GandALF'17. EPTCS 256. p R. PelA!nek: BEEM: benchmarks for explicit model checkers Proceed- ings of Spin'07. LNCS 4595. pps N. Piterman, A. Pnueli, and Y. Sa'ar: Synthesis of Reactive(1) De- signs. Proceedings of VMCAI'06. LNCS 3855. rv K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin'07. LNCS 4595. sb F. Somenzi and R. Bloem: Efficient BA1/4chi Automata for LTL Formu- lae. Proceedings of CAV'00. LNCS 1855. sejk S. Sickert, J. Esparza, S. Jaax, and J. KAetAnskA1/2: Limit-Deter- ministic BA1/4chi Automata for Linear Temporal Logic. Proceedings of CAV'16. LNCS 9780. tv D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. Proceedings of RV'10. LNCS 6418. tv L. M. Tabajara and M. Y. Vardi: Partitioning Techniques in LTLf Syn- thesis. Proceedings of IJCAI'19. 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 genaut(1), ltlfilt(1), randaut(1), randltl(1) ltlmix(1) genltl (spot) 2.14.5 January 2026 GENLTL(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=genltl&sektion=1&manpath=FreeBSD+Ports+15.1.quarterly>