org: more examples for autfilt
* doc/org/oaut.org: Some typos. * doc/org/autfilt.org: Add some examples.
This commit is contained in:
Alexandre Duret-Lutz
parent
ead2ca0158
commit
b4e22a3c7e
2 changed files with 192 additions and 3 deletions
|
|
@ -260,3 +260,191 @@ autfilt --help | sed -n '/Transformations:/,/^$/p' | sed '1d;$d'
|
|||
--strip-acceptance remove the acceptance condition and all acceptance
|
||||
sets
|
||||
#+end_example
|
||||
|
||||
* Examples
|
||||
|
||||
Here is an automaton with transition-based acceptance:
|
||||
|
||||
#+BEGIN_SRC sh :result verbatim :export code
|
||||
cat >aut-ex1.hoa<<EOF
|
||||
HOA: v1
|
||||
States: 3
|
||||
Start: 0
|
||||
AP: 2 "a" "b"
|
||||
acc-name: Buchi
|
||||
Acceptance: 4 Inf(0)&Fin(1)&Fin(3) | Inf(2)&Inf(3) | Inf(0)
|
||||
--BODY--
|
||||
State: 0 {3}
|
||||
[t] 0
|
||||
[0] 1 {1}
|
||||
[!0] 2 {0}
|
||||
State: 1 {3}
|
||||
[1] 0
|
||||
[0&1] 1 {0}
|
||||
[!0&1] 2 {2}
|
||||
State: 2
|
||||
[!1] 0
|
||||
[0&!1] 1 {0}
|
||||
[!0&!1] 2 {0}
|
||||
--END--
|
||||
EOF
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
|
||||
(Note: the '=.=' argument passed to =--dot= below hides default
|
||||
options discussed [[file:oaut.org::#default-dot][on another page]], while the '=a=' causes the
|
||||
acceptance condition to be displayed.)
|
||||
|
||||
#+NAME: autfilt-ex1
|
||||
#+BEGIN_SRC sh :results verbatim :export code
|
||||
autfilt aut-ex1.hoa --dot=.a
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: autfilt-ex1
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<(Fin(<font color="#F17CB0">❶</font>) & Fin(<font color="#B276B2">❸</font>) & Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#5DA5DA">⓿</font>)>
|
||||
labelloc="t"
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label=<1<br/><font color="#B276B2">❸</font>>]
|
||||
0 -> 1 [label=<a<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
|
||||
0 -> 2 [label=<!a<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<b<br/><font color="#B276B2">❸</font>>]
|
||||
1 -> 1 [label=<a & b<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
1 -> 2 [label=<!a & b<br/><font color="#FAA43A">❷</font><font color="#B276B2">❸</font>>]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label=<!b>]
|
||||
2 -> 1 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 -> 2 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfilt-ex1.png :cmdline -Tpng :var txt=autfilt-ex1 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
[[file:autfilt-ex1.png]]
|
||||
|
||||
Using =--sba= will "push" the acceptance membership of the transitions to the states:
|
||||
|
||||
#+NAME: autfilt-ex2
|
||||
#+BEGIN_SRC sh :results verbatim :export code
|
||||
autfilt --sba aut-ex1.hoa --dot=.a
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: autfilt-ex2
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<(Fin(<font color="#F17CB0">❶</font>) & Fin(<font color="#B276B2">❸</font>) & Inf(<font color="#5DA5DA">⓿</font>)) | (Inf(<font color="#FAA43A">❷</font>)&Inf(<font color="#B276B2">❸</font>)) | Inf(<font color="#5DA5DA">⓿</font>)>
|
||||
labelloc="t"
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label=<0<br/><font color="#B276B2">❸</font>>]
|
||||
0 -> 0 [label=<1>]
|
||||
0 -> 1 [label=<a>]
|
||||
0 -> 2 [label=<!a>]
|
||||
1 [label=<1<br/><font color="#F17CB0">❶</font><font color="#B276B2">❸</font>>]
|
||||
1 -> 0 [label=<b>]
|
||||
1 -> 6 [label=<a & b>]
|
||||
1 -> 7 [label=<!a & b>]
|
||||
2 [label=<2<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
2 -> 3 [label=<!b>]
|
||||
2 -> 4 [label=<a & !b>]
|
||||
2 -> 5 [label=<!a & !b>]
|
||||
3 [label=<3>]
|
||||
3 -> 0 [label=<1>]
|
||||
3 -> 1 [label=<a>]
|
||||
3 -> 2 [label=<!a>]
|
||||
4 [label=<4<br/><font color="#5DA5DA">⓿</font>>]
|
||||
4 -> 0 [label=<b>]
|
||||
4 -> 6 [label=<a & b>]
|
||||
4 -> 7 [label=<!a & b>]
|
||||
5 [label=<5<br/><font color="#5DA5DA">⓿</font>>]
|
||||
5 -> 3 [label=<!b>]
|
||||
5 -> 4 [label=<a & !b>]
|
||||
5 -> 5 [label=<!a & !b>]
|
||||
6 [label=<6<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
6 -> 0 [label=<b>]
|
||||
6 -> 6 [label=<a & b>]
|
||||
6 -> 7 [label=<!a & b>]
|
||||
7 [label=<7<br/><font color="#FAA43A">❷</font><font color="#B276B2">❸</font>>]
|
||||
7 -> 3 [label=<!b>]
|
||||
7 -> 4 [label=<a & !b>]
|
||||
7 -> 5 [label=<!a & !b>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfilt-ex2.png :cmdline -Tpng :var txt=autfilt-ex2 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
[[file:autfilt-ex2.png]]
|
||||
|
||||
|
||||
Using =--remove-fin= will transform the automaton to remove all traces
|
||||
of Fin-acceptance: this usually requires adding non-deterministic jumps to
|
||||
altered copies of strongly-connected components.
|
||||
|
||||
#+NAME: autfilt-ex3
|
||||
#+BEGIN_SRC sh :results verbatim :export code
|
||||
autfilt --remove-fin aut-ex1.hoa --dot=.a
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: autfilt-ex3
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
label=<(Inf(<font color="#5DA5DA">⓿</font>)&Inf(<font color="#F17CB0">❶</font>)&Inf(<font color="#60BD68">❹</font>)) | Inf(<font color="#5DA5DA">⓿</font>) | (Inf(<font color="#FAA43A">❷</font>)&Inf(<font color="#B276B2">❸</font>))>
|
||||
labelloc="t"
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label=<1<br/><font color="#B276B2">❸</font>>]
|
||||
0 -> 1 [label=<a<br/><font color="#B276B2">❸</font>>]
|
||||
0 -> 2 [label=<!a<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label=<b<br/><font color="#B276B2">❸</font>>]
|
||||
1 -> 1 [label=<a & b<br/><font color="#5DA5DA">⓿</font><font color="#B276B2">❸</font>>]
|
||||
1 -> 2 [label=<!a & b<br/><font color="#FAA43A">❷</font><font color="#B276B2">❸</font>>]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label=<!b>]
|
||||
2 -> 1 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 -> 2 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 -> 3 [label=<!b>]
|
||||
2 -> 4 [label=<a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
2 -> 5 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font>>]
|
||||
3 [label="3"]
|
||||
4 [label="4"]
|
||||
5 [label="5"]
|
||||
5 -> 3 [label=<!b<br/><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
|
||||
5 -> 4 [label=<a & !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
|
||||
5 -> 5 [label=<!a & !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file autfilt-ex3.png :cmdline -Tpng :var txt=autfilt-ex3 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
[[file:autfilt-ex3.png]]
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
y# -*- coding: utf-8 -*-
|
||||
# -*- coding: utf-8 -*-
|
||||
#+TITLE: Common output options for automata
|
||||
#+SETUPFILE: setup.org
|
||||
#+HTML_LINK_UP: tools.html
|
||||
|
|
@ -561,7 +561,7 @@ be ouput as bullets (e.g., ⓿ instead of ={0}=); option =r= (for
|
|||
rainbow) causes sets to be displayed in different colors, while option
|
||||
=R= also uses colors, but it chooses them depending on whether a set
|
||||
is used with Fin-acceptance, Inf-acceptance, or both. Finally option
|
||||
=f(FONT)= is used to select a fontname: is is often necessary when =b=
|
||||
=f(FONT)= is used to select a fontname: it is often necessary when =b=
|
||||
is used to ensure the characters ⓿, ❶, etc. are all selected from the
|
||||
same font.
|
||||
|
||||
|
|
@ -801,6 +801,7 @@ $txt
|
|||
#+RESULTS:
|
||||
[[file:oaut-dot3.png]]
|
||||
|
||||
<<default-dot>>
|
||||
|
||||
The dot output can also be customized via two environment variables:
|
||||
- =SPOT_DOTDEFAULT= contains default arguments for the =--dot= option
|
||||
|
|
@ -823,7 +824,7 @@ The dot output can also be customized via two environment variables:
|
|||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
export SPOT_DOTDEFAULT='brf(Lato)'
|
||||
export SPOT_DOTEXTRA='node[style=filled, fillcolor="#ffffa0"]'
|
||||
#+END
|
||||
#+END_SRC
|
||||
|
||||
* Statistics
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue