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

org: improve recurrence example

Browse source 
* doc/org/hierarchy.org: When generating DBA from recurrence formulas,
actually use -B instead of --tgba.
This commit is contained in:
Alexandre Duret-Lutz 2017-06-30 14:28:11 +02:00
parent 772404c131
commit fba3c78206
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
doc/org/hierarchy.org
View file

@ -639,9 +639,9 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot:
#+RESULTS: #+RESULTS:
[[file:hier-recurrence-6.png]] [[file:hier-recurrence-6.png]]
4. Finally, convert the resulting automaton to TGBA, using =autfilt 4. Finally, convert the resulting automaton to BA, using =autfilt
--tgba=. Spot can convert automata with any acceptance condition -B=. Spot can convert automata with any acceptance condition
to TGBA, but when the input is a deterministic state-based Rabin to BA, but when the input is a deterministic state-based Rabin
automaton, it uses a dedicated algorithm that preserves automaton, it uses a dedicated algorithm that preserves
determinism whenever possible (and we know it is possible, because determinism whenever possible (and we know it is possible, because
we are working on a recurrence formula). Adding =-D= here to we are working on a recurrence formula). Adding =-D= here to
@ -653,7 +653,7 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot:
#+BEGIN_SRC sh :results verbatim :exports code #+BEGIN_SRC sh :results verbatim :exports code
ltl2tgba -G -D 'G(Gb | Fa)' | ltl2tgba -G -D 'G(Gb | Fa)' |
autfilt -S --generalized-rabin | autfilt -S --generalized-rabin |
autfilt --tgba -D -d.a autfilt -B -D -d.a
#+END_SRC #+END_SRC
#+BEGIN_SRC dot :file hier-recurrence-7.png :cmdline -Tpng :var txt=hier-recurrence-7 :exports results #+BEGIN_SRC dot :file hier-recurrence-7.png :cmdline -Tpng :var txt=hier-recurrence-7 :exports results
$txt $txt