#+TITLE: =genltl=
#+EMAIL: spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: tools.html

This tool generates LTL formulas according to scalable patterns.
These pattern are usually taken from the literature (see the 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.

#+BEGIN_SRC sh :results verbatim :exports results
genltl --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
#+END_SRC
#+RESULTS:
#+begin_example
      --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)))
      --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)
      --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)))
#+end_example

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

#+BEGIN_SRC sh :results verbatim :exports both
genltl --and-gf=1..5 --u-left=1..5
#+END_SRC
#+RESULTS:
#+begin_example
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
#+end_example

=genltl= supports the [[file:ioltl.org][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.


#+BEGIN_SRC sh :results verbatim :exports both
genltl --and-gf=1..5 --u-left=1..5 --latex --format='%F & %L & $%f$ \\'
#+END_SRC
#+RESULTS:
#+begin_example
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}$ \\
#+end_example

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:

#+BEGIN_SRC sh :results verbatim :exports both
genltl --ccj-alpha=3
#+END_SRC
#+RESULTS:
: F(F(Fq3 & q2) & q1) & F(F(Fp3 & p2) & p1)

with

#+BEGIN_SRC sh :results verbatim :exports both
genltl --ccj-alpha=3 --lbt
#+END_SRC
#+RESULTS:
: & F & p2 F & p1 F p0 F & F & F p3 p4 p5

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

#  LocalWords:  genltl num toc LTL scalable SRC sed gh pn fg FG gf qn
#  LocalWords:  ccj Xp XXp Xq XXq rv GFp lbt