1# -*- coding: utf-8 -*-
2#+TITLE: =genltl=
3#+DESCRIPTION: Spot command-line tool that generates LTL formulas from known patterns
4#+INCLUDE: setup.org
5#+HTML_LINK_UP: tools.html
6#+PROPERTY: header-args:sh :results verbatim :exports both
7
8This tool outputs LTL formulas that either comes from named lists of
9formulas, or from scalable patterns.
10
11These patterns are usually taken from the literature (see the
12[[./man/genltl.1.html][=genltl=]](1) man page for references).  Sometimes the same pattern is
13given different names in different papers, so we alias different
14option names to the same pattern.
15
16#+BEGIN_SRC sh :exports results
17genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
18#+END_SRC
19#+RESULTS:
20#+begin_example
21      --and-f=RANGE, --gh-e=RANGE
22                             F(p1)&F(p2)&...&F(pn)
23      --and-fg=RANGE         FG(p1)&FG(p2)&...&FG(pn)
24      --and-gf=RANGE, --ccj-phi=RANGE, --gh-c2=RANGE
25                             GF(p1)&GF(p2)&...&GF(pn)
26      --ccj-alpha=RANGE      F(p1&F(p2&F(p3&...F(pn)))) &
27                             F(q1&F(q2&F(q3&...F(qn))))
28      --ccj-beta=RANGE       F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))
29      --ccj-beta-prime=RANGE F(p&(Xp)&(XXp)&...(X...X(p))) &
30                             F(q&(Xq)&(XXq)&...(X...X(q)))
31      --dac-patterns[=RANGE], --spec-patterns[=RANGE]
32                             Dwyer et al. [FMSP'98] Spec. Patterns for LTL
33                             (range should be included in 1..55)
34      --eh-patterns[=RANGE]  Etessami and Holzmann [Concur'00] patterns (range
35                             should be included in 1..12)
36      --fxg-or=RANGE         F(p0 | XG(p1 | XG(p2 | ... XG(pn))))
37      --gf-equiv=RANGE       (GFa1 & GFa2 & ... & GFan) <-> GFz
38      --gf-equiv-xn=RANGE    GF(a <-> X^n(a))
39      --gf-implies=RANGE     (GFa1 & GFa2 & ... & GFan) -> GFz
40      --gf-implies-xn=RANGE  GF(a -> X^n(a))
41      --gh-q=RANGE           (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))
42      --gh-r=RANGE           (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...
43                             &(GF(pn)|FG(p{n+1}))
44      --go-theta=RANGE       !((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))
45      --gxf-and=RANGE        G(p0 & XF(p1 & XF(p2 & ... XF(pn))))
46      --hkrss-patterns[=RANGE], --liberouter-patterns[=RANGE]
47                             Holeček et al. patterns from the Liberouter
48                             project (range should be included in 1..55)
49      --kr-n=RANGE           linear formula with doubly exponential DBA
50      --kr-nlogn=RANGE       quasilinear formula with doubly exponential DBA
51      --kv-psi=RANGE, --kr-n2=RANGE
52                             quadratic formula with doubly exponential DBA
53      --ms-example=RANGE[,RANGE]
54                             GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))
55      --ms-phi-h=RANGE       FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...
56      --ms-phi-r=RANGE       (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))
57      --ms-phi-s=RANGE       (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))
58      --or-fg=RANGE, --ccj-xi=RANGE
59                             FG(p1)|FG(p2)|...|FG(pn)
60      --or-g=RANGE, --gh-s=RANGE   G(p1)|G(p2)|...|G(pn)
61      --or-gf=RANGE, --gh-c1=RANGE
62                             GF(p1)|GF(p2)|...|GF(pn)
63      --p-patterns[=RANGE], --beem-patterns[=RANGE], --p[=RANGE]
64                             Pelánek [Spin'07] patterns from BEEM (range
65                             should be included in 1..20)
66      --r-left=RANGE         (((p1 R p2) R p3) ... R pn)
67      --r-right=RANGE        (p1 R (p2 R (... R pn)))
68      --rv-counter=RANGE     n-bit counter
69      --rv-counter-carry=RANGE   n-bit counter w/ carry
70      --rv-counter-carry-linear=RANGE
71                             n-bit counter w/ carry (linear size)
72      --rv-counter-linear=RANGE   n-bit counter (linear size)
73      --sb-patterns[=RANGE]  Somenzi and Bloem [CAV'00] patterns (range should
74                             be included in 1..27)
75      --sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U
76                             G(f(i-1,j)))
77      --sejk-j=RANGE         (GFa1&...&GFan) -> (GFb1&...&GFbn)
78      --sejk-k=RANGE         (GFa1|FGb1)&...&(GFan|FGbn)
79      --sejk-patterns[=RANGE]   φ₁,φ₂,φ₃ from Sikert et al's [CAV'16]
80                             paper (range should be included in 1..3)
81      --tv-f1=RANGE          G(p -> (q | Xq | ... | XX...Xq)
82      --tv-f2=RANGE          G(p -> (q | X(q | X(... | Xq)))
83      --tv-g1=RANGE          G(p -> (q & Xq & ... & XX...Xq)
84      --tv-g2=RANGE          G(p -> (q & X(q & X(... & Xq)))
85      --tv-uu=RANGE          G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...))))))
86      --u-left=RANGE, --gh-u=RANGE
87                             (((p1 U p2) U p3) ... U pn)
88      --u-right=RANGE, --gh-u2=RANGE, --go-phi=RANGE
89                             (p1 U (p2 U (... U pn)))
90#+end_example
91
92An example is probably all it takes to understand how this tool works:
93
94#+BEGIN_SRC sh
95genltl --and-gf=1..5 --u-left=1..5
96#+END_SRC
97#+RESULTS:
98#+begin_example
99GFp1
100GFp1 & GFp2
101GFp1 & GFp2 & GFp3
102GFp1 & GFp2 & GFp3 & GFp4
103GFp1 & GFp2 & GFp3 & GFp4 & GFp5
104p1
105p1 U p2
106(p1 U p2) U p3
107((p1 U p2) U p3) U p4
108(((p1 U p2) U p3) U p4) U p5
109#+end_example
110
111=genltl= supports the [[file:ioltl.org][common option for output of LTL formulas]], so you
112may output these pattern for various tools.
113
114For instance here is the same formulas, but formatted in a way that is
115suitable for being included in a LaTeX table.
116
117
118#+BEGIN_SRC sh
119genltl --and-gf=1..5 --u-left=1..5 --latex --format='%F & %L & $%f$ \\'
120#+END_SRC
121#+RESULTS:
122#+begin_example
123and-gf & 1 & $\G \F p_{1}$ \\
124and-gf & 2 & $\G \F p_{1} \land \G \F p_{2}$ \\
125and-gf & 3 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3}$ \\
126and-gf & 4 & $\G \F p_{1} \land \G \F p_{2} \land \G \F p_{3} \land \G \F p_{4}$ \\
127and-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}$ \\
128u-left & 1 & $p_{1}$ \\
129u-left & 2 & $p_{1} \U p_{2}$ \\
130u-left & 3 & $(p_{1} \U p_{2}) \U p_{3}$ \\
131u-left & 4 & $((p_{1} \U p_{2}) \U p_{3}) \U p_{4}$ \\
132u-left & 5 & $(((p_{1} \U p_{2}) \U p_{3}) \U p_{4}) \U p_{5}$ \\
133#+end_example
134
135Note that for the =--lbt= syntax, each formula is relabeled using
136=p0=, =p1=, ...  before it is output, when the pattern (like
137=--ccj-alpha=) use different names.  Compare:
138
139#+BEGIN_SRC sh
140genltl --ccj-alpha=3
141#+END_SRC
142#+RESULTS:
143: F(p1 & F(p2 & Fp3)) & F(q1 & F(q2 & Fq3))
144
145with
146
147#+BEGIN_SRC sh
148genltl --ccj-alpha=3 --lbt
149#+END_SRC
150#+RESULTS:
151: & F & p0 F & p1 F p2 F & p3 F & p4 F p5
152
153This is because most tools using =lbt='s syntax require atomic
154propositions to have the form =pNN=.
155
156
157Five options provide lists of unrelated LTL formulas, taken from the
158literature (see the [[./man/genltl.1.html][=genltl=]](1) man page for references):
159=--dac-patterns=, =--eh-patterns=, =--hkrss-patterns=, =--p-patterns=,
160and =--sb-patterns=.  With these options, the range is used to select
161a subset of the list of formulas.  Without range, all formulas are
162used.  Here is the complete list:
163
164#+BEGIN_SRC sh
165  genltl --dac --eh --hkrss --p --sb --format='%F=%L,%f'
166#+END_SRC
167
168#+RESULTS:
169#+begin_example
170dac-patterns=1,G!p0
171dac-patterns=2,Fp0 -> (!p1 U p0)
172dac-patterns=3,G(p0 -> G!p1)
173dac-patterns=4,G((p0 & !p1 & Fp1) -> (!p2 U p1))
174dac-patterns=5,G((p0 & !p1) -> (!p2 W p1))
175dac-patterns=6,Fp0
176dac-patterns=7,!p0 W (!p0 & p1)
177dac-patterns=8,G!p0 | F(p0 & Fp1)
178dac-patterns=9,G((p0 & !p1) -> (!p1 W (!p1 & p2)))
179dac-patterns=10,G((p0 & !p1) -> (!p1 U (!p1 & p2)))
180dac-patterns=11,!p0 W (p0 W (!p0 W (p0 W G!p0)))
181dac-patterns=12,Fp0 -> ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | ((!p0 & !p1) U (p0 | ((!p0 & p1) U (p0 | (!p1 U p0)))))))))
182dac-patterns=13,Fp0 -> (!p0 U (p0 & (!p1 W (p1 W (!p1 W (p1 W G!p1))))))
183dac-patterns=14,G((p0 & Fp1) -> ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | ((!p1 & !p2) U (p1 | ((!p1 & p2) U (p1 | (!p2 U p1))))))))))
184dac-patterns=15,G(p0 -> ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | ((!p1 & !p2) U (p2 | ((p1 & !p2) U (p2 | (!p1 W p2) | Gp1)))))))))
185dac-patterns=16,Gp0
186dac-patterns=17,Fp0 -> (p1 U p0)
187dac-patterns=18,G(p0 -> Gp1)
188dac-patterns=19,G((p0 & !p1 & Fp1) -> (p2 U p1))
189dac-patterns=20,G((p0 & !p1) -> (p2 W p1))
190dac-patterns=21,!p0 W p1
191dac-patterns=22,Fp0 -> (!p1 U (p0 | p2))
192dac-patterns=23,G!p0 | F(p0 & (!p1 W p2))
193dac-patterns=24,G((p0 & !p1 & Fp1) -> (!p2 U (p1 | p3)))
194dac-patterns=25,G((p0 & !p1) -> (!p2 W (p1 | p3)))
195dac-patterns=26,G(p0 -> Fp1)
196dac-patterns=27,Fp0 -> ((p1 -> (!p0 U (!p0 & p2))) U p0)
197dac-patterns=28,G(p0 -> G(p1 -> Fp2))
198dac-patterns=29,G((p0 & !p1 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3))) U p1))
199dac-patterns=30,G((p0 & !p1) -> ((p2 -> (!p1 U (!p1 & p3))) W p1))
200dac-patterns=31,Fp0 -> (!p0 U (!p0 & p1 & X(!p0 U p2)))
201dac-patterns=32,Fp0 -> (!p1 U (p0 | (!p1 & p2 & X(!p1 U p3))))
202dac-patterns=33,G!p0 | (!p0 U ((p0 & Fp1) -> (!p1 U (!p1 & p2 & X(!p1 U p3)))))
203dac-patterns=34,G((p0 & Fp1) -> (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4)))))
204dac-patterns=35,G(p0 -> (Fp1 -> (!p1 U (p2 | (!p1 & p3 & X(!p1 U p4))))))
205dac-patterns=36,F(p0 & XFp1) -> (!p0 U p2)
206dac-patterns=37,Fp0 -> (!(!p0 & p1 & X(!p0 U (!p0 & p2))) U (p0 | p3))
207dac-patterns=38,G!p0 | (!p0 U (p0 & (F(p1 & XFp2) -> (!p1 U p3))))
208dac-patterns=39,G((p0 & Fp1) -> (!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)))
209dac-patterns=40,G(p0 -> ((!(!p1 & p2 & X(!p1 U (!p1 & p3))) U (p1 | p4)) | G!(p2 & XFp3)))
210dac-patterns=41,G((p0 & XFp1) -> XF(p1 & Fp2))
211dac-patterns=42,Fp0 -> (((p1 & X(!p0 U p2)) -> X(!p0 U (p2 & Fp3))) U p0)
212dac-patterns=43,G(p0 -> G((p1 & XFp2) -> X(!p2 U (p2 & Fp3))))
213dac-patterns=44,G((p0 & Fp1) -> (((p2 & X(!p1 U p3)) -> X(!p1 U (p3 & Fp4))) U p1))
214dac-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))))))
215dac-patterns=46,G(p0 -> F(p1 & XFp2))
216dac-patterns=47,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & X(!p0 U p3)))) U p0)
217dac-patterns=48,G(p0 -> G(p1 -> (p2 & XFp3)))
218dac-patterns=49,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & X(!p1 U p4)))) U p1))
219dac-patterns=50,G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4)))))
220dac-patterns=51,G(p0 -> F(p1 & !p2 & X(!p2 U p3)))
221dac-patterns=52,Fp0 -> ((p1 -> (!p0 U (!p0 & p2 & !p3 & X((!p0 & !p3) U p4)))) U p0)
222dac-patterns=53,G(p0 -> G(p1 -> (p2 & !p3 & X(!p3 U p4))))
223dac-patterns=54,G((p0 & Fp1) -> ((p2 -> (!p1 U (!p1 & p3 & !p4 & X((!p1 & !p4) U p5)))) U p1))
224dac-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))))))
225eh-patterns=1,p0 U (p1 & Gp2)
226eh-patterns=2,p0 U (p1 & X(p2 U p3))
227eh-patterns=3,p0 U (p1 & X(p2 & F(p3 & XF(p4 & XF(p5 & XFp6)))))
228eh-patterns=4,F(p0 & XGp1)
229eh-patterns=5,F(p0 & X(p1 & XFp2))
230eh-patterns=6,F(p0 & X(p1 U p2))
231eh-patterns=7,FGp0 | GFp1
232eh-patterns=8,G(p0 -> (p1 U p2))
233eh-patterns=9,G(p0 & XF(p1 & XF(p2 & XFp3)))
234eh-patterns=10,GFp0 & GFp1 & GFp2 & GFp3 & GFp4
235eh-patterns=11,(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))
236eh-patterns=12,G(p0 -> (p1 U (Gp2 | Gp3)))
237hkrss-patterns=1,G(Fp0 & F!p0)
238hkrss-patterns=2,GFp0 & GF!p0
239hkrss-patterns=3,GF(!(p1 <-> Xp1) | !(p0 <-> Xp0))
240hkrss-patterns=4,GF(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3))
241hkrss-patterns=5,G!p0
242hkrss-patterns=6,G((p0 -> F!p0) & (!p0 -> Fp0))
243hkrss-patterns=7,G(p0 -> F(p0 & p1))
244hkrss-patterns=8,G(p0 -> F((!p0 & p1 & p2 & p3) -> Fp4))
245hkrss-patterns=9,G(p0 -> F!p1)
246hkrss-patterns=10,G(p0 -> Fp1)
247hkrss-patterns=11,G(p0 -> F(p1 -> Fp2))
248hkrss-patterns=12,G(p0 -> F((p1 & p2) -> Fp3))
249hkrss-patterns=13,G((p0 -> Fp1) & (p2 -> Fp3) & (p4 -> Fp5) & (p6 -> Fp7))
250hkrss-patterns=14,G(!p0 & !p1)
251hkrss-patterns=15,G!(p0 & p1)
252hkrss-patterns=16,G(p0 -> p1)
253hkrss-patterns=17,G((p0 -> !p1) & (p1 -> !p0))
254hkrss-patterns=18,G(!p0 -> (p1 <-> !p2))
255hkrss-patterns=19,G((!p0 & (p1 | p2 | p3)) -> p4)
256hkrss-patterns=20,G((p0 & p1) -> (p2 | !(p3 & p4)))
257hkrss-patterns=21,G((!p0 & p1 & !p2 & !p3 & !p4) -> F(!p5 & !p6 & !p7 & !p8))
258hkrss-patterns=22,G((p0 & p1 & !p2 & !p3 & !p4) -> F(p5 & !p6 & !p7 & !p8))
259hkrss-patterns=23,G(!p0 -> !(p1 & p2 & p3 & p4 & p5))
260hkrss-patterns=24,G(!p0 -> ((p1 & p2 & p3 & p4) -> !p5))
261hkrss-patterns=25,G((p0 & p1) -> (p2 | p3 | !(p4 & p5)))
262hkrss-patterns=26,G((!p0 & (p1 | p2 | p3 | p4)) -> (!p5 <-> p6))
263hkrss-patterns=27,G((p0 & p1) -> (p2 | p3 | p4 | !(p5 & p6)))
264hkrss-patterns=28,G((p0 & p1) -> (p2 | p3 | p4 | p5 | !(p6 & p7)))
265hkrss-patterns=29,G((p0 & p1 & !p2 & Xp2) -> X(p3 | X(!p1 | p3)))
266hkrss-patterns=30,G((p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3))))))
267hkrss-patterns=31,G(p0 & p1 & !p2 & Xp2) -> X(X!p1 | (p2 U (!p2 U (p2 U (!p1 | p3)))))
268hkrss-patterns=32,G(p0 -> (p1 U (!p1 U (!p2 | p3))))
269hkrss-patterns=33,G(p0 -> (p1 U (!p1 U (p2 | p3))))
270hkrss-patterns=34,G((!p0 & p1) -> Xp2)
271hkrss-patterns=35,G(p0 -> X(p0 | p1))
272hkrss-patterns=36,G((!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) -> (X!p4 & X(!(!(p1 <-> Xp1) | !(p0 <-> Xp0) | !(p2 <-> Xp2) | !(p3 <-> Xp3)) U p4)))
273hkrss-patterns=37,G((p0 & !p1 & Xp1 & Xp0) -> (p2 -> Xp3))
274hkrss-patterns=38,G(p0 -> X(!p0 U p1))
275hkrss-patterns=39,G((!p0 & Xp0) -> X((p0 U p1) | Gp0))
276hkrss-patterns=40,G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1))))
277hkrss-patterns=41,G((!p0 & Xp0) -> X(p0 U (p0 & !p1 & X(p0 & p1 & (p0 U (p0 & !p1 & X(p0 & p1)))))))
278hkrss-patterns=42,G((p0 & X!p0) -> X(!p0 U (!p0 & !p1 & X(!p0 & p1 & (!p0 U (!p0 & !p1 & X(!p0 & p1)))))))
279hkrss-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))))))))))
280hkrss-patterns=44,G((!p0 & Xp0) -> X(!(!p0 & Xp0) U (!p1 & Xp1)))
281hkrss-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)))))))))))
282hkrss-patterns=46,G((Xp0 -> p0) -> (p1 <-> Xp1))
283hkrss-patterns=47,G((Xp0 -> p0) -> ((p1 -> Xp1) & (!p1 -> X!p1)))
284hkrss-patterns=48,!p0 U G!((p1 & p2) | (p3 & p4) | (p2 & p3) | (p2 & p4) | (p1 & p4) | (p1 & p3))
285hkrss-patterns=49,!p0 U p1
286hkrss-patterns=50,(p0 U p1) | Gp0
287hkrss-patterns=51,p0 & XG!p0
288hkrss-patterns=52,XG(p0 -> (G!p1 | (!Xp1 U p2)))
289hkrss-patterns=53,XG((p0 & !p1) -> (G!p1 | (!p1 U p2)))
290hkrss-patterns=54,XG((p0 & p1) -> ((p1 U p2) | Gp1))
291hkrss-patterns=55,Xp0 & G((!p0 & Xp0) -> XXp0)
292p-patterns=1,G(p0 -> Fp1)
293p-patterns=2,(GFp1 & GFp0) -> GFp2
294p-patterns=3,G(p0 -> (p1 & (p2 U p3)))
295p-patterns=4,F(p0 | p1)
296p-patterns=5,GF(p0 | p1)
297p-patterns=6,(p0 U p1) -> ((p2 U p3) | Gp2)
298p-patterns=7,G(p0 -> (!p1 U (p1 U (!p1 & (p2 R !p1)))))
299p-patterns=8,G(p0 -> (p1 R !p2))
300p-patterns=9,G(!p0 -> Fp0)
301p-patterns=10,G(p0 -> F(p1 | p2))
302p-patterns=11,!(!(p0 | p1) U p2) & G(p3 -> !(!(p0 | p1) U p2))
303p-patterns=12,G!p0 -> G!p1
304p-patterns=13,G(p0 -> (G!p1 | (!p2 U p1)))
305p-patterns=14,G(p0 -> (p1 R (p1 | !p2)))
306p-patterns=15,G((p0 & p1) -> (!p1 R (p0 | !p1)))
307p-patterns=16,G(p0 -> F(p1 & p2))
308p-patterns=17,G(p0 -> (!p1 U (p1 U (p1 & p2))))
309p-patterns=18,G(p0 -> (!p1 U (p1 U (!p1 U (p1 U (p1 & p2))))))
310p-patterns=19,GFp0 -> GFp1
311p-patterns=20,GF(p0 | p1) & GF(p1 | p2)
312sb-patterns=1,p0 U p1
313sb-patterns=2,p0 U (p1 U p2)
314sb-patterns=3,!(p0 U (p1 U p2))
315sb-patterns=4,GFp0 -> GFp1
316sb-patterns=5,Fp0 U Gp1
317sb-patterns=6,Gp0 U p1
318sb-patterns=7,!(Fp0 <-> Fp1)
319sb-patterns=8,!(GFp0 -> GFp1)
320sb-patterns=9,!(GFp0 <-> GFp1)
321sb-patterns=10,p0 R (p0 | p1)
322sb-patterns=11,(Xp0 U Xp1) | !X(p0 U p1)
323sb-patterns=12,(Xp0 U p1) | !X(p0 U (p0 & p1))
324sb-patterns=13,G(p0 -> Fp1) & ((Xp0 U p1) | !X(p0 U (p0 & p1)))
325sb-patterns=14,G(p0 -> Fp1) & ((Xp0 U Xp1) | !X(p0 U p1))
326sb-patterns=15,G(p0 -> Fp1)
327sb-patterns=16,!G(p0 -> X(p1 R p2))
328sb-patterns=17,!(FGp0 | FGp1)
329sb-patterns=18,G(Fp0 & Fp1)
330sb-patterns=19,Fp0 & F!p0
331sb-patterns=20,(p0 & Xp1) R X(((p2 U p3) R p0) U (p2 R p0))
332sb-patterns=21,Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0
333sb-patterns=22,Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1))
334sb-patterns=23,!(Gp2 | (G(p0 | GFp1) & G(p2 | GF!p1)) | Gp0)
335sb-patterns=24,!(Gp0 | Gp2 | (G(p0 | FGp1) & G(p2 | FG!p1)))
336sb-patterns=25,G(p0 | XGp1) & G(p2 | XG!p1)
337sb-patterns=26,G(p0 | (Xp1 & X!p1))
338sb-patterns=27,p0 | (p1 U p0)
339#+end_example
340
341Note that ~--sb-patterns=2 --sb-patterns=4 --sb-patterns=21..22~ also
342have their complement formulas listed as ~--sb-patterns=3
343--sb-patterns=8 --sb-patterns=23..24~.  So if you build the set of
344formulas output by =genltl --sb-patterns= plus their negations, it will
345contain only 46 formulas, not 54.
346
347#+BEGIN_SRC sh
348genltl --sb | ltlfilt --uniq --count
349genltl --sb --pos --neg | ltlfilt --uniq --count
350#+END_SRC
351#+RESULTS:
352: 27
353: 46
354
355#  LocalWords:  genltl num toc LTL scalable SRC sed gh pn fg FG gf qn
356#  LocalWords:  ccj Xp XXp Xq XXq rv GFp lbt utf SETUPFILE html dac
357#  LocalWords:  Dwyer et al FMSP Etessami Holzmann sb Somenzi Bloem
358#  LocalWords:  CAV LaTeX Fq Fp pNN Gp XFp XF XGp FGp XG ltlfilt uniq
359#  LocalWords:  args fxg GFa GFan GFz xn gxf hkrss liberouter Holeček
360#  LocalWords:  kr DBA nlogn quasilinear kv Xb XXb XXXb FGa GFb beem
361#  LocalWords:  Pelánek sejk GFai GFbn FGb FGbn Sikert al's tv uu pos
362