UP | HOME

genltl

This tool outputs LTL formulas that either comes from named lists of formulas, or from scalable patterns.

These patterns are usually taken from the literature (see the genltl(1) man page for references). Sometimes the same pattern is given different names in different papers, so we alias different option names to the same pattern.

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

An example is probably all it takes to understand how this tool works:

genltl --and-gf=1..5 --u-left=1..5
GFp1
GFp1 & GFp2
GFp1 & GFp2 & GFp3
GFp1 & GFp2 & GFp3 & GFp4
GFp1 & GFp2 & GFp3 & GFp4 & GFp5
p1
p1 U p2
(p1 U p2) U p3
((p1 U p2) U p3) U p4
(((p1 U p2) U p3) U p4) U p5

genltl supports the common option for output of LTL formulas, so you may output these pattern for various tools.

For instance here is the same formulas, but formatted in a way that is suitable for being included in a LaTeX table.

genltl --and-gf=1..5 --u-left=1..5 --latex --format='%F & %L & $%f$ \\'
and-gf & 1 & $\G \F p_{1}$ \\
and-gf & 2 & $\G \F p_{1} \land \G \F p_{2}$ \\
and-gf & 3 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3}$ \\
and-gf & 4 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4}$ \\
and-gf & 5 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4} \land \G \F p_{5}$ \\
u-left & 1 & $p_{1}$ \\
u-left & 2 & $p_{1} \U p_{2}$ \\
u-left & 3 & $(p_{1} \U p_{2}) \U p_{3}$ \\
u-left & 4 & $((p_{1} \U p_{2}) \U p_{3}) \U p_{4}$ \\
u-left & 5 & $(((p_{1} \U p_{2}) \U p_{3}) \U p_{4}) \U p_{5}$ \\

Note that for the --lbt syntax, each formula is relabeled using p0, p1, … before it is output, when the pattern (like --ccj-alpha) use different names. Compare:

genltl --ccj-alpha=3
F(p1 & F(p2 & Fp3)) & F(q1 & F(q2 & Fq3))

with

genltl --ccj-alpha=3 --lbt
& F & p0 F & p1 F p2 F & p3 F & p4 F p5

This is because most tools using lbt's syntax require atomic propositions to have the form pNN.

Five options provide lists of unrelated LTL formulas, taken from the literature (see the genltl(1) man page for references): --dac-patterns, --eh-patterns, --hkrss-patterns, --p-patterns, and --sb-patterns. With these options, the range is used to select a subset of the list of formulas. Without range, all formulas are used. Here is the complete list:

genltl --dac --eh --hkrss --p --sb --format='%F=%L,%f'
dac-patterns=1,G!p0
dac-patterns=2,Fp0 -> (!p1 U p0)
dac-patterns=3,G(p0 -> G!p1)
dac-patterns=4,G((p0 & !p1 & Fp1) -> (!p2 U p1))
dac-patterns=5,G((p0 & !p1) -> (!p2 W p1))
dac-patterns=6,Fp0
dac-patterns=7,!p0 W (!p0 & p1)
dac-patterns=8,G!p0 | F(p0 & Fp1)
dac-patterns=9,G((p0 & !p1) -> (!p1 W (!p1 & p2)))
dac-patterns=10,G((p0 & !p1) -> (!p1 U (!p1 & p2)))
dac-patterns=11,!p0 W (p0 W (!p0 W (p0 W G!p0)))
dac-patterns=12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0)))))))))
dac-patterns=13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1))))))
dac-patterns=14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1))))))))))
dac-patterns=15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1)))))))))
dac-patterns=16,Gp0
dac-patterns=17,Fp0 -> (p1 U p0)
dac-patterns=18,G(p0 -> Gp1)
dac-patterns=19,G((p0 & !p1 & Fp1) -> (p2 U p1))
dac-patterns=20,G((p0 & !p1) -> (p2 W p1))
dac-patterns=21,!p0 W p1
dac-patterns=22,Fp0 -> (!p1 U (p0 | p2))
dac-patterns=23,G!p0 | F(p0 & (!p1 W p2))
dac-patterns=24,G((p0 & !p1 & Fp1) -> (!p2 U (p1 | p3)))
dac-patterns=25,G((p0 & !p1) -> (!p2 W (p1 | p3)))
dac-patterns=26,G(p0 -> Fp1)
dac-patterns=27,Fp0 -> ((p1 -> (!p0 U (!p0 & p2))) U p0)
dac-patterns=28,G(p0 -> G(p1 -> Fp2))
dac-patterns=29,G((p0 & !p1 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3))) U p1))
dac-patterns=30,G((p0 & !p1) -> ((p2 -> (!p1 U (!p1 & p3))) W p1))
dac-patterns=31,Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2)))
dac-patterns=32,Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3))))
dac-patterns=33,G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 & X(!p1 U p3)))))
dac-patterns=34,G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4)))))
dac-patterns=35,G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1 U p4))))))
dac-patterns=36,F(p0 & XFp1) -> (!p0 U p2)
dac-patterns=37,Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p0 | p3))
dac-patterns=38,G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3))))
dac-patterns=39,G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)))
dac-patterns=40,G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)) | G!(p2 & XFp3)))
dac-patterns=41,G((p0 & XFp1) -> XF(p1 & Fp2))
dac-patterns=42,Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & Fp3))) U p0)
dac-patterns=43,G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3))))
dac-patterns=44,G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 U (p3 & Fp4))) U p1))
dac-patterns=45,G(p0 -> (((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4))) U (p2 | G((p1 & X(!p2 U p3)) -> X(!p2 U (p3 & Fp4))))))
dac-patterns=46,G(p0 -> F(p1 & XFp2))
dac-patterns=47,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3)))) U p0)
dac-patterns=48,G(p0 -> G(p1 -> (p2 & XFp3)))
dac-patterns=49,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!p1 U p4)))) U p1))
dac-patterns=50,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4)))))
dac-patterns=51,G(p0 -> F(p1 & !p2 & X(!p2 U p3)))
dac-patterns=52,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0 & !p3) U p4)))) U p0)
dac-patterns=53,G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4))))
dac-patterns=54,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4 & X((!p1 & !p4) U p5)))) U p1))
dac-patterns=55,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5))))))
eh-patterns=1,p0 U (p1 & Gp2)
eh-patterns=2,p0 U (p1 & X(p2 U p3))
eh-patterns=3,p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
eh-patterns=4,F(p0 & XGp1)
eh-patterns=5,F(p0 & X(p1 & XFp2))
eh-patterns=6,F(p0 & X(p1 U p2))
eh-patterns=7,FGp0 | GFp1
eh-patterns=8,G(p0 -> (p1 U p2))
eh-patterns=9,G(p0 & XF(p1 & XF(p2 & XFp3)))
eh-patterns=10,GFp0 & GFp1 & GFp2 & GFp3 & GFp4
eh-patterns=11,(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))
eh-patterns=12,G(p0 -> (p1 U (Gp2 | Gp3)))
hkrss-patterns=1,G(Fp0 & F!p0)
hkrss-patterns=2,GFp0 & GF!p0
hkrss-patterns=3,GF(!(p1 <-> Xp1) | !(p0 <-> Xp0))
hkrss-patterns=4,GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3))
hkrss-patterns=5,G!p0
hkrss-patterns=6,G((p0 -> F!p0) & (!p0 -> Fp0))
hkrss-patterns=7,G(p0 -> F(p0 & p1))
hkrss-patterns=8,G(p0 -> F((!p0 & p1 & p2 & p3) -> Fp4))
hkrss-patterns=9,G(p0 -> F!p1)
hkrss-patterns=10,G(p0 -> Fp1)
hkrss-patterns=11,G(p0 -> F(p1 -> Fp2))
hkrss-patterns=12,G(p0 -> F((p1 & p2) -> Fp3))
hkrss-patterns=13,G((p0 -> Fp1) & (p2 -> Fp3) & (p4 -> Fp5) & (p6 -> Fp7))
hkrss-patterns=14,G(!p0 & !p1)
hkrss-patterns=15,G!(p0 & p1)
hkrss-patterns=16,G(p0 -> p1)
hkrss-patterns=17,G((p0 -> !p1) & (p1 -> !p0))
hkrss-patterns=18,G(!p0 -> (p1 <-> !p2))
hkrss-patterns=19,G((!p0 & (p1 | p2 | p3)) -> p4)
hkrss-patterns=20,G((p0 & p1) -> (p2 | !(p3 & p4)))
hkrss-patterns=21,G((!p0 & p1 & !p2 & !p3 & !p4) -> F(!p5 & !p6 & !p7 & !p8))
hkrss-patterns=22,G((p0 & p1 & !p2 & !p3 & !p4) -> F(p5 & !p6 & !p7 & !p8))
hkrss-patterns=23,G(!p0 -> !(p1 & p2 & p3 & p4 & p5))
hkrss-patterns=24,G(!p0 -> ((p1 & p2 & p3 & p4) -> !p5))
hkrss-patterns=25,G((p0 & p1) -> (p2 | p3 | !(p4 & p5)))
hkrss-patterns=26,G((!p0 & (p1 | p2 | p3 | p4)) -> (!p5 <-> p6))
hkrss-patterns=27,G((p0 & p1) -> (p2 | p3 | p4 | !(p5 & p6)))
hkrss-patterns=28,G((p0 & p1) -> (p2 | p3 | p4 | p5 | !(p6 & p7)))
hkrss-patterns=29,G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3)))
hkrss-patterns=30,G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3))))))
hkrss-patterns=31,G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3)))))
hkrss-patterns=32,G(p0 -> (p1 U (!p1 U (!p2 | p3))))
hkrss-patterns=33,G(p0 -> (p1 U (!p1 U (p2 | p3))))
hkrss-patterns=34,G((!p0 & p1) -> Xp2)
hkrss-patterns=35,G(p0 -> X(p0 | p1))
hkrss-patterns=36,G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) -> (X!p4 & X(!(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) U p4)))
hkrss-patterns=37,G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))
hkrss-patterns=38,G(p0 -> X(!p0 U p1))
hkrss-patterns=39,G((!p0 & Xp0) -> X((p0 U p1) | Gp0))
hkrss-patterns=40,G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1))))
hkrss-patterns=41,G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 & (p0 U (p0 & !p1 & X(p0 & p1)))))))
hkrss-patterns=42,G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1)))))))
hkrss-patterns=43,G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1))))))))))
hkrss-patterns=44,G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1)))
hkrss-patterns=45,G(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X(!p0 | X!p0)))))))))))
hkrss-patterns=46,G((Xp0 -> p0) -> (p1 <-> Xp1))
hkrss-patterns=47,G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1)))
hkrss-patterns=48,!p0 U G!((p1 & p2) | (p3 & p4) | (p2 & p3) | (p2 & p4) | (p1 & p4) | (p1 & p3))
hkrss-patterns=49,!p0 U p1
hkrss-patterns=50,(p0 U p1) | Gp0
hkrss-patterns=51,p0 & XG!p0
hkrss-patterns=52,XG(p0 -> (G!p1 | (!Xp1 U p2)))
hkrss-patterns=53,XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))
hkrss-patterns=54,XG((p0 & p1) -> ((p1 U p2) | Gp1))
hkrss-patterns=55,Xp0 & G((!p0 & Xp0) -> XXp0)
p-patterns=1,G(p0 -> Fp1)
p-patterns=2,(GFp1 & GFp0) -> GFp2
p-patterns=3,G(p0 -> (p1 & (p2 U p3)))
p-patterns=4,F(p0 | p1)
p-patterns=5,GF(p0 | p1)
p-patterns=6,(p0 U p1) -> ((p2 U p3) | Gp2)
p-patterns=7,G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))
p-patterns=8,G(p0 -> (p1 R !p2))
p-patterns=9,G(!p0 -> Fp0)
p-patterns=10,G(p0 -> F(p1 | p2))
p-patterns=11,!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))
p-patterns=12,G!p0 -> G!p1
p-patterns=13,G(p0 -> (G!p1 | (!p2 U p1)))
p-patterns=14,G(p0 -> (p1 R (p1 | !p2)))
p-patterns=15,G((p0 & p1) -> (!p1 R (p0 | !p1)))
p-patterns=16,G(p0 -> F(p1 & p2))
p-patterns=17,G(p0 -> (!p1 U (p1 U (p1 & p2))))
p-patterns=18,G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))
p-patterns=19,GFp0 -> GFp1
p-patterns=20,GF(p0 | p1) & GF(p1 | p2)
sb-patterns=1,p0 U p1
sb-patterns=2,p0 U (p1 U p2)
sb-patterns=3,!(p0 U (p1 U p2))
sb-patterns=4,GFp0 -> GFp1
sb-patterns=5,Fp0 U Gp1
sb-patterns=6,Gp0 U p1
sb-patterns=7,!(Fp0 <-> Fp1)
sb-patterns=8,!(GFp0 -> GFp1)
sb-patterns=9,!(GFp0 <-> GFp1)
sb-patterns=10,p0 R (p0 | p1)
sb-patterns=11,(Xp0 U Xp1) | !X(p0 U p1)
sb-patterns=12,(Xp0 U p1) | !X(p0 U (p0 & p1))
sb-patterns=13,G(p0 -> Fp1) & ((Xp0 U p1) | !X(p0 U (p0 & p1)))
sb-patterns=14,G(p0 -> Fp1) & ((Xp0 U Xp1) | !X(p0 U p1))
sb-patterns=15,G(p0 -> Fp1)
sb-patterns=16,!G(p0 -> X(p1 R p2))
sb-patterns=17,!(FGp0 | FGp1)
sb-patterns=18,G(Fp0 & Fp1)
sb-patterns=19,Fp0 & F!p0
sb-patterns=20,(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0))
sb-patterns=21,Gp2 | Gp0 | (G(p0 | GFp1) & G(p2 | GF!p1))
sb-patterns=22,Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1))
sb-patterns=23,!(Gp2 | Gp0 | (G(p0 | GFp1) & G(p2 | GF!p1)))
sb-patterns=24,!(Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1)))
sb-patterns=25,G(p0 | XGp1) & G(p2 | XG!p1)
sb-patterns=26,G(p0 | (Xp1 & X!p1))
sb-patterns=27,p0 | (p1 U p0)

Note that --sb-patterns=2 --sb-patterns=4 --sb-patterns=21..22 also have their complement formulas listed as --sb-patterns=3 --sb-patterns=8 --sb-patterns=23..24. So if you build the set of formulas output by genltl --sb-patterns plus their negations, it will contain only 46 formulas, not 54.

genltl --sb | ltlfilt --uniq --count
genltl --sb --pos --neg | ltlfilt --uniq --count
27
46