alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* doc/org/autfilt.org: Add missing text.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2016-03-09 16:19:07 +01:00
parent 81333df2c3
commit 1287525afa
1 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

14
doc/org/autfilt.org
View file

@ -720,11 +720,15 @@ $txt
rm -f example.hoa aut-ex1.hoa rm -f example.hoa aut-ex1.hoa
#+END_SRC #+END_SRC
#+BEGIN_SRC sh :results verbatim :exports code The following example checks whether the formula ~a U b U c~ accepts
ltl2tgba 'a U b U c' | autfilt --accept-word 'b; cycle{c}' -q && the word ~b; cycle{c}~.
echo "word accepted"
#+END_SRC
#+BEGIN_SRC sh :results verbatim :exports both
ltl2tgba 'a U b U c' |
autfilt --accept-word 'b; cycle{c}' -q && echo "word accepted"
#+END_SRC
#+RESULTS:
: word accepted
Here is an example where we generate an infinite stream of random LTL Here is an example where we generate an infinite stream of random LTL
formulas using [[file:randltl.org][=randltl=]], convert them all to automata using formulas using [[file:randltl.org][=randltl=]], convert them all to automata using
@ -733,7 +737,7 @@ words =a&!b;cycle{!a&!b}= and =!a&!b;cycle{a&b}= yet reject any word
of the form =cycle{b}=, and display the associated formula (which was of the form =cycle{b}=, and display the associated formula (which was
stored as the name of the automaton by =ltl2tgba=). stored as the name of the automaton by =ltl2tgba=).
#+BEGIN_SRC sh :results verbatim :export both #+BEGIN_SRC sh :results verbatim :exports both
randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- | randltl -n -1 a b | ltlfilt --simplify --uniq | ltl2tgba -F- |
autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \ autfilt --accept-word='a&!b;cycle{!a&!b}' --accept-word='!a&!b;cycle{a&b}' \
--reject-word='cycle{b}' --stats=%M -n 10 --reject-word='cycle{b}' --stats=%M -n 10