UP | HOME

GENLTL

Table of Contents

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)))

−−dac−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)))

−−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)

−−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.

Output options:

−−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 %

%a

number of atomic propositions used in the formula

%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

%L

the argument of the pattern

%s

the length (or size) of the formula

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.

BIBLIOGRAPHY

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:

gh

J. Geldenhuys and H. Hansen: Larger automata and less work for LTL model checking. Proceedings of Spin’06. LNCS 3925.

ccj

J. Cichoń, A. Czubak, and A. Jasiński: Minimal Büchi Automata for Certain Classes of LTL Formulas. Proceedings of DepCoS’09.

go

P. Gastin and D. Oddoux: Fast LTL to Büchi Automata Translation. Proceedings of CAV’01. LNCS 2102.

rv

K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin’07. LNCS 4595.

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.

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.

REPORTING BUGS

Report bugs to <spot@lrde.epita.fr>.

COPYRIGHT

Copyright © 2016 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.

SEE ALSO

randltl(1)