org: fix some automata rendering
The new ob-dot.el installed by 15ea2e66e8
makes all the sed escaping useless (and actually harmful).
* doc/org/ltl2tgta.org, doc/org/oaut.org: Fix those.
This commit is contained in:
Alexandre Duret-Lutz
parent
06d5aa5ea2
commit
ce7b9c5161
2 changed files with 44 additions and 191 deletions
|
|
@ -17,61 +17,37 @@ described by [[http://spinroot.com/spin/Workshops/ws06/039.pdf][Geldenhuys and H
|
|||
Here is the output on =a U Gb= (we omit the call to =dot=, as shown while
|
||||
discussing [[file:ltl2tgba.org][=ltl2tgba=]]).
|
||||
|
||||
#+NAME: augb-ta
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgta --ta --multiple-init 'a U Gb'
|
||||
#+END_SRC
|
||||
#+RESULTS:
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
|
||||
-1 [label="", style=invis, height=0]
|
||||
-1 -> 1 [label="a & b"]
|
||||
-2 [label="", style=invis, height=0]
|
||||
-2 -> 2 [label="a & !b"]
|
||||
-3 [label="", style=invis, height=0]
|
||||
-3 -> 3 [label="!a & b"]
|
||||
1 [label="2\na & b",shape=box]
|
||||
1 -> 4 [label="{a}\n"]
|
||||
1 -> 3 [label="{a}\n"]
|
||||
1 -> 2 [label="{b}\n"]
|
||||
2 [label="1\na & !b"]
|
||||
2 -> 1 [label="{b}\n"]
|
||||
2 -> 3 [label="{a, b}\n"]
|
||||
3 [label="0\n!a & b",shape=box]
|
||||
3 -> 4 [label="{a}\n"]
|
||||
4 [label="3",peripheries=2,shape=box]
|
||||
4 -> 4 [label="{a}\n{0}"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+NAME: augb-ta
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
ltl2tgta --ta --multiple-init 'a U Gb' | sed 's/\\/\\\\/'
|
||||
#+END_SRC
|
||||
#+RESULTS: augb-ta
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [style="filled", fillcolor="#ffffa0"]
|
||||
fontname="Lato"
|
||||
node [fontname="Lato"]
|
||||
edge [fontname="Lato"]
|
||||
edge[arrowhead=vee, arrowsize=.7]
|
||||
-1 [label="", style=invis, height=0]
|
||||
-1 -> 1 [label="!a & b"]
|
||||
-2 [label="", style=invis, height=0]
|
||||
-2 -> 2 [label="a & b"]
|
||||
-2 -> 2 [label="a & !b"]
|
||||
-3 [label="", style=invis, height=0]
|
||||
-3 -> 3 [label="a & !b"]
|
||||
1 [label="2\\n!a & b",shape=box]
|
||||
1 -> 4 [label="{a}\\n"]
|
||||
2 [label="1\\na & b",shape=box]
|
||||
2 -> 4 [label="{a}\\n"]
|
||||
2 -> 1 [label="{a}\\n"]
|
||||
2 -> 3 [label="{b}\\n"]
|
||||
3 [label="0\\na & !b"]
|
||||
3 -> 2 [label="{b}\\n"]
|
||||
3 -> 1 [label="{a, b}\\n"]
|
||||
-3 -> 3 [label="a & b"]
|
||||
1 [label="2\n!a & b",shape=box]
|
||||
1 -> 4 [label="{a}\n"]
|
||||
2 [label="1\na & !b"]
|
||||
2 -> 3 [label="{b}\n"]
|
||||
2 -> 1 [label="{a, b}\n"]
|
||||
3 [label="0\na & b",shape=box]
|
||||
3 -> 4 [label="{a}\n"]
|
||||
3 -> 1 [label="{a}\n"]
|
||||
3 -> 2 [label="{b}\n"]
|
||||
4 [label="3",peripheries=2,shape=box]
|
||||
4 -> 4 [label="{a}\\n{0}"]
|
||||
4 -> 4 [label="{a}\n{0}"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
|
|
@ -101,6 +77,7 @@ one of these state is accepting.
|
|||
Without the =--multiple-init= option, a fake initial state is added.
|
||||
This is the default since it often makes the result more readable.
|
||||
|
||||
#+NAME: augb-ta2
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgta --ta 'a U Gb'
|
||||
#+END_SRC
|
||||
|
|
@ -127,33 +104,6 @@ digraph G {
|
|||
}
|
||||
#+end_example
|
||||
|
||||
#+NAME: augb-ta2
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
ltl2tgta --ta 'a U Gb' | sed 's/\\/\\\\/'
|
||||
#+END_SRC
|
||||
#+RESULTS: augb-ta2
|
||||
#+begin_example
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label=init]
|
||||
1 -> 2 [label="!a & b\\n"]
|
||||
1 -> 3 [label="a & b\\n"]
|
||||
1 -> 4 [label="a & !b\\n"]
|
||||
2 [label="2",shape=box]
|
||||
2 -> 5 [label="{a}\\n"]
|
||||
3 [label="3",shape=box]
|
||||
3 -> 5 [label="{a}\\n"]
|
||||
3 -> 2 [label="{a}\\n"]
|
||||
3 -> 4 [label="{b}\\n"]
|
||||
4 [label="1"]
|
||||
4 -> 3 [label="{b}\\n"]
|
||||
4 -> 2 [label="{a, b}\\n"]
|
||||
5 [label="4",peripheries=2,shape=box]
|
||||
5 -> 5 [label="{a}\\n{0}"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file augb-ta2.png :cmdline -Tpng :var txt=augb-ta2 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -166,6 +116,7 @@ acceptance. In that case double-enclosures are not used anymore, and
|
|||
Büchi accepting transitions are marked with the same ={0,1}=
|
||||
notation used in TGBA.
|
||||
|
||||
#+NAME: gfagfb-gta
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgta --gta 'GFa & GFb'
|
||||
#+END_SRC
|
||||
|
|
@ -198,39 +149,6 @@ digraph G {
|
|||
}
|
||||
#+end_example
|
||||
|
||||
#+NAME: gfagfb-gta
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
ltl2tgta --gta 'GFa & GFb' | sed 's/\\/\\\\/'
|
||||
#+END_SRC
|
||||
#+RESULTS: gfagfb-gta
|
||||
#+begin_example
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label=init]
|
||||
1 -> 2 [label="a & b\\n"]
|
||||
1 -> 3 [label="!a & b\\n"]
|
||||
1 -> 4 [label="a & !b\\n"]
|
||||
1 -> 5 [label="!a & !b\\n"]
|
||||
2 [label="1",shape=box]
|
||||
2 -> 3 [label="{a}\\n{0,1}"]
|
||||
2 -> 4 [label="{b}\\n{0,1}"]
|
||||
2 -> 5 [label="{a, b}\\n{0,1}"]
|
||||
3 [label="3"]
|
||||
3 -> 2 [label="{a}\\n{1}"]
|
||||
3 -> 4 [label="{a, b}\\n{1}"]
|
||||
3 -> 5 [label="{b}\\n{1}"]
|
||||
4 [label="2"]
|
||||
4 -> 2 [label="{b}\\n{0}"]
|
||||
4 -> 3 [label="{a, b}\\n{0}"]
|
||||
4 -> 5 [label="{a}\\n{0}"]
|
||||
5 [label="4"]
|
||||
5 -> 2 [label="{a, b}\\n"]
|
||||
5 -> 3 [label="{b}\\n"]
|
||||
5 -> 4 [label="{a}\\n"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file gfagfb-gta.png :cmdline -Tpng :var txt=gfagfb-gta :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -248,6 +166,7 @@ Testing Automaton [fn:topnoc]. In TGTAs, the stuttering states are
|
|||
made explicit with ={}= self-loops. Since these self-loop can be in
|
||||
acceptance sets, livelock acceptance states are no longer needed.
|
||||
|
||||
#+NAME: gfagfb-tgta
|
||||
#+BEGIN_SRC sh :results verbatim :exports code
|
||||
ltl2tgta 'GFa & GFb'
|
||||
#+END_SRC
|
||||
|
|
@ -284,43 +203,6 @@ digraph G {
|
|||
}
|
||||
#+end_example
|
||||
|
||||
#+NAME: gfagfb-tgta
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
ltl2tgta 'GFa & GFb' | sed 's/\\/\\\\/'
|
||||
#+END_SRC
|
||||
#+RESULTS: gfagfb-tgta
|
||||
#+begin_example
|
||||
digraph G {
|
||||
0 [label="", style=invis, height=0]
|
||||
0 -> 1
|
||||
1 [label=init]
|
||||
1 -> 2 [label="a & b\\n"]
|
||||
1 -> 3 [label="!a & b\\n"]
|
||||
1 -> 4 [label="a & !b\\n"]
|
||||
1 -> 5 [label="!a & !b\\n"]
|
||||
2 [label="3"]
|
||||
2 -> 3 [label="{a}\\n{0,1}"]
|
||||
2 -> 4 [label="{b}\\n{0,1}"]
|
||||
2 -> 5 [label="{a, b}\\n{0,1}"]
|
||||
2 -> 2 [label="{}\\n{0,1}"]
|
||||
3 [label="2"]
|
||||
3 -> 2 [label="{a}\\n{1}"]
|
||||
3 -> 4 [label="{a, b}\\n{1}"]
|
||||
3 -> 5 [label="{b}\\n{1}"]
|
||||
3 -> 3 [label="{}\\n"]
|
||||
4 [label="4"]
|
||||
4 -> 2 [label="{b}\\n{0}"]
|
||||
4 -> 3 [label="{a, b}\\n{0}"]
|
||||
4 -> 5 [label="{a}\\n{0}"]
|
||||
4 -> 4 [label="{}\\n"]
|
||||
5 [label="1"]
|
||||
5 -> 2 [label="{a, b}\\n"]
|
||||
5 -> 3 [label="{b}\\n"]
|
||||
5 -> 4 [label="{a}\\n"]
|
||||
5 -> 5 [label="{}\\n"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file gfagfb-tgta.png :cmdline -Tpng :var txt=gfagfb-tgta :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
|
|||
|
|
@ -547,14 +547,16 @@ format.
|
|||
ltl2tgba '(Ga -> Gb) W c' -d
|
||||
#+END_SRC
|
||||
|
||||
#+NAME: oaut-dot1
|
||||
#+BEGIN_SRC sh :results verbatim :exports results
|
||||
SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot=
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS:
|
||||
#+RESULTS: oaut-dot1
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 1
|
||||
0 [label="0"]
|
||||
|
|
@ -580,37 +582,6 @@ digraph G {
|
|||
This output should be processed with =dot= to be converted into a
|
||||
picture. For instance use =dot -Tpng= or =dot -Tpdf=.
|
||||
|
||||
#+NAME: oaut-dot1
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
SPOT_DOTEXTRA= ltl2tgba '(Ga -> Gb) W c' --dot= | sed 's/\\/\\\\/'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: oaut-dot1
|
||||
#+begin_example
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 1
|
||||
0 [label="0"]
|
||||
0 -> 0 [label="b\\n{0}"]
|
||||
1 [label="1"]
|
||||
1 -> 0 [label="a & b & !c"]
|
||||
1 -> 1 [label="!a & !c\\n{0}"]
|
||||
1 -> 2 [label="a & !c"]
|
||||
1 -> 3 [label="c"]
|
||||
2 [label="2"]
|
||||
2 -> 1 [label="!a & !c\\n{0}"]
|
||||
2 -> 2 [label="a & !c"]
|
||||
2 -> 3 [label="!a & c"]
|
||||
2 -> 4 [label="a & c"]
|
||||
3 [label="3"]
|
||||
3 -> 3 [label="1\\n{0}"]
|
||||
4 [label="4"]
|
||||
4 -> 3 [label="!a"]
|
||||
4 -> 4 [label="a"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
#+BEGIN_SRC dot :file oaut-dot1.png :cmdline -Tpng :var txt=oaut-dot1 :exports results
|
||||
$txt
|
||||
#+END_SRC
|
||||
|
|
@ -683,13 +654,13 @@ digraph G {
|
|||
|
||||
#+NAME: oaut-dot2
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c' | sed 's/\\/\\\\/'
|
||||
SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
|
||||
#+END_SRC
|
||||
|
||||
#+RESULTS: oaut-dot2
|
||||
#+begin_example
|
||||
digraph G {
|
||||
label="(Gb | F!a) W c\\nInf(0)"
|
||||
label="(Gb | F!a) W c\nInf(0)"
|
||||
labelloc="t"
|
||||
node [shape="circle"]
|
||||
I [label="", style=invis, height=0]
|
||||
|
|
@ -715,16 +686,16 @@ digraph G {
|
|||
1 [label="1"]
|
||||
2 [label="2"]
|
||||
}
|
||||
0 -> 0 [label="b\\n{0}"]
|
||||
0 -> 0 [label="b\n{0}"]
|
||||
1 -> 0 [label="a & b & !c"]
|
||||
1 -> 1 [label="!a & !c\\n{0}"]
|
||||
1 -> 1 [label="!a & !c\n{0}"]
|
||||
1 -> 2 [label="a & !c"]
|
||||
1 -> 3 [label="c"]
|
||||
2 -> 1 [label="!a & !c\\n{0}"]
|
||||
2 -> 1 [label="!a & !c\n{0}"]
|
||||
2 -> 2 [label="a & !c"]
|
||||
2 -> 3 [label="!a & c"]
|
||||
2 -> 4 [label="a & c"]
|
||||
3 -> 3 [label="1\\n{0}"]
|
||||
3 -> 3 [label="1\n{0}"]
|
||||
4 -> 3 [label="!a"]
|
||||
4 -> 4 [label="a"]
|
||||
}
|
||||
|
|
@ -751,7 +722,7 @@ Here is an example involving all colors:
|
|||
|
||||
#+NAME: oaut-dot3
|
||||
#+BEGIN_SRC sh :results verbatim :exports none
|
||||
SPOT_DOTEXTRA= autfilt --dot=cas <<EOF | sed 's/\\/\\\\/'
|
||||
SPOT_DOTEXTRA= autfilt --dot=cas <<EOF
|
||||
HOA: v1
|
||||
States: 10
|
||||
Start: 1
|
||||
|
|
@ -839,25 +810,25 @@ digraph G {
|
|||
1 [label="1"]
|
||||
3 [label="3"]
|
||||
}
|
||||
0 -> 0 [label="a & b\\n{0,1,2}"]
|
||||
0 -> 0 [label="!a & !b\\n{2}"]
|
||||
0 -> 5 [label="a\\n{2}"]
|
||||
0 -> 0 [label="a & b\n{0,1,2}"]
|
||||
0 -> 0 [label="!a & !b\n{2}"]
|
||||
0 -> 5 [label="a\n{2}"]
|
||||
1 -> 4 [label="b"]
|
||||
1 -> 3 [label="a & !b"]
|
||||
2 -> 0 [label="a"]
|
||||
2 -> 7 [label="b"]
|
||||
3 -> 1 [label="a & b\\n{0,1}"]
|
||||
4 -> 4 [label="!b\\n{1,2}"]
|
||||
3 -> 1 [label="a & b\n{0,1}"]
|
||||
4 -> 4 [label="!b\n{1,2}"]
|
||||
4 -> 2 [label="b"]
|
||||
5 -> 6 [label="1\\n{1}"]
|
||||
5 -> 6 [label="1\n{1}"]
|
||||
6 -> 5 [label="1"]
|
||||
7 -> 7 [label="!a & b\\n{0,2}"]
|
||||
7 -> 7 [label="a & b\\n{0,1}"]
|
||||
7 -> 7 [label="!a & b\n{0,2}"]
|
||||
7 -> 7 [label="a & b\n{0,1}"]
|
||||
7 -> 8 [label="1"]
|
||||
8 -> 8 [label="!a & b\\n{0,2}"]
|
||||
8 -> 9 [label="a & b\\n{0,1}"]
|
||||
9 -> 8 [label="!a & b\\n{0,1}"]
|
||||
9 -> 9 [label="a & b\\n{0,2}"]
|
||||
8 -> 8 [label="!a & b\n{0,2}"]
|
||||
8 -> 9 [label="a & b\n{0,1}"]
|
||||
9 -> 8 [label="!a & b\n{0,1}"]
|
||||
9 -> 9 [label="a & b\n{0,2}"]
|
||||
}
|
||||
#+end_example
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue