#+TITLE: =genltl=
#+EMAIL spot@lrde.epita.fr
#+OPTIONS: H:2 num:nil toc:t
#+LINK_UP: file: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 explain 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.

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

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