diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 80a2704e3..5a2e8438d 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -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<❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(⓿)> + 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
❸>] + 0 -> 1 [label=❶❸>] + 0 -> 2 [label=⓿❸>] + 1 [label="1"] + 1 -> 0 [label=❸>] + 1 -> 1 [label=⓿❸>] + 1 -> 2 [label=❷❸>] + 2 [label="2"] + 2 -> 0 [label=] + 2 -> 1 [label=⓿>] + 2 -> 2 [label=⓿>] +} +#+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(❶) & Fin(❸) & Inf(⓿)) | (Inf(❷)&Inf(❸)) | Inf(⓿)> + 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>] + 0 -> 1 [label=] + 0 -> 2 [label=] + 1 [label=<1
❶❸>] + 1 -> 0 [label=] + 1 -> 6 [label=] + 1 -> 7 [label=] + 2 [label=<2
⓿❸>] + 2 -> 3 [label=] + 2 -> 4 [label=] + 2 -> 5 [label=] + 3 [label=<3>] + 3 -> 0 [label=<1>] + 3 -> 1 [label=] + 3 -> 2 [label=] + 4 [label=<4
⓿>] + 4 -> 0 [label=] + 4 -> 6 [label=] + 4 -> 7 [label=] + 5 [label=<5
⓿>] + 5 -> 3 [label=] + 5 -> 4 [label=] + 5 -> 5 [label=] + 6 [label=<6
⓿❸>] + 6 -> 0 [label=] + 6 -> 6 [label=] + 6 -> 7 [label=] + 7 [label=<7
❷❸>] + 7 -> 3 [label=] + 7 -> 4 [label=] + 7 -> 5 [label=] +} +#+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(⓿)&Inf(❶)&Inf(❹)) | Inf(⓿) | (Inf(❷)&Inf(❸))> + 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
❸>] + 0 -> 1 [label=❸>] + 0 -> 2 [label=⓿❸>] + 1 [label="1"] + 1 -> 0 [label=❸>] + 1 -> 1 [label=⓿❸>] + 1 -> 2 [label=❷❸>] + 2 [label="2"] + 2 -> 0 [label=] + 2 -> 1 [label=⓿>] + 2 -> 2 [label=⓿>] + 2 -> 3 [label=] + 2 -> 4 [label=⓿>] + 2 -> 5 [label=⓿>] + 3 [label="3"] + 4 [label="4"] + 5 [label="5"] + 5 -> 3 [label=❶❹>] + 5 -> 4 [label=⓿❶❹>] + 5 -> 5 [label=⓿❶❹>] +} +#+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]] diff --git a/doc/org/oaut.org b/doc/org/oaut.org index 024ffdbec..085c5d721 100644 --- a/doc/org/oaut.org +++ b/doc/org/oaut.org @@ -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]] +<> 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