org: adjust text for simplified example for dstar2tgba
* doc/org/dstar2tgba.org: Simplify example now that the automaton is further reduced.
This commit is contained in:
parent
2ccfba906c
commit
76517d9cd2
1 changed files with 11 additions and 29 deletions
|
|
@ -211,9 +211,7 @@ $txt
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
And now its conversion by =dstar2tgba= to a 4-state TGBA.
|
And now its conversion by =dstar2tgba= to a 1-state TGBA.
|
||||||
We don't pass any option to =dstar2tgba= because converting to TGBA is
|
|
||||||
the default:
|
|
||||||
|
|
||||||
#+NAME: gfagfb2ba
|
#+NAME: gfagfb2ba
|
||||||
#+BEGIN_SRC sh :results verbatim :exports code
|
#+BEGIN_SRC sh :results verbatim :exports code
|
||||||
|
|
@ -221,35 +219,23 @@ dstar2tgba gfagfb -d
|
||||||
#+END_SRC
|
#+END_SRC
|
||||||
#+RESULTS: gfagfb2ba
|
#+RESULTS: gfagfb2ba
|
||||||
#+begin_example
|
#+begin_example
|
||||||
digraph G {
|
digraph "" {
|
||||||
rankdir=LR
|
rankdir=LR
|
||||||
|
label=<Inf(<font color="#1F78B4">⓿</font>)&Inf(<font color="#FF4DA0">❶</font>)<br/>[gen. Büchi 2]>
|
||||||
|
labelloc="t"
|
||||||
node [shape="circle"]
|
node [shape="circle"]
|
||||||
|
node [style="filled", fillcolor="#ffffa0"]
|
||||||
fontname="Lato"
|
fontname="Lato"
|
||||||
node [fontname="Lato"]
|
node [fontname="Lato"]
|
||||||
edge [fontname="Lato"]
|
edge [fontname="Lato"]
|
||||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
node[fontsize=12] fontsize=12 stylesheet="spot.css" edge[arrowhead=vee, arrowsize=.7, fontsize=12]
|
||||||
I [label="", style=invis, width=0]
|
I [label="", style=invis, width=0]
|
||||||
I -> 0
|
I -> 0
|
||||||
0 [label="0"]
|
0 [label=<0>]
|
||||||
0 -> 0 [label=<a & b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
0 -> 0 [label=<!a & !b>]
|
||||||
0 -> 1 [label=<!a & b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
0 -> 0 [label=<!a & b<br/><font color="#FF4DA0">❶</font>>]
|
||||||
0 -> 2 [label=<a & !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
0 -> 0 [label=<a & !b<br/><font color="#1F78B4">⓿</font>>]
|
||||||
0 -> 3 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font>>]
|
0 -> 0 [label=<a & b<br/><font color="#1F78B4">⓿</font><font color="#FF4DA0">❶</font>>]
|
||||||
1 [label="1"]
|
|
||||||
1 -> 0 [label=<a & b<br/><font color="#F17CB0">❶</font>>]
|
|
||||||
1 -> 1 [label=<!a & b<br/><font color="#F17CB0">❶</font>>]
|
|
||||||
1 -> 2 [label=<a & !b<br/><font color="#F17CB0">❶</font>>]
|
|
||||||
1 -> 3 [label=<!a & !b<br/><font color="#F17CB0">❶</font>>]
|
|
||||||
2 [label="2"]
|
|
||||||
2 -> 0 [label=<a & b<br/><font color="#5DA5DA">⓿</font>>]
|
|
||||||
2 -> 1 [label=<!a & b<br/><font color="#5DA5DA">⓿</font>>]
|
|
||||||
2 -> 2 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
|
||||||
2 -> 3 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
|
||||||
3 [label="3"]
|
|
||||||
3 -> 0 [label=<a & b>]
|
|
||||||
3 -> 1 [label=<!a & b>]
|
|
||||||
3 -> 2 [label=<a & !b>]
|
|
||||||
3 -> 3 [label=<!a & !b>]
|
|
||||||
}
|
}
|
||||||
#+end_example
|
#+end_example
|
||||||
|
|
||||||
|
|
@ -259,10 +245,6 @@ $txt
|
||||||
#+RESULTS:
|
#+RESULTS:
|
||||||
[[file:gfagfb2ba.svg]]
|
[[file:gfagfb2ba.svg]]
|
||||||
|
|
||||||
Obviously the resulting automaton could be simplified further, as the
|
|
||||||
minimal TGBA for this formula has a single state. (Patches
|
|
||||||
welcome...)
|
|
||||||
|
|
||||||
* Details
|
* Details
|
||||||
|
|
||||||
** General behavior
|
** General behavior
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue