Quick Navigator

Search Site

Unix VPS
A - Starter
B - Basic
C - Preferred
D - Commercial
MPS - Dedicated
Previous VPSs
* Sign Up! *

Contact Us
Online Help
Domain Status
Man Pages

Virtual Servers

Topology Map

Server Agreement
Year 2038

USA Flag



Man Pages
GENLTL(1) User Commands GENLTL(1)

genltl - generate LTL formulas from scalable patterns

genltl [OPTION...]

Generate temporal logic formulas from predefined patterns.

--and-f=RANGE, --gh-e=RANGE
--and-gf=RANGE, --ccj-phi=RANGE, --gh-c2=RANGE
F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))
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))) &
--dac-patterns[=RANGE], --spec-patterns[=RANGE]
Dwyer et al. [FMSP'98] Spec. Patterns for LTL (range should be included in 1..55)
Etessami and Holzmann [Concur'00] patterns (range should be included in 1..12)
F(p0 | XG(p1 | XG(p2 | ... XG(pn))))
(GFa1 & GFa2 & ... & GFan) <-> GFz
GF(a <-> X^n(a))
(GFa1 & GFa2 & ... & GFan) -> GFz
GF(a -> X^n(a))
(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))
!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))
G(p0 & XF(p1 & XF(p2 & ... XF(pn))))
--hkrss-patterns[=RANGE], --liberouter-patterns[=RANGE]
Holeček et al. patterns from the Liberouter project (range should be included in 1..55)
linear formula with doubly exponential DBA
quasilinear formula with doubly exponential DBA
--kv-psi=RANGE, --kr-n2=RANGE
quadratic formula with doubly exponential DBA
--or-fg=RANGE, --ccj-xi=RANGE
--or-g=RANGE, --gh-s=RANGE
--or-gf=RANGE, --gh-c1=RANGE
--p-patterns[=RANGE], --beem-patterns[=RANGE], --p[=RANGE]
Pelánek [Spin'07] patterns from BEEM (range should be included in 1..20)
Arbiter with n clients that sent requests (ri) and receive grants (gi). Standard semantics.
Arbiter with n clients that sent requests (ri) and receive grants (gi). Strict semantics.
(((p1 R p2) R p3) ... R pn)
(p1 R (p2 R (... R pn)))
n-bit counter
n-bit counter w/ carry
n-bit counter w/ carry (linear size)
n-bit counter (linear size)
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
(GFa1&...&GFan) -> (GFb1&...&GFbn)
φ?\',φ?\\,φ?\- from Sikert et al's [CAV'16] paper (range should be included in 1..3)
G(p -> (q | Xq | ... | XX...Xq)
G(p -> (q | X(q | X(... | Xq)))
G(p -> (q & Xq & ... & XX...Xq)
G(p -> (q & X(q & X(... & Xq)))
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.

-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
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 '>>'.
output the positive versions of all formulas (done by default, unless --negative is specified without --positive)
-p, --full-parentheses
output fully-parenthesized formulas
-s, --spin
output in Spin's syntax
output in Spot's syntax (default)
output in Wring's syntax

The FORMAT string passed to --format may use the following interpreted sequences:

a single %
the Boolean-length of the formula (i.e., all Boolean subformulas count as 1)
the formula (in the selected syntax)
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)
the argument of the pattern
the nesting depth of operator OP. OP should be a single letter denoting 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.
the length (or size) of the formula
number of atomic propositions used in the
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) double-quotes with CSV-style escape, (p) between parentheses, any extra non-alphanumeric character will be used to separate propositions

print this help
print program version

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

If you would like to give a reference to this tool in an article, we suggest 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:

J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS'09.
M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property Specification Patterns for Finite-state Verification. Proceedings of FMSP'98.
K. Etessami and G. J. Holzmann: Optimizing Büchi Automata. Proceedings of Concur'00. LNCS 1877.
J. Geldenhuys and H. Hansen: Larger automata and less work for LTL model checking. Proceedings of Spin'06. LNCS 3925.
J. Holeček, T. Kratochvila, V. Řehák, D. ? afránek, and P. ? imeček: Verification Results in Liberouter Project. Tech. Report 03, CESNET, 2004.
P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. Proceedings of CAV'01. LNCS 2102.
O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic Automata. Proceedings of MoChArt'10. LNAI 6572.
O. Kupferman and M. Y. Vardi: From Linear Time to Branching Time. ACM Transactions on Computational Logic, 6(2):273-294, 2005.
D. Müller and S. Sickert: LTL to Deterministic Emerson-Lei Automata. Proceedings of GandALF'17. EPTCS 256.
R. Pelánek: BEEM: benchmarks for explicit model checkers Proceedings of Spin'07. LNCS 4595.
N. Piterman, A. Pnueli, and Y. Sa'ar: Synthesis of Reactive(1) Designs. Proceedings of VMCAI'06. LNCS 3855.
K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin'07. LNCS 4595.
F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. Proceedings of CAV'00. LNCS 1855.
S. Sickert, J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic Büchi Automata for Linear Temporal Logic. Proceedings of CAV'16. LNCS 9780.
D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. Proceedings of RV'10. LNCS 6418.

Report bugs to <>.

Copyright © 2022 Laboratoire de Recherche et Développement de l'Epita. 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.

genaut(1), ltlfilt(1), randaut(1), randltl(1)
February 2022 genltl (spot) 2.10.4

Search for    or go to Top of page |  Section 1 |  Main Index

Powered by GSP Visit the GSP FreeBSD Man Page Interface.
Output converted with ManDoc.