From ce7b9c516114dd14aeeb7d40dfe247b34680f59c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 5 Aug 2016 20:47:33 +0200
Subject: [PATCH] org: fix some automata rendering

The new ob-dot.el installed by 15ea2e66e8ff87b2ed149fe9e98ea09cca69f8d3
makes all the sed escaping useless (and actually harmful).

* doc/org/ltl2tgta.org, doc/org/oaut.org: Fix those.
---
 doc/org/ltl2tgta.org | 162 ++++++-------------------------------------
 doc/org/oaut.org     |  73 ++++++-------------
 2 files changed, 44 insertions(+), 191 deletions(-)

diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org
index a7e3d6fdb..6307db0dc 100644
--- a/doc/org/ltl2tgta.org
+++ b/doc/org/ltl2tgta.org
@@ -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
diff --git a/doc/org/oaut.org b/doc/org/oaut.org
index 6854b72dd..58d197eb4 100644
--- a/doc/org/oaut.org
+++ b/doc/org/oaut.org
@@ -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