GENLTL

genltl - generate LTL formulas from scalable patterns

genltl [OPTION...]

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

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

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

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

Pelánek [Spin’07] patterns from BEEM (range should be included in 1..20)

--pps-arbiter-standard=RANGE

Arbiter with n clients that sent requests (ri) and receive grants (gi). Standard semantics.

--pps-arbiter-strict=RANGE

Arbiter with n clients that sent requests (ri) and receive grants (gi). 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]

φ₁,φ₂,φ₃ from Sikert et al’s [CAV’16] paper (range should be included in 1..3)

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

-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, unless --negative is specified without --positive)

-p, --full-parentheses

output fully-parenthesized formulas

-s, --spin

output in Spin’s syntax

--wring

output in Wring’s syntax

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

%h, %[vw]h

the class of the formula is the Manna-Pnueli hierarchy ([v] replaces abbreviations by class names, [w] for all compatible classes)

%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

Miscellaneous options:

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

Prefixes used in pattern names refer to the following papers:

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

Copyright © 2024 by the Spot authors, see the AUTHORS File for details. 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)