genltl − generate LTL formulas from scalable patterns
genltl [OPTION...]
Generate temporal logic formulas from predefined patterns.
−−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)))
−−dac−patterns[=RANGE], −−spec−patterns[=RANGE]
Dwyer et al. [FMSP’98] Spec. Patterns for LTL (range should be included in 1..55)
−−eh−patterns[=RANGE]
Etessami and Holzmann [Concur’00] patterns (range should be included in 1..12)
−−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)))
−−hkrss−patterns[=RANGE], −−liberouter−patterns[=RANGE]
Holeček 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
−−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]
Pelánek [Spin’07] patterns from BEEM (range should be included in 1..20)
−−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)
−−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−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.
−−negative, −−negated
output the negated versions of all formulas
−−positive
output the positive versions of all formulas (done by default, unless −−negative is specified without −−positive)
−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
specify how each line should be output (default: "%f")
−l, −−lbt
output in LBT’s syntax
−−latex
output using LaTeX macros
−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 ’>>’.
−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 sequences:
%% |
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 |
the argument of the pattern |
|||
%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) double−quotes with CSV−style escape, (p) between parentheses, any extra non−alphanumeric character will be used to separate propositions
−−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.
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:
ccj |
J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS’09. | ||
dac |
M. B. Dwyer and G. S. Avrunin and J. C. Corbett: Property Specification Patterns for Finite-state Verification. Proceedings of FMSP’98. | ||
eh |
K. Etessami and G. J. Holzmann: Optimizing Büchi Automata. Proceedings 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. | ||
hkrss |
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. | ||
go |
P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. Proceedings of CAV’01. LNCS 2102. | ||
kr |
O. Kupferman and A. Rosenberg: The Blow-Up in Translating LTL to Deterministic 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. | ||
p |
R. Pelánek: BEEM: benchmarks for explicit model checkers Proceedings of Spin’07. LNCS 4595. | ||
rv |
K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin’07. LNCS 4595. | ||
sb |
F. Somenzi and R. Bloem: Efficient Büchi Automata for LTL Formulae. Proceedings of CAV’00. LNCS 1855. | ||
tv |
D. Tabakov and M. Y. Vardi: Optimized Temporal Monitors for SystemC. Proceedings of RV’10. LNCS 6418. |
Report bugs to <spot@lrde.epita.fr>.
Copyright
© 2017 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.
randltl(1)