260 lines
9.5 KiB
Org Mode
260 lines
9.5 KiB
Org Mode
#+TITLE: =ltlfilt=
|
|
#+EMAIL spot@lrde.epita.fr
|
|
#+OPTIONS: H:2 num:nil toc:t
|
|
#+LINK_UP: file:tools.html
|
|
|
|
This tool is a filter for LTL formulas. (It will also work with PSL
|
|
formulas.) It can be used to perform a number of tasks. Essentially:
|
|
- converting formulas from one syntax to another,
|
|
- transforming formulas,
|
|
- selecting formulas matching some criterion.
|
|
|
|
* Changing syntaxes
|
|
|
|
Because it read and write formulas, =ltlfilt= accepts
|
|
all the [[file:ioltl.org][common input and output options]].
|
|
|
|
Additionally, if no =-f= or =-F= option is specified, =ltlfilt=
|
|
will read formulas from the standard input.
|
|
|
|
For instance the following will convert two LTL formulas expressed
|
|
using infix notation (with different names supported for the same
|
|
operators) and convert it into LBT's syntax.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
ltlfilt -l -f 'p1 U (p2 & GFp3)' -f 'X<>[]p4'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: U p1 & p2 G F p3
|
|
: X F G p4
|
|
|
|
Conversely, here is how to rewrite formulas expressed using the
|
|
LBT's Polish notation. Let's take the following four formulas
|
|
taken from examples distributed with =scheck=:
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
cat >scheck.ltl<<EOF
|
|
! | G p0 & G p1 F p3
|
|
| | X p7 F p6 & | | t p3 p7 U | f p3 p3
|
|
& U & X p0 X p4 F p1 X X U X F p5 U p0 X X p3
|
|
U p0 & | p0 p5 p1
|
|
EOF
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
|
|
These can be turned into something easier to read (to the human) with:
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt --lbt-input -F scheck.ltl
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: !(Gp0 | (Gp1 & Fp3))
|
|
: Xp7 | Fp6 | p3
|
|
: ((Xp0 & Xp4) U Fp1) & XX(XFp5 U (p0 U XXp3))
|
|
: p0 U ((p0 | p5) & p1)
|
|
|
|
* Altering the formula
|
|
|
|
As with [[file:randltl.org][=randltl=]], the =-r= option can be used to simplify formulas.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt --lbt-input -F scheck.ltl -r
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: F!p0 & (F!p1 | G!p3)
|
|
: p3 | Xp7 | Fp6
|
|
: Fp1 & XX(XFp5 U (p0 U XXp3))
|
|
: p0 U (p1 & (p0 | p5))
|
|
|
|
You may notice that operands of n-ary operators such as =&= or =|= can
|
|
be reordered by =ltlfilt= even when the formula is not changed
|
|
otherwise. This is because Spot internally order all operands of
|
|
commutative and associative operators, and that this order depends on
|
|
the order in which the subformulas are first encountered. Adding
|
|
transformation options such as =-r= may alter this order. However
|
|
this difference is semantically insignificant.
|
|
|
|
Formulas can be easily negated using the =-n= option, rewritten into
|
|
negative normal form using the =--nnf= option, and the =W= and =M=
|
|
operators can be rewritten using =U= and =R= using the =--remove-wm=
|
|
option (note that this is already done when a formula is output in
|
|
Spin's syntax).
|
|
|
|
Another way to alter formula is to rename the atomic propositions it
|
|
uses. The =--relabel=abc= will relabel all atomic propositions using
|
|
letters of the alphabet, while =--relabel=pnn= will use =p0=, =p1=,
|
|
etc. as in LBT's syntax.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt --lbt-input -F scheck.ltl -r --relabel=abc
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: F!a & (F!b | G!c)
|
|
: a | Xb | Fc
|
|
: Fa & XX(XFb U (c U XXd))
|
|
: a U (b & (a | c))
|
|
|
|
Note that the relabeling is reset between each formula: =p3= became
|
|
=c= in the first formula, but it became =d= in the third.
|
|
|
|
Another use of relabeling is to get rid of complex atomic propositions
|
|
such as the one shown when [[file:ioltl.org][presenting lenient mode]]:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt --lenient --relabel=pnn -f '(a < b) U (process[2]@ok)'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: p0 U p1
|
|
|
|
* Filtering
|
|
|
|
=ltlfilt= supports many ways to filter formulas:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports results
|
|
ltlfilt --help | sed -n '/Filtering options.*:/,/^$/p' | sed '1d;$d'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
--boolean match Boolean formulas
|
|
--bsize-max=INT match formulas with Boolean size <= INT
|
|
--bsize-min=INT match formulas with Boolean size >= INT
|
|
--equivalent-to=FORMULA match formulas equivalent to FORMULA
|
|
--eventual match pure eventualities
|
|
--guarantee match guarantee formulas (even pathological)
|
|
--implied-by=FORMULA match formulas implied by FORMULA
|
|
--imply=FORMULA match formulas implying FORMULA
|
|
--ltl match only LTL formulas (no PSL operator)
|
|
--nox match X-free formulas
|
|
--obligation match obligation formulas (even pathological)
|
|
--safety match safety formulas (even pathological)
|
|
--size-max=INT match formulas with size <= INT
|
|
--size-min=INT match formulas with size >= INT
|
|
--stutter-insensitive, --stutter-invariant
|
|
match stutter-insensitive LTL formulas
|
|
--syntactic-guarantee match syntactic-guarantee formulas
|
|
--syntactic-obligation match syntactic-obligation formulas
|
|
--syntactic-persistence match syntactic-persistence formulas
|
|
--syntactic-recurrence match syntactic-recurrence formulas
|
|
--syntactic-safety match syntactic-safety formulas
|
|
--universal match purely universal formulas
|
|
-u, --unique drop formulas that have already been output (not
|
|
affected by -v)
|
|
-v, --invert-match select non-matching formulas
|
|
#+end_example
|
|
|
|
Most of the above options should be self-explanatory. For instance
|
|
the following command will extract all formulas from =scheck.ltl=
|
|
which do not represent guarantee properties.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt --lbt-input -F scheck.ltl -v --guarantee
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: !(Gp0 | (Gp1 & Fp3))
|
|
|
|
Combining =ltlfilt= with [[file:randltl.org][=randltl=]] makes it easier to generate random
|
|
formulas that respect certain constraints. For instance let us
|
|
generate 10 formulas that are equivalent to =a U b=:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
randltl -n -1 a b | ltlfilt --equivalent-to 'a U b' | head -n 10
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
!(!a R !b)
|
|
(!Gb -> a) U b
|
|
a U b
|
|
Fb & (a W b)
|
|
((a <-> !(a | b)) W a) U ((!b M b) U b)
|
|
(b <-> (Xb M a)) -> b
|
|
(a | b) U b
|
|
((!b U b) -> (a W b)) U b
|
|
(a xor b) U b
|
|
b R (Fb & (a U (a W b)))
|
|
#+end_example
|
|
|
|
The =-n -1= option to =randltl= will cause it to output an infinite
|
|
stream of random formulas. =ltlfilt=, which reads its standard input
|
|
by default, will select only those equivalent to =a U b=. The output
|
|
of =ltlfilt= would still be an infinite stream of random formulas, so
|
|
we display only the first 10 using the standard =head= utility. Less
|
|
trivial formulas could be obtained by adding the =-r= option to
|
|
=randltl= (or equivalently adding the =-r= and =-u= option to
|
|
=ltlfilt=).
|
|
|
|
|
|
Another similar example, that requires two calls to =ltlfilt=, is the
|
|
generation of random pathological safety formulas. Pathological
|
|
safety formulas are safety formulas that do not /look/ so
|
|
syntactically. We can generate some starting again with =randltl=,
|
|
then ignoring all syntactic safety formulas, and keeping only the
|
|
safety formulas in the remaining list.
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
randltl -r -n -1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety | head -n 10
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
#+begin_example
|
|
(!a & Fa) R Xa
|
|
!a | (a & b) | (((!a & b) | (a & !b)) M (!a M X!a))
|
|
G(!a M Xa)
|
|
G((G!b & !a) | (a & Fb)) R a
|
|
G!a M !a
|
|
G(!a M ((!b & XGb) | (b & XF!b)))
|
|
F(b | G!b)
|
|
F(Xa | G!a)
|
|
G(XXa | (b & F!a))
|
|
G((!a & (!a M !b)) | (a & (a W b)))
|
|
#+end_example
|
|
|
|
|
|
=ltlfilt='s filtering ability can also be used to answer questions
|
|
about a single formula. For instance is =a U (b U a)= equivalent to
|
|
=b U a=?
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt -f 'a U (b U a)' --equivalent-to 'b U a'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: a U (b U a)
|
|
|
|
The command prints the formula and returns an exit status of 0 if the
|
|
two formulas are equivalent. It would print nothing and set the exit
|
|
status to 1, were the two formulas not equivalent.
|
|
|
|
|
|
If the formula =F(a & X(!a & Gb))= stutter-invariant?
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt -f 'F(a & X(!a & Gb))' --stutter-invariant
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: F(a & X(!a & Gb))
|
|
|
|
Yes it is. And since it is stutter-invariant, there exist some
|
|
equivalent formulas that do not use =X= operator. The =--remove-x=
|
|
option gives one:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt -f 'F(a & X(!a & Gb))' --remove-x
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & Gb & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b))))
|
|
|
|
We could even verify that the resulting horrible formula is equivalent
|
|
to the original one:
|
|
|
|
#+BEGIN_SRC sh :results verbatim :exports both
|
|
ltlfilt -f 'F(a & X(!a & Gb))' --remove-x | ltlfilt --equivalent-to 'F(a & X(!a & Gb))'
|
|
#+END_SRC
|
|
#+RESULTS:
|
|
: F(a & ((a & (a U (!a & Gb)) & ((!b U !a) | (b U !a))) | (!a & (!a U (a & !a & Gb)) & ((!b U a) | (b U a))) | (b & (b U (!a & Gb & !b)) & ((!a U !b) | (a U !b))) | (!b & (!b U (!a & b & Gb)) & ((!a U b) | (a U b))) | (!a & Gb & (G!a | Ga) & (Gb | G!b))))
|
|
|
|
It is therefore equivalent, but that is not a surprise since the
|
|
=--stutter-invariant= filter is actually implemented using exactly
|
|
[[http://homepages.inf.ed.ac.uk/kousha/note_on_stut_tl_lpi.ps][this procedure]] (calling the =remove_x()= function, and checking the
|
|
equivalence of the resulting formula with the original one).
|
|
|
|
|
|
# LocalWords: ltlfilt num toc LTL PSL syntaxes LBT's SRC GFp scheck
|
|
# LocalWords: ltl EOF lbt Gp Fp Xp XFp XXp randltl ary nnf wm abc
|
|
# LocalWords: pnn Xb Fc XFb XXd sed boolean bsize nox Gb Fb Xa XGb
|
|
# LocalWords: XF XXa
|