diff --git a/.gitignore b/.gitignore
index 2d2676ed4..92e041696 100644
--- a/.gitignore
+++ b/.gitignore
@@ -69,6 +69,7 @@ dt*a-sat.dbg
 *.dstar
 *.satlog
 *.png
+*.svg
 GPATH
 GRTAGS
 GSYMS
diff --git a/HACKING b/HACKING
index 9dae74a74..e40590478 100644
--- a/HACKING
+++ b/HACKING
@@ -39,6 +39,7 @@ since the generated files they produce are distributed.)
   GraphViz
   Java >= 1.7 (needed to run PlantUML while generating the doc)
   wget or curl (needed to download PlantUML)
+  pdf2svg
 
 The following additional tools are used if they are present, or
 only for certain operations (like releases):
diff --git a/doc/Makefile.am b/doc/Makefile.am
index 4502787b1..a1297a6f3 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -77,7 +77,7 @@ ORG_FILES = \
   org/init.el.in \
   org/spot.css \
   org/arch.tex \
-  $(srcdir)/org/arch.png \
+  $(srcdir)/org/arch.svg \
   org/autcross.org \
   org/autfilt.org \
   org/csv.org \
@@ -90,7 +90,7 @@ ORG_FILES = \
   org/hoa.org \
   org/hierarchy.org \
   org/hierarchy.tex \
-  $(srcdir)/org/hierarchy.png \
+  $(srcdir)/org/hierarchy.svg \
   org/index.org \
   org/install.org \
   org/ioltl.org \
@@ -125,21 +125,24 @@ ORG_FILES = \
   org/satmin.org \
   org/satmin.tex \
   org/setup.org \
-  $(srcdir)/org/satmin.png
+  $(srcdir)/org/satmin.svg
 
-$(srcdir)/org/satmin.png: org/satmin.tex
+$(srcdir)/org/satmin.svg: org/satmin.tex
 	cd $(srcdir)/org && \
-	pdflatex -shell-escape satmin.tex && \
+	pdflatex satmin.tex && \
+	pdf2svg satmin.pdf satmin.svg && \
 	rm -f satmin.pdf satmin.aux satmin.log
 
-$(srcdir)/org/arch.png: org/arch.tex
+$(srcdir)/org/arch.svg: org/arch.tex
 	cd $(srcdir)/org && \
-	pdflatex -shell-escape arch.tex && \
+	pdflatex arch.tex && \
+	pdf2svg arch.pdf arch.svg && \
 	rm -f arch.pdf arch.aux arch.log
 
-$(srcdir)/org/hierarchy.png: org/hierarchy.tex
+$(srcdir)/org/hierarchy.svg: org/hierarchy.tex
 	cd $(srcdir)/org && \
-	pdflatex -shell-escape hierarchy.tex && \
+	pdflatex hierarchy.tex && \
+	pdf2svg hierarchy.pdf hierarchy.svg && \
 	rm -f hierarchy.pdf hierarchy.aux hierarchy.log
 
 $(srcdir)/org-stamp: $(ORG_FILES) $(configure_ac)
diff --git a/doc/org/.dir-locals.el.in b/doc/org/.dir-locals.el.in
index 62d969e67..4b1f6327c 100644
--- a/doc/org/.dir-locals.el.in
+++ b/doc/org/.dir-locals.el.in
@@ -23,7 +23,7 @@
 			      (concat "@abs_top_builddir@/python/.libs:@abs_top_builddir@/spot/.libs:@abs_top_builddir@/buddy/src/.libs:"
 				      (getenv "DYLD_LIBRARY_PATH")))
 		      (setenv "SPOT_DOTDEFAULT" "Brf(Lato)C(#ffffa0)")
-		      (setenv "SPOT_DOTEXTRA" "edge[arrowhead=vee, arrowsize=.7]")
+		      (setenv "SPOT_DOTEXTRA" "node[fontsize=12] fontsize=12 stylesheet=\"spot.css\" edge[arrowhead=vee, arrowsize=.7, fontsize=12]")
                       (setq org-babel-temporary-directory "@abs_top_builddir@/doc/org/tmp")
                       (make-directory org-babel-temporary-directory t)
 		      (org-babel-do-load-languages 'org-babel-load-languages
@@ -62,7 +62,7 @@
 		   :auto-preamble t)
 		  ("spot-static"
 		   :base-directory "."
-		   :base-extension "css\\|js\\|png\\|jpg\\|gif\\|pdf"
+		   :base-extension "css\\|js\\|png\\|svg\\|jpg\\|gif\\|pdf"
 		   :publishing-directory "../userdoc/"
 		   :recursive t
 		   :publishing-function org-publish-attachment)
diff --git a/doc/org/arch.tex b/doc/org/arch.tex
index 90306b998..4c346efbd 100644
--- a/doc/org/arch.tex
+++ b/doc/org/arch.tex
@@ -1,4 +1,4 @@
-\documentclass[convert={size=640}]{standalone}
+\documentclass{standalone}
 \usepackage{tikz}
 \usetikzlibrary{arrows}
 \usetikzlibrary{arrows.meta}
@@ -9,6 +9,7 @@
 
 \begin{document}
 
+\scalebox{1.2}{
 \begin{tikzpicture}
   \tikzset{node distance=2mm,
            basicbox/.style={minimum width=#1,minimum height=8mm},
@@ -81,7 +82,7 @@
 ($(libspot.south east)+(1mm,-1mm)$) --
 ($(libspot.south west)+(-1mm,-1mm)$) -- cycle;
 \end{pgfonlayer}
-\end{tikzpicture}
+\end{tikzpicture}}
 \end{document}
 %%% Local Variables:
 %%% mode: latex
diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org
index 20ba7b268..05e4d717f 100644
--- a/doc/org/autfilt.org
+++ b/doc/org/autfilt.org
@@ -493,12 +493,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex1.png :cmdline -Tpng :var txt=autfilt-ex1 :exports results
-$txt
+#+BEGIN_SRC dot :file autfilt-ex1.svg :var txt=autfilt-ex1 :exports results
+  $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex1.png]]
+[[file:autfilt-ex1.svgz]]
 
 Using =-S= will "push" the acceptance membership of the transitions to the states:
 
@@ -555,12 +555,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex2.png :cmdline -Tpng :var txt=autfilt-ex2 :exports results
+#+BEGIN_SRC dot :file autfilt-ex2.svg :var txt=autfilt-ex2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex2.png]]
+[[file:autfilt-ex2.svg]]
 
 Using =--cnf-acceptance= simply rewrites the acceptance condition in Conjunctive Normal Form:
 
@@ -596,12 +596,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex3.png :cmdline -Tpng :var txt=autfilt-ex3 :exports results
+#+BEGIN_SRC dot :file autfilt-ex3.svg :var txt=autfilt-ex3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex3.png]]
+[[file:autfilt-ex3.svg]]
 
 
 Using =--remove-fin= transforms the automaton to remove all traces
@@ -643,12 +643,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex4.png :cmdline -Tpng :var txt=autfilt-ex4 :exports results
+#+BEGIN_SRC dot :file autfilt-ex4.svg :var txt=autfilt-ex4 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex4.png]]
+[[file:autfilt-ex4.svg]]
 
 Use =--mask-acc=NUM= to remove some acceptances sets and all
 transitions they contain.  The acceptance condition will be updated to
@@ -684,12 +684,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex5.png :cmdline -Tpng :var txt=autfilt-ex5 :exports results
+#+BEGIN_SRC dot :file autfilt-ex5.svg :var txt=autfilt-ex5 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex5.png]]
+[[file:autfilt-ex5.svg]]
 
 ** Atomic proposition removal
 
@@ -733,12 +733,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex6a.png :cmdline -Tpng :var txt=autfilt-ex6a :exports results
+#+BEGIN_SRC dot :file autfilt-ex6a.svg :var txt=autfilt-ex6a :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex6a.png]]
+[[file:autfilt-ex6a.svg]]
 
 #+NAME: autfilt-ex6b
 #+BEGIN_SRC sh :results verbatim :exports code
@@ -766,12 +766,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-ex6b.png :cmdline -Tpng :var txt=autfilt-ex6b :exports results
+#+BEGIN_SRC dot :file autfilt-ex6b.svg :var txt=autfilt-ex6b :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex6b.png]]
+[[file:autfilt-ex6b.svg]]
 
 #+NAME: autfilt-ex6c
 #+BEGIN_SRC sh :results verbatim :exports code
@@ -780,12 +780,12 @@ autfilt --remove-ap=a=1 aut-ex1.hoa --dot=.a
 
 #+RESULTS: autfilt-ex6c
 
-#+BEGIN_SRC dot :file autfilt-ex6c.png :cmdline -Tpng :var txt=autfilt-ex6c :exports results
+#+BEGIN_SRC dot :file autfilt-ex6c.svg :var txt=autfilt-ex6c :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-ex6c.png]]
+[[file:autfilt-ex6c.svg]]
 
 ** Testing word acceptance
 
@@ -886,12 +886,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-hlword.png :cmdline -Tpng :var txt=highlight-word :exports results
+#+BEGIN_SRC dot :file autfilt-hlword.svg :var txt=highlight-word :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-hlword.png]]
+[[file:autfilt-hlword.svg]]
 
 
 We can change the color by prefixing the word with a number and a
@@ -930,12 +930,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-hlword2.png :cmdline -Tpng :var txt=highlight-word2 :exports results
+#+BEGIN_SRC dot :file autfilt-hlword2.svg :var txt=highlight-word2 :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-hlword2.png]]
+[[file:autfilt-hlword2.svg]]
 
 
 
@@ -978,12 +978,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfilt-hlnondet.png :cmdline -Tpng :var txt=highlight-nondet :exports results
+#+BEGIN_SRC dot :file autfilt-hlnondet.svg :var txt=highlight-nondet :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfilt-hlnondet.png]]
+[[file:autfilt-hlnondet.svg]]
 
 
 #+BEGIN_SRC sh :results silent :exports results
diff --git a/doc/org/concepts.org b/doc/org/concepts.org
index 22933274d..9f79718a8 100644
--- a/doc/org/concepts.org
+++ b/doc/org/concepts.org
@@ -132,12 +132,12 @@ which $a$ is always true, and $b$ is true infinitely often.
 ltl2tgba 'G(a) & GF(b)' -B -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file concept-buchi1.png :cmdline -Tpng :var txt=buchi-example1 :exports results
+#+BEGIN_SRC dot :file concept-buchi1.svg :var txt=buchi-example1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-buchi1.png]]
+[[file:concept-buchi1.svg]]
 
 
 The above automaton would accept the [[#word][ω-word we used previously as an
@@ -153,12 +153,12 @@ the [[#ltl][LTL formula]] =G(door_open -> light_on)= that specifies that
 ltl2tgba 'G(door_open -> light_on)' -d -C
 #+END_SRC
 
-#+BEGIN_SRC dot :file concept-buchi2.png :cmdline -Tpng :var txt=buchi-example2 :exports results
+#+BEGIN_SRC dot :file concept-buchi2.svg :var txt=buchi-example2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-buchi.png]]
+[[file:concept-buchi.svg]]
 
 The =1= displayed on the edge that loops on state =1= should be
 read as /true/, i.e., the Boolean formula that accepts
@@ -186,12 +186,12 @@ instant.
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba 'G(a <-> Xb)' -B -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-buchi3.png :cmdline -Tpng :var txt=buchi-example3 :exports results
+#+BEGIN_SRC dot :file concept-buchi3.svg :var txt=buchi-example3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-buchi3.png]]
+[[file:concept-buchi3.svg]]
 
 * Transitions vs. Edges
    :PROPERTIES:
@@ -224,12 +224,12 @@ State: 1 1 0 0 0
 EOF
 autfilt --merge concept-te.hoa -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-te1.png :cmdline -Tpng :var txt=te1 :exports results
+#+BEGIN_SRC dot :file concept-te1.svg :var txt=te1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-te1.png]]
+[[file:concept-te1.svg]]
 
 #+NAME: size
 #+BEGIN_SRC sh :exports none
@@ -246,12 +246,12 @@ following transition structure:
 #+BEGIN_SRC sh :results verbatim :exports none
 autfilt concept-te.hoa -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-te2.png :cmdline -Tpng :var txt=te2 :exports results
+#+BEGIN_SRC dot :file concept-te2.svg :var txt=te2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-te2.png]]
+[[file:concept-te2.svg]]
 
 The above is actually a different automaton from the point of view of
 Spot: it is an automaton with call_size(arg="%t")[:results raw] edges
@@ -300,12 +300,12 @@ contains a single state.
 ltl2tgba 'GFa & GFb' | autfilt -S --sat-minimize -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file concept-gba1.png :cmdline -Tpng :var txt=gen-buchi-example1 :exports results
+#+BEGIN_SRC dot :file concept-gba1.svg :var txt=gen-buchi-example1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-gba1.png]]
+[[file:concept-gba1.svg]]
 
 The accepting runs are only those that visit infinitely often both
 states, so that means this automaton accepts all words in which $a$
@@ -321,12 +321,12 @@ its more complex look).
 ltl2tgba 'GFa & GFb' -S -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file concept-gba2.png :cmdline -Tpng :var txt=gen-buchi-example2 :exports results
+#+BEGIN_SRC dot :file concept-gba2.svg :var txt=gen-buchi-example2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-gba2.png]]
+[[file:concept-gba2.svg]]
 
 
 Speaking of size... Let us note that using a generalized Büchi
@@ -341,12 +341,12 @@ equivalent Büchi automaton has three state:
 ltl2tgba 'GFa & GFb' -B -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file concept-gba-vs-ba.png :cmdline -Tpng :var txt=gen-buchi-example-ba :exports results
+#+BEGIN_SRC dot :file concept-gba-vs-ba.svg :var txt=gen-buchi-example-ba :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-gba-vs-ba.png]]
+[[file:concept-gba-vs-ba.svg]]
 
 Finally, let us point the obvious fact that a Büchi automaton is a
 particular case of generalized-Büchi acceptance with a single
@@ -360,12 +360,12 @@ both.
 ltl2tgba 'GFa & GFb' -B -d.b
 #+END_SRC
 
-#+BEGIN_SRC dot :file concept-gba-vs-ba2.png :cmdline -Tpng :var txt=gen-buchi-example-ba2 :exports results
+#+BEGIN_SRC dot :file concept-gba-vs-ba2.svg :var txt=gen-buchi-example-ba2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-gba-vs-ba2.png]]
+[[file:concept-gba-vs-ba2.svg]]
 
 * Transition-based, vs. State-based acceptance
    :PROPERTIES:
@@ -387,12 +387,12 @@ Here is an example of Transition-based Generalized Büchi Automaton
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba 'GF(a & X(a U b))' -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-tgba1.png :cmdline -Tpng :var txt=tgba-example1 :exports results
+#+BEGIN_SRC dot :file concept-tgba1.svg :var txt=tgba-example1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-tgba1.png]]
+[[file:concept-tgba1.svg]]
 
 This automaton accept all ω-words that infinitely often match the
 pattern $a^+;b$ (that is: a positive number of letters where $a$ is
@@ -406,12 +406,12 @@ automaton:
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba 'GFa' -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-tgba2.png :cmdline -Tpng :var txt=tgba-example2 :exports results
+#+BEGIN_SRC dot :file concept-tgba2.svg :var txt=tgba-example2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-tgba2.png]]
+[[file:concept-tgba2.svg]]
 
 While the same property require a 2-state Büchi automaton using
 state-based acceptance:
@@ -420,12 +420,12 @@ state-based acceptance:
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba 'GFa' -B -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-tba-vs-ba.png :cmdline -Tpng :var txt=tgba-example3 :exports results
+#+BEGIN_SRC dot :file concept-tba-vs-ba.svg :var txt=tgba-example3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-tba-vs-ba.png]]
+[[file:concept-tba-vs-ba.svg]]
 
 
 #+BEGIN_implem
@@ -547,12 +547,12 @@ by Spot:
 #+BEGIN_SRC sh :results verbatim :exports none
 ltlfilt -l -f 'GFa | FGb' | ltl2dstar --output-format=hoa - - | autfilt --merge -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file concept-twa1.png :cmdline -Tpng :var txt=twa-example1 :exports results
+#+BEGIN_SRC dot :file concept-twa1.svg :var txt=twa-example1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-twa1.png]]
+[[file:concept-twa1.svg]]
 
 * Alternating ω-automata
 
@@ -600,12 +600,12 @@ State: 4 "t"
 EOF
 #+END_SRC
 
-#+BEGIN_SRC dot :file concepts-alt.png :cmdline -Tpng :var txt=concepts-alt :exports results
+#+BEGIN_SRC dot :file concepts-alt.svg :var txt=concepts-alt :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concepts-alt.png]]
+[[file:concepts-alt.svg]]
 
 In this picture, the universal edges appear as arrows with a white
 tip going to a small dot, from which additional arrows connect to the
@@ -668,12 +668,12 @@ accept_all:				accept_all:
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba -Bd 'p0 | GFp1'
 #+END_SRC
-#+BEGIN_SRC dot :file concept-never1.png :cmdline -Tpng :var txt=never-ex1 :exports results
+#+BEGIN_SRC dot :file concept-never1.svg :var txt=never-ex1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-never1.png]]
+[[file:concept-never1.svg]]
 
 The two different types of never claims differ only in a few syntactic
 elements: =do..od= instead of =if..fi=, =assert= instead of =goto
@@ -721,7 +721,7 @@ ltl2tgba --ba --lbtt 'p0 | GFp1'
 -1
 #+end_example
 
-[[file:concept-never1.png]]
+[[file:concept-never1.svg]]
 
 The format has been extended in two ways.  First, LBTT extended it to
 support transition-based acceptance.  This is indicated by a =t= on
@@ -751,12 +751,12 @@ ltl2tgba --lbtt 'p0 | GFp1'
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba -d 'p0 | GFp1'
 #+END_SRC
-#+BEGIN_SRC dot :file concept-lbtt2.png :cmdline -Tpng :var txt=lbtt-ex2 :exports results
+#+BEGIN_SRC dot :file concept-lbtt2.svg :var txt=lbtt-ex2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-lbtt2.png]]
+[[file:concept-lbtt2.svg]]
 
 We call this format the LBTT format because of this extension.
 
@@ -824,12 +824,12 @@ Acc-Sig: +0 +1
 #+BEGIN_SRC sh :results verbatim :exports none
 echo '| F G p0 G F p1' | ltl2dstar --output-format=native - - | autfilt -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file concept-dstar.png :cmdline -Tpng :var txt=dstar-example1 :exports results
+#+BEGIN_SRC dot :file concept-dstar.svg :var txt=dstar-example1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-dstar.png]]
+[[file:concept-dstar.svg]]
 
 * Hanoi Omega-Automaton format (HOA)
    :PROPERTIES:
@@ -883,12 +883,12 @@ State: 3 {1 3}
 #+BEGIN_SRC sh :results verbatim :exports none
 ltldo ltl2dstar -f 'FGp0 | GFp1' -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file concept-hoa.png :cmdline -Tpng :var txt=hoa1 :exports results
+#+BEGIN_SRC dot :file concept-hoa.svg :var txt=hoa1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-hoa.png]]
+[[file:concept-hoa.svg]]
 
 
 Since this file format is the only one able to represent the range of
@@ -997,12 +997,12 @@ Here is for instance a translation of ={(1;1)[*]}[]->a= discussed [[#psl][above]
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba '{(1;1)[*]}[]->a' -d
 #+END_SRC
-#+BEGIN_SRC dot :file concept-ltl2tgba.png :cmdline -Tpng :var txt=ltl2tgba1 :exports results
+#+BEGIN_SRC dot :file concept-ltl2tgba.svg :var txt=ltl2tgba1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:concept-ltl2tgba.png]]
+[[file:concept-ltl2tgba.svg]]
 
 
 [[file:tut10.org][Another page shows how to translate an LTL formula into a never claim]]
@@ -1013,7 +1013,7 @@ from the command-line, Python, or C++.
    :CUSTOM_ID: architecture
    :END:
 
-[[file:arch.png]]
+[[file:arch.svg]]
 
 The Spot project can be broken down into several parts, as shown
 above.  Orange boxes are C/C++ libraries.  Red boxes are command-line
diff --git a/doc/org/dstar2tgba.org b/doc/org/dstar2tgba.org
index 9c69cd49e..3ea005063 100644
--- a/doc/org/dstar2tgba.org
+++ b/doc/org/dstar2tgba.org
@@ -114,12 +114,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file fagfb.png :cmdline -Tpng :var txt=fagfb :exports results
+#+BEGIN_SRC dot :file fagfb.svg :var txt=fagfb :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:fagfb.png]]
+[[file:fagfb.svg]]
 
 We used =--dot=a= to display Spot's representation of the acceptance
 condition (which uses the same convention as in the [[file:hoa.org][HOA format]]).  The
@@ -158,11 +158,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file fagfb2ba.png :cmdline -Tpng :var txt=fagfb2ba :exports results
+#+BEGIN_SRC dot :file fagfb2ba.svg :var txt=fagfb2ba :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:fagfb2ba.png]]
+[[file:fagfb2ba.svg]]
 
 
 Note that by default the output is not complete.  Use =-C= if you want
@@ -243,12 +243,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gfafgb.png :cmdline -Tpng :var txt=gfafgb :exports results
+#+BEGIN_SRC dot :file gfafgb.svg :var txt=gfafgb :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:gfafgb.png]]
+[[file:gfafgb.svg]]
 
 
 
@@ -294,11 +294,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gfagfb2ba.png :cmdline -Tpng :var txt=gfagfb2ba :exports results
+#+BEGIN_SRC dot :file gfagfb2ba.svg :var txt=gfagfb2ba :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gfagfb2ba.png]]
+[[file:gfagfb2ba.svg]]
 
 Obviously the resulting automaton could be simplified further, as the
 minimal TGBA for this formula has a single state.  (Patches
diff --git a/doc/org/genaut.org b/doc/org/genaut.org
index 3bb4045dc..74d8fad99 100644
--- a/doc/org/genaut.org
+++ b/doc/org/genaut.org
@@ -34,12 +34,12 @@ For instance:
 genaut --ks-nca=2 --dot
 #+END_SRC
 
-#+BEGIN_SRC dot :file kscobuchi2.png :cmdline -Tpng :var txt=kscobuchi2 :exports results
+#+BEGIN_SRC dot :file kscobuchi2.svg :var txt=kscobuchi2 :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:kscobuchi2.png]]
+[[file:kscobuchi2.svg]]
 
 The patterns can be specified using a range of the form =N= (a single
 value), =N..M= (all values between N and M included), or =..M= (all
diff --git a/doc/org/hierarchy.org b/doc/org/hierarchy.org
index 5d942eef8..b92b00921 100644
--- a/doc/org/hierarchy.org
+++ b/doc/org/hierarchy.org
@@ -18,7 +18,7 @@ the /recurrence/ class includes the /obligation/ class which also
 includes the /safety/ and /guarantee/ classes, as well as the unnamed
 intersection of /safety/ and /guarantee/ (=B= in the picture).
 
-[[file:hierarchy.png]]
+[[file:hierarchy.svg]]
 
 Forget about the LTL properties and about the red letters displayed in
 this picture for a moment.
@@ -307,12 +307,12 @@ non-determinism occurs):
 ltl2tgba 'Fa R b' | autfilt --highlight-nondet -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file hier-oblig-1.png :cmdline -Tpng :var txt=hier-oblig-1 :exports results
+#+BEGIN_SRC dot :file hier-oblig-1.svg :var txt=hier-oblig-1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-oblig-1.png]]
+[[file:hier-oblig-1.svg]]
 
 Note that the above automaton uses transition-based acceptance, but
 since it is an obligation, using transition-based acceptance will not
@@ -324,12 +324,12 @@ improve anything, so we might as well require a Büchi automaton with
 ltl2tgba -B 'Fa R b' | autfilt --highlight-nondet -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file hier-oblig-1b.png :cmdline -Tpng :var txt=hier-oblig-1b :exports results
+#+BEGIN_SRC dot :file hier-oblig-1b.svg :var txt=hier-oblig-1b :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-oblig-1b.png]]
+[[file:hier-oblig-1b.svg]]
 
 
 With =ltl2tgba -D= we get a (minimal) deterministic weak Büchi
@@ -340,12 +340,12 @@ automaton instead.
   ltl2tgba -D 'Fa R b' -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file hier-oblig-2.png :cmdline -Tpng :var txt=hier-oblig-2 :exports results
+#+BEGIN_SRC dot :file hier-oblig-2.svg :var txt=hier-oblig-2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-oblig-2.png]]
+[[file:hier-oblig-2.svg]]
 
 
 When we called =ltl2tgba=, without the option =-D=, the two automata
@@ -364,12 +364,12 @@ for the obligation property =a <-> GXa=:
 #+BEGIN_SRC sh :results verbatim :exports code
 ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file hier-oblig-3.png :cmdline -Tpng :var txt=hier-oblig-3 :exports results
+#+BEGIN_SRC dot :file hier-oblig-3.svg :var txt=hier-oblig-3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-oblig-3.png]]
+[[file:hier-oblig-3.svg]]
 
 We can now minimize this automaton with:
 
@@ -377,11 +377,11 @@ We can now minimize this automaton with:
 #+BEGIN_SRC sh :results verbatim :exports code
 ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' | autfilt -D -C -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-oblig-4.png :cmdline -Tpng :var txt=hier-oblig-4 :exports results
+#+BEGIN_SRC dot :file hier-oblig-4.svg :var txt=hier-oblig-4 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:hier-oblig-4.png]]
+[[file:hier-oblig-4.svg]]
 
 Here we have used option =-C= to keep the automaton complete, so that
 the comparison with =ltl2dstar= is fair, since =ltl2dstar= always
@@ -411,23 +411,23 @@ ltlfilt -f 'a U Xb' --format='%[v]h'
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba 'a U Xb' | autfilt --highlight-nondet -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-guarantee-1.png :cmdline -Tpng :var txt=hier-guarantee-1 :exports results
+#+BEGIN_SRC dot :file hier-guarantee-1.svg :var txt=hier-guarantee-1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-guarantee-1.png]]
+[[file:hier-guarantee-1.svg]]
 
 #+NAME: hier-guarantee-2
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -D 'a U Xb' -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-guarantee-2.png :cmdline -Tpng :var txt=hier-guarantee-2 :exports results
+#+BEGIN_SRC dot :file hier-guarantee-2.svg :var txt=hier-guarantee-2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-guarantee-2.png]]
+[[file:hier-guarantee-2.svg]]
 
 ** Safety
    :PROPERTIES:
@@ -461,12 +461,12 @@ ltlfilt -f '(a W Gb) M b' --format='%[v]h'
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba '(a W Gb) M b' | autfilt --highlight-nondet -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-safety-1.png :cmdline -Tpng :var txt=hier-safety-1 :exports results
+#+BEGIN_SRC dot :file hier-safety-1.svg :var txt=hier-safety-1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-safety-1.png]]
+[[file:hier-safety-1.svg]]
 
 Actually, marking all states of this automaton as accepting would not
 be wrong, the translator simply does not know it.
@@ -478,12 +478,12 @@ that is guaranteed to be minimal, and where all runs are accepting.
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -D '(a W Gb) M b' -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-safety-2.png :cmdline -Tpng :var txt=hier-safety-2 :exports results
+#+BEGIN_SRC dot :file hier-safety-2.svg :var txt=hier-safety-2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-safety-2.png]]
+[[file:hier-safety-2.svg]]
 
 
 If you are working with safety formula, and know you want to work with
@@ -497,23 +497,23 @@ extended into valid ω-words).
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -M '(a W Gb) M b' | autfilt --highlight-nondet -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-safety-1m.png :cmdline -Tpng :var txt=hier-safety-1m :exports results
+#+BEGIN_SRC dot :file hier-safety-1m.svg :var txt=hier-safety-1m :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-safety-1m.png]]
+[[file:hier-safety-1m.svg]]
 
 #+NAME: hier-safety-2m
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -M -D '(a W Gb) M b' -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-safety-2m.png :cmdline -Tpng :var txt=hier-safety-2m :exports results
+#+BEGIN_SRC dot :file hier-safety-2m.svg :var txt=hier-safety-2m :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-safety-2m.png]]
+[[file:hier-safety-2m.svg]]
 
 
 Note that the =-M= option can be used with formulas that are not
@@ -550,12 +550,12 @@ ltlfilt -f 'GFa' --format='%[v]h'
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba 'GFa' -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-recurrence-1.png :cmdline -Tpng :var txt=hier-recurrence-1 :exports results
+#+BEGIN_SRC dot :file hier-recurrence-1.svg :var txt=hier-recurrence-1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-recurrence-1.png]]
+[[file:hier-recurrence-1.svg]]
 
 Using state-based acceptance, at least two states are required.  For instance:
 
@@ -563,12 +563,12 @@ Using state-based acceptance, at least two states are required.  For instance:
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -S 'GFa' -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-recurrence-2.png :cmdline -Tpng :var txt=hier-recurrence-2 :exports results
+#+BEGIN_SRC dot :file hier-recurrence-2.svg :var txt=hier-recurrence-2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-recurrence-2.png]]
+[[file:hier-recurrence-2.svg]]
 
 
 Here is an example of a formula for which =ltl2tgba= does not produce a
@@ -585,12 +585,12 @@ ltlfilt -f 'G(Gb | Fa)' --format='%[v]h'
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -D 'G(Gb | Fa)' | autfilt --highlight-nondet -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-recurrence-3.png :cmdline -Tpng :var txt=hier-recurrence-3 :exports results
+#+BEGIN_SRC dot :file hier-recurrence-3.svg :var txt=hier-recurrence-3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-recurrence-3.png]]
+[[file:hier-recurrence-3.svg]]
 
 One way to obtain a deterministic Büchi automaton (it has to exist, since this is
 a /recurrence/ property), is to chain a few algorithms implemented in Spot:
@@ -604,11 +604,11 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot:
     #+BEGIN_SRC sh :results verbatim :exports code
     ltl2tgba -G -D 'G(Gb | Fa)' -d.a
     #+END_SRC
-    #+BEGIN_SRC dot :file hier-recurrence-4.png :cmdline -Tpng :var txt=hier-recurrence-4 :exports results
+    #+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results
     $txt
     #+END_SRC
     #+RESULTS:
-    [[file:hier-recurrence-4.png]]
+    [[file:hier-recurrence-4.svg]]
 
  2. Transform the parity acceptance into Rabin acceptance: this is
     done with =autfilt --generalized-rabin=.  Because of the type of
@@ -620,12 +620,12 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot:
     ltl2tgba -G -D 'G(Gb | Fa)' |
       autfilt --generalized-rabin -d.a
     #+END_SRC
-    #+BEGIN_SRC dot :file hier-recurrence-5.png :cmdline -Tpng :var txt=hier-recurrence-5 :exports results
+    #+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results
     $txt
     #+END_SRC
 
     #+RESULTS:
-    [[file:hier-recurrence-5.png]]
+    [[file:hier-recurrence-5.svg]]
 
     (The only change here is in the acceptance condition.)
 
@@ -640,12 +640,12 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot:
       autfilt -S --generalized-rabin -d.a
     #+END_SRC
 
-    #+BEGIN_SRC dot :file hier-recurrence-6.png :cmdline -Tpng :var txt=hier-recurrence-6 :exports results
+    #+BEGIN_SRC dot :file hier-recurrence-6.svg :var txt=hier-recurrence-6 :exports results
     $txt
     #+END_SRC
 
     #+RESULTS:
-    [[file:hier-recurrence-6.png]]
+    [[file:hier-recurrence-6.svg]]
 
  4. Finally, convert the resulting automaton to BA, using =autfilt
     -B=.  Spot can convert automata with any acceptance condition to
@@ -664,12 +664,12 @@ a /recurrence/ property), is to chain a few algorithms implemented in Spot:
       autfilt -B -D -d.a
     #+END_SRC
 
-    #+BEGIN_SRC dot :file hier-recurrence-7.png :cmdline -Tpng :var txt=hier-recurrence-7 :exports results
+    #+BEGIN_SRC dot :file hier-recurrence-7.svg :var txt=hier-recurrence-7 :exports results
     $txt
     #+END_SRC
 
     #+RESULTS:
-    [[file:hier-recurrence-7.png]]
+    [[file:hier-recurrence-7.svg]]
 
 Here we are lucky that the deterministic Büchi automaton is even
 smaller than the original non-deterministic version.  As said earlier,
@@ -683,12 +683,12 @@ ltl2tgba -G -D 'G(Gb | Fa)' |
   autfilt -B -D -d.a
 #+END_SRC
 
-#+BEGIN_SRC dot :file hier-recurrence-8.png :cmdline -Tpng :var txt=hier-recurrence-8 :exports results
+#+BEGIN_SRC dot :file hier-recurrence-8.svg :var txt=hier-recurrence-8 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-recurrence-8.png]]
+[[file:hier-recurrence-8.svg]]
 
 It is likely that =ltl2tgba= will implement all this processing chain
 in the future.
@@ -703,12 +703,12 @@ persistence formula is =FGa=, and using =-D= on this is hopeless.
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -D FGa -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file hier-persistence-1.png :cmdline -Tpng :var txt=hier-persistence-1 :exports results
+#+BEGIN_SRC dot :file hier-persistence-1.svg :var txt=hier-persistence-1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-persistence-1.png]]
+[[file:hier-persistence-1.svg]]
 
 
 However since the *negation* of =FGa= is a /recurrence/, this negation
@@ -723,12 +723,12 @@ ltlfilt --negate -f FGa |
   ltl2tgba -D |
   autfilt --complement -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file hier-persistence-2.png :cmdline -Tpng :var txt=hier-persistence-2 :exports results
+#+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-persistence-2.png]]
+[[file:hier-persistence-2.svg]]
 
 Note that in this example, we know that =GFa= is trivial enough that
 =ltl2tgba -D GFa= will generate a deterministic automaton.  In the
@@ -765,12 +765,12 @@ Unfortunately the default output of the translation is not weak:
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba 'F(G!a | G(b U a))' -d
 #+END_SRC
-#+BEGIN_SRC dot :file hier-persistence-3.png :cmdline -Tpng :var txt=hier-persistence-3 :exports results
+#+BEGIN_SRC dot :file hier-persistence-3.svg :var txt=hier-persistence-3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-persistence-3.png]]
+[[file:hier-persistence-3.svg]]
 
 Furthermore it appears that =ltl2tgba= does generate a deterministic
 Büchi automaton for the complement, instead we get a non-deterministic
@@ -782,12 +782,12 @@ ltlfilt --negate -f 'F(G!a | G(b U a))' |
   ltl2tgba -D |
   autfilt --highlight-nondet=5 -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file hier-persistence-4.png :cmdline -Tpng :var txt=hier-persistence-4 :exports results
+#+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-persistence-4.png]]
+[[file:hier-persistence-4.svg]]
 
 So let us use the same tricks as in the previous section,
 determinizing this automaton into a Rabin automaton, and then back to
@@ -800,12 +800,12 @@ ltlfilt --negate -f 'F(G!a | G(b U a))' |
   autfilt --generalized-rabin |
   autfilt --tgba -D -d.a
 #+END_SRC
-#+BEGIN_SRC dot :file hier-persistence-5.png :cmdline -Tpng :var txt=hier-persistence-5 :exports results
+#+BEGIN_SRC dot :file hier-persistence-5.svg :var txt=hier-persistence-5 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-persistence-5.png]]
+[[file:hier-persistence-5.svg]]
 
 This is a deterministic Büchi automaton for the negation of our formula.
 Now we can complement it to obtain a deterministic co-Büchi automaton for =F(G!a | G(b U a))=:
@@ -818,12 +818,12 @@ ltlfilt --negate -f 'F(G!a | G(b U a))' |
   autfilt --tgba -D |
   autfilt --complement -d.ab
 #+END_SRC
-#+BEGIN_SRC dot :file hier-persistence-6.png :cmdline -Tpng :var txt=hier-persistence-6 :exports results
+#+BEGIN_SRC dot :file hier-persistence-6.svg :var txt=hier-persistence-6 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hier-persistence-6.png]]
+[[file:hier-persistence-6.svg]]
 
 And finally we convert the result back to Büchi:
 
@@ -836,10 +836,10 @@ ltlfilt --negate -f 'F(G!a | G(b U a))' |
   autfilt --complement -B -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file hier-persistence-7.png :cmdline -Tpng :var txt=hier-persistence-7 :exports results
+#+BEGIN_SRC dot :file hier-persistence-7.svg :var txt=hier-persistence-7 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:hier-persistence-7.png]]
+[[file:hier-persistence-7.svg]]
 
 That is indeed, a weak automaton.
diff --git a/doc/org/hierarchy.tex b/doc/org/hierarchy.tex
index 502910daf..71607fea4 100644
--- a/doc/org/hierarchy.tex
+++ b/doc/org/hierarchy.tex
@@ -1,4 +1,4 @@
-\documentclass[convert={size=360}]{standalone}
+\documentclass{standalone}
 \usepackage{tikz}
 \usetikzlibrary{shadows}
 \def\F{\mathsf{F}} % in future
@@ -8,6 +8,7 @@
 
 \def\mycyan{cyan!30}
 \def\mypink{magenta!30}
+\scalebox{1.2}{
  \begin{tikzpicture}[scale=.9]
     \draw[drop shadow,fill=white] (0,0) rectangle (6,7);
 
@@ -36,7 +37,7 @@
     \node[above,red] at (saf.north) {\tt S};
     \node[above,red] at (gua.north) {\tt G};
     \node[above,red] at (3,0.3) {\tt B};
-  \end{tikzpicture}
+  \end{tikzpicture}}
 \end{document}
 %%% Local Variables:
 %%% mode: latex
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
index 728024199..f86a27fda 100644
--- a/doc/org/hoa.org
+++ b/doc/org/hoa.org
@@ -1014,12 +1014,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file decorate.png :cmdline -Tpng :var txt=decorate :exports results
+#+BEGIN_SRC dot :file decorate.svg :var txt=decorate :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:decorate.png]]
+[[file:decorate.svg]]
 
 
 On the above example, we call =autfilt= with option =-d#= to display
diff --git a/doc/org/init.el.in b/doc/org/init.el.in
index 19e922c26..10714af1e 100644
--- a/doc/org/init.el.in
+++ b/doc/org/init.el.in
@@ -57,7 +57,7 @@
 	(concat "@abs_top_builddir@/python/.libs:@abs_top_builddir@/spot/.libs:@abs_top_builddir@/buddy/src/.libs:"
 		(getenv "DYLD_LIBRARY_PATH")))
 (setenv "SPOT_DOTDEFAULT" "Brf(Lato)C(#ffffa0)")
-(setenv "SPOT_DOTEXTRA" "edge[arrowhead=vee, arrowsize=.7]")
+(setenv "SPOT_DOTEXTRA" "node[fontsize=12] fontsize=12 stylesheet=\"spot.css\" edge[arrowhead=vee, arrowsize=.7, fontsize=12]")
 
 (setq org-export-html-home/up-format
 "<div id=\"org-div-home-and-up\" style=\"text-align:center;white-space:nowrap;\">
@@ -85,7 +85,7 @@
 	:auto-preamble t)
        ("spot-static"
 	:base-directory "@abs_top_srcdir@/doc/org/"
-	:base-extension "css\\|js\\|png\\|jpg\\|gif\\|pdf"
+	:base-extension "css\\|js\\|png\\|svg\\|jpg\\|gif\\|pdf"
 	:publishing-directory "@abs_top_srcdir@/doc/userdoc/"
 	:recursive t
 	:publishing-function org-publish-attachment)
diff --git a/doc/org/ltl2tgba.org b/doc/org/ltl2tgba.org
index f2f04185e..db01cbcb3 100644
--- a/doc/org/ltl2tgba.org
+++ b/doc/org/ltl2tgba.org
@@ -96,12 +96,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file dotex.png :cmdline -Tpng :var txt=dotex :exports results
+#+BEGIN_SRC dot :file dotex.svg :var txt=dotex :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:dotex.png]]
+[[file:dotex.svg]]
 
 Characters like ⓿, ❶, etc. denotes the acceptance sets a transition
 belongs to.  In this case, there is only one acceptance set, called
@@ -139,11 +139,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file dotex2.png :cmdline -Tpng :var txt=dotex2 :exports results
+#+BEGIN_SRC dot :file dotex2.svg :var txt=dotex2 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:dotex2.png]]
+[[file:dotex2.svg]]
 
 The above TGBA has two acceptance sets: ⓿ and ❶.  The position of
 these acceptance sets ensures that atomic propositions =a= and =b= must
@@ -181,11 +181,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file dotex2ba.png :cmdline -Tpng :var txt=dotex2ba :exports results
+#+BEGIN_SRC dot :file dotex2ba.svg :var txt=dotex2ba :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:dotex2ba.png]]
+[[file:dotex2ba.svg]]
 
 Although accepting states in the Büchi automaton are (traditionally)
 pictured with double-lines, internally this automaton is still handled
@@ -228,11 +228,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file dotex2ba-t.png :cmdline -Tpng :var txt=dotex2ba-t :exports results
+#+BEGIN_SRC dot :file dotex2ba-t.svg :var txt=dotex2ba-t :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:dotex2ba-t.png]]
+[[file:dotex2ba-t.svg]]
 
 Using option =-S= instead of option =-B= you can obtain generalized
 Büchi automata with state-based acceptance.  Here is the same formula
@@ -277,11 +277,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file dotex2gba.png :cmdline -Tpng :var txt=dotex2gba :exports results
+#+BEGIN_SRC dot :file dotex2gba.svg :var txt=dotex2gba :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:dotex2gba.png]]
+[[file:dotex2gba.svg]]
 
 Note that =ltl2tgba= is not very good at generating state-based
 generalized Büchi automata (GBA): all it does is generating a
@@ -368,11 +368,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file dotex2ba8.png :cmdline -Tpng :var txt=dotex2ba8 :exports results
+#+BEGIN_SRC dot :file dotex2ba8.svg :var txt=dotex2ba8 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:dotex2ba8.png]]
+[[file:dotex2ba8.svg]]
 
 * Spin output
 
@@ -498,11 +498,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gagbgc1.png :cmdline -Tpng :var txt=gagbgc1 :exports results
+#+BEGIN_SRC dot :file gagbgc1.svg :var txt=gagbgc1 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gagbgc1.png]]
+[[file:gagbgc1.svg]]
 
 #+NAME: gagbgc2
 #+BEGIN_SRC sh :results verbatim :exports code
@@ -548,11 +548,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gagbgc2.png :cmdline -Tpng :var txt=gagbgc2 :exports results
+#+BEGIN_SRC dot :file gagbgc2.svg :var txt=gagbgc2 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gagbgc2.png]]
+[[file:gagbgc2.svg]]
 
 You can augment the number of terms in the disjunction to magnify the
 difference.  For N terms, the =--small= automaton has N+1 states,
@@ -602,11 +602,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file ambig1.png :cmdline -Tpng :var txt=ambig1 :exports results
+#+BEGIN_SRC dot :file ambig1.svg :var txt=ambig1 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:ambig1.png]]
+[[file:ambig1.svg]]
 
 Here is an unambiguous automaton for the same formula, in which there
 is only one run that recognizes this example word:
@@ -650,12 +650,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file ambig2.png :cmdline -Tpng :var txt=ambig2 :exports results
+#+BEGIN_SRC dot :file ambig2.svg :var txt=ambig2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:ambig2.png]]
+[[file:ambig2.svg]]
 
 
 Unlike =--small= and =--deterministic= that express preferences,
@@ -734,12 +734,12 @@ expectations.
 ltl2tgba "FGa" -D -d.a
 #+END_SRC
 
-#+BEGIN_SRC dot :file ltl2tgba-fga.png :cmdline -Tpng :var txt=ltl2tgba-fga :exports results
+#+BEGIN_SRC dot :file ltl2tgba-fga.svg :var txt=ltl2tgba-fga :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:ltl2tgba-fga.png]]
+[[file:ltl2tgba-fga.svg]]
 
    But with =--generic=, =ltl2tgba= will output the following Rabin automaton:
 
@@ -748,12 +748,12 @@ ltl2tgba "FGa" -D -d.a
 ltl2tgba "FGa" -G -D -d.a
 #+END_SRC
 
-#+BEGIN_SRC dot :file ltl2tgba-fga-D.png :cmdline -Tpng :var txt=ltl2tgba-fga-D :exports results
+#+BEGIN_SRC dot :file ltl2tgba-fga-D.svg :var txt=ltl2tgba-fga-D :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:ltl2tgba-fga-D.png]]
+[[file:ltl2tgba-fga-D.svg]]
 
 Note that determinization algorithm implemented actually outputs
 parity acceptance, but =Fin(0)&Inf(1)= can be interpreted either as
@@ -772,12 +772,12 @@ For instance the following deterministic automaton
 ltl2tgba "F(a W FGb)" -G -D -d.a
 #+END_SRC
 
-#+BEGIN_SRC dot :file ltl2tgba-det1.png :cmdline -Tpng :var txt=ltl2tgba-det1 :exports results
+#+BEGIN_SRC dot :file ltl2tgba-det1.svg :var txt=ltl2tgba-det1 :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:ltl2tgba-det1.png]]
+[[file:ltl2tgba-det1.svg]]
 
 would be larger if SCC-based optimizations were disabled:
 
@@ -786,12 +786,12 @@ would be larger if SCC-based optimizations were disabled:
 ltl2tgba "F(a W FGb)" -x '!det-scc' -G -D -d.a
 #+END_SRC
 
-#+BEGIN_SRC dot :file ltl2tgba-det2.png :cmdline -Tpng :var txt=ltl2tgba-det2 :exports results
+#+BEGIN_SRC dot :file ltl2tgba-det2.svg :var txt=ltl2tgba-det2 :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:ltl2tgba-det2.png]]
+[[file:ltl2tgba-det2.svg]]
 
 * Translating multiple formulas for statistics
 
@@ -912,24 +912,24 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file monitor1.png :cmdline -Tpng :var txt=monitor1 :exports results
+#+BEGIN_SRC dot :file monitor1.svg :var txt=monitor1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:monitor1.png]]
+[[file:monitor1.svg]]
 
 #+NAME: monitor2
 #+BEGIN_SRC sh :results verbatim :exports code
 ltl2tgba -MD '(Xa & Fb) | Gc' -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file monitor2.png :cmdline -Tpng :var txt=monitor2 :exports results
+#+BEGIN_SRC dot :file monitor2.svg :var txt=monitor2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:monitor2.png]]
+[[file:monitor2.svg]]
 
 Because they accept all finite executions that could be extended to
 match the formula, monitor cannot be used to check for eventualities
@@ -951,12 +951,12 @@ if) a sink state had to be added.  For instance, here is the
 ltl2tgba -C -M -D '(Xa & Fb) | Gc' -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file monitor3.png :cmdline -Tpng :var txt=monitor3 :exports results
+#+BEGIN_SRC dot :file monitor3.svg :var txt=monitor3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:monitor3.png]]
+[[file:monitor3.svg]]
 
 
 
diff --git a/doc/org/ltl2tgta.org b/doc/org/ltl2tgta.org
index 6307db0dc..87b97b9e5 100644
--- a/doc/org/ltl2tgta.org
+++ b/doc/org/ltl2tgta.org
@@ -51,11 +51,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file augb-ta.png :cmdline -Tpng :var txt=augb-ta :exports results
+#+BEGIN_SRC dot :file augb-ta.svg :var txt=augb-ta :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:augb-ta.png]]
+[[file:augb-ta.svg]]
 
 As always, the labels of the states have no influence on the language
 recognized by the automaton.  This automaton has three possible
@@ -104,11 +104,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file augb-ta2.png :cmdline -Tpng :var txt=augb-ta2 :exports results
+#+BEGIN_SRC dot :file augb-ta2.svg :var txt=augb-ta2 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:augb-ta2.png]]
+[[file:augb-ta2.svg]]
 
 The =--gba= option can be used to request a Generalized Testing
 Automaton, i.e., a Testing Automaton with Generalized Büchi
@@ -149,11 +149,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gfagfb-gta.png :cmdline -Tpng :var txt=gfagfb-gta :exports results
+#+BEGIN_SRC dot :file gfagfb-gta.svg :var txt=gfagfb-gta :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gfagfb-gta.png]]
+[[file:gfagfb-gta.svg]]
 
 The interpretation is similar to that of the TA.  Execution that
 stutter in a livelock-accepting (square) state are accepting as well
@@ -203,11 +203,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gfagfb-tgta.png :cmdline -Tpng :var txt=gfagfb-tgta :exports results
+#+BEGIN_SRC dot :file gfagfb-tgta.svg :var txt=gfagfb-tgta :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gfagfb-tgta.png]]
+[[file:gfagfb-tgta.svg]]
 
 
 [fn:topnoc]: This new class of automaton, as well as the
diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org
index 2a470be6b..6bef8214b 100644
--- a/doc/org/ltlcross.org
+++ b/doc/org/ltlcross.org
@@ -476,7 +476,7 @@ number of transitions (7 versus 8), because the initial self-loop is
 more constrained in the first automaton.  A smaller number of
 transition is therefore an indication of a more constrained automaton.
 
-#+BEGIN_SRC dot :file edges.png :cmdline -Tpng :exports results
+#+BEGIN_SRC dot :file edges.svg :exports results
 digraph G {
   0 [label="", style=invis, height=0]
   0 -> 1
@@ -497,7 +497,7 @@ digraph G {
 #+END_SRC
 
 #+RESULTS:
-[[file:edges.png]]
+[[file:edges.svg]]
 
 
 =scc= counts the number of strongly-connected components in the automaton.
diff --git a/doc/org/oaut.org b/doc/org/oaut.org
index dac51f0a2..99c2636c6 100644
--- a/doc/org/oaut.org
+++ b/doc/org/oaut.org
@@ -300,12 +300,12 @@ digraph root {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file hoafex.png :cmdline -Tpng :var txt=hoafex :exports results
+#+BEGIN_SRC dot :file hoafex.svg :var txt=hoafex :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:hoafex.png]]
+[[file:hoafex.svg]]
 
 The [[http://adl.github.io/hoaf/][HOA format]] supports both state and transition-based acceptance.
 Although Spot works only with transition-based acceptance, its output
@@ -582,14 +582,15 @@ digraph G {
 ** Converting dot output to images or pdf
 
 This output should be processed with =dot= to be converted into a
-picture.  For instance use =dot -Tpng= or =dot -Tpdf=.
+picture.  For instance use =dot -Tpng= or =dot -Tpdf=.  The pictures
+on this page are produced with =dot -Tsvg=.
 
-#+BEGIN_SRC dot :file oaut-dot1.png :cmdline -Tpng :var txt=oaut-dot1 :exports results
+#+BEGIN_SRC dot :file oaut-dot1.svg :var txt=oaut-dot1 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:oaut-dot1.png]]
+[[file:oaut-dot1.svg]]
 
 ** Customizing the dot output
 
@@ -705,12 +706,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file oaut-dot2.png :cmdline -Tpng :var txt=oaut-dot2 :exports results
+#+BEGIN_SRC dot :file oaut-dot2.svg :var txt=oaut-dot2 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:oaut-dot2.png]]
+[[file:oaut-dot2.svg]]
 
 The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA
 format]]. Here =Inf(0)= means that runs are accepting if and only if
@@ -838,12 +839,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file oaut-dot3.png :cmdline -Tpng :var txt=oaut-dot3 :exports results
+#+BEGIN_SRC dot :file oaut-dot3.svg :var txt=oaut-dot3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:oaut-dot3.png]]
+[[file:oaut-dot3.svg]]
 
 <<default-dot>>
 
@@ -898,12 +899,14 @@ following figure:
 
 #+BEGIN_SRC sh :results silent :exports results
   ltl2tgba 'p0 U p1' --dot=x | dot2tex --autosize --nominsize > dot2tex.tex
+  sed -e 's/{article}/{standalone}/' -e '/^\\enlarge/d' dot2tex.tex >dot2tex.tmp
+  mv dot2tex.tmp dot2tex.tex
   latexmk --pdf dot2tex.tex
-  convert -density 300 -scale '50%' -trim dot2tex.pdf dot2tex.png
+  pdf2svg dot2tex.pdf dot2tex.svg
   latexmk -C dot2tex.tex
   rm -f dot2tex.tex
 #+END_SRC
-[[file:dot2tex.png]]
+[[file:dot2tex.svg]]
 
 Here an example with bullets denoting acceptance sets, and SCCs:
 
@@ -913,12 +916,15 @@ ltl2tgba -G -D '!a & FGa' --dot=sbarx | dot2tex --autosize --nominsize > out.tex
 
 #+BEGIN_SRC sh :results silent :exports results
   ltl2tgba -G -D '!a & FGa' --dot=sbarx | dot2tex --autosize --nominsize > dot2tex2.tex
+  sed -e 's/{article}/{standalone}/' -e '/^\\enlarge/d' dot2tex2.tex >dot2tex2.tmp
+  mv dot2tex2.tmp dot2tex2.tex
   latexmk --pdf dot2tex2.tex
-  convert -density 300 -scale '50%' -trim dot2tex2.pdf dot2tex2.png
+  pdf2svg dot2tex2.pdf dot2tex2.svg
   latexmk -C dot2tex2.tex
   rm -f dot2tex2.tex
 #+END_SRC
-[[file:dot2tex2.png]]
+
+[[file:dot2tex2.svg]]
 
 Caveats:
 - =dot2tex= should be called with option =--autosize= in order to
@@ -1121,12 +1127,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file oaut-name.png :cmdline -Tpng :var txt=oaut-name :exports results
+#+BEGIN_SRC dot :file oaut-name.svg :var txt=oaut-name :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:oaut-name.png]]
+[[file:oaut-name.svg]]
 
 If you have an automaton saved in the HOA format, you can extract its
 name using =autfilt --stats=%M input.hoa=. The =%M= escape sequence is
diff --git a/doc/org/randaut.org b/doc/org/randaut.org
index 99639c4af..23d31d588 100644
--- a/doc/org/randaut.org
+++ b/doc/org/randaut.org
@@ -70,11 +70,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut1.png :cmdline -Tpng :var txt=randaut1 :exports results
+#+BEGIN_SRC dot :file randaut1.svg :var txt=randaut1 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut1.png]]
+[[file:randaut1.svg]]
 
 As for [[file:randltl.org][=randltl=]], you can supply a number of atomic propositions
 instead of giving a list of atomic propositions.
@@ -119,11 +119,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut2.png :cmdline -Tpng :var txt=randaut2 :exports results
+#+BEGIN_SRC dot :file randaut2.svg :var txt=randaut2 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut2.png]]
+[[file:randaut2.svg]]
 
 #+NAME: randaut3
 #+BEGIN_SRC sh :results verbatim :exports code
@@ -156,12 +156,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut3.png :cmdline -Tpng :var txt=randaut3 :exports results
+#+BEGIN_SRC dot :file randaut3.svg :var txt=randaut3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:randaut3.png]]
+[[file:randaut3.svg]]
 
 * Acceptance condition
 
@@ -249,11 +249,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut4.png :cmdline -Tpng :var txt=randaut4 :exports results
+#+BEGIN_SRC dot :file randaut4.svg :var txt=randaut4 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut4.png]]
+[[file:randaut4.svg]]
 
 
 #+NAME: randaut5
@@ -285,11 +285,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut5.png :cmdline -Tpng :var txt=randaut5 :exports results
+#+BEGIN_SRC dot :file randaut5.svg :var txt=randaut5 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut5.png]]
+[[file:randaut5.svg]]
 
 #+NAME: randaut5b
 #+BEGIN_SRC sh :results verbatim :exports code
@@ -332,11 +332,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut5b.png :cmdline -Tpng :var txt=randaut5b :exports results
+#+BEGIN_SRC dot :file randaut5b.svg :var txt=randaut5b :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut5b.png]]
+[[file:randaut5b.svg]]
 
 For generating random parity automata you should use the option
 =--colored= to make sure each transition (or state in the following
@@ -400,11 +400,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut5c.png :cmdline -Tpng :var txt=randaut5c :exports results
+#+BEGIN_SRC dot :file randaut5c.svg :var txt=randaut5c :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut5c.png]]
+[[file:randaut5c.svg]]
 
 * Determinism
 
@@ -449,11 +449,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file randaut6.png :cmdline -Tpng :var txt=randaut6 :exports results
+#+BEGIN_SRC dot :file randaut6.svg :var txt=randaut6 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:randaut6.png]]
+[[file:randaut6.svg]]
 
 
 Note that in a deterministic automaton with $a$ atomic propositions,
@@ -521,12 +521,12 @@ autfilt --sccs=5 --trivial-sccs=1 --rejecting-sccs=1 \
         --inherently-weak-sccs=2 --weak-sccs=1 -n 1 --dot=.as
 #+END_SRC
 
-#+BEGIN_SRC dot :file randaut7.png :cmdline -Tpng :var txt=randaut7 :exports results
+#+BEGIN_SRC dot :file randaut7.svg :var txt=randaut7 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:randaut7.png]]
+[[file:randaut7.svg]]
 
 You should be able to find each of the expected type of SCCs in the above picture.
 The green rectangles mark the three SCCs that contain some accepting cycles.
diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index 73b9a415a..ef7719ae8 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -153,11 +153,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gfaexxb3.png :cmdline -Tpng :var txt=gfaexxb3 :exports results
+#+BEGIN_SRC dot :file gfaexxb3.svg :var txt=gfaexxb3 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gfaexxb3.png]]
+[[file:gfaexxb3.svg]]
 
 Clearly this automaton benefits from the transition-based
 acceptance.  If we want a traditional Büchi automaton, with
@@ -207,11 +207,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file gfaexxb4.png :cmdline -Tpng :var txt=gfaexxb4 :exports results
+#+BEGIN_SRC dot :file gfaexxb4.svg :var txt=gfaexxb4 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:gfaexxb4.png]]
+[[file:gfaexxb4.svg]]
 
 
 There are cases where =ltl2tgba='s =tba-det= algorithm fails to produce a deterministic automaton.
@@ -319,7 +319,7 @@ minimal DBA/DTBA/DTGBA.  The blue area at the top describes =ltl2tgba
 -D -x sat-minimize=, while the purple area at the bottom corresponds
 to =dstar2tgba -D -x stat-minimize=.
 
-[[file:satmin.png]]
+[[file:satmin.svg]]
 
 The picture is slightly inaccurate in the sense that both =ltl2tgba=
 and =dstar2tgba= are actually using the same post-processing chain:
@@ -454,11 +454,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm1.png :cmdline -Tpng :var txt=autfiltsm1 :exports results
+#+BEGIN_SRC dot :file autfiltsm1.svg :var txt=autfiltsm1 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:autfiltsm1.png]]
+[[file:autfiltsm1.svg]]
 
 So this is a state-based Rabin automaton with two pairs.  If we call
 =autfilt= with the =--sat-minimize= option, we can get the following
@@ -490,11 +490,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm2.png :cmdline -Tpng :var txt=autfiltsm2 :exports results
+#+BEGIN_SRC dot :file autfiltsm2.svg :var txt=autfiltsm2 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:autfiltsm2.png]]
+[[file:autfiltsm2.svg]]
 
 We can also attempt to build a state-based version with
 
@@ -525,11 +525,11 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm3.png :cmdline -Tpng :var txt=autfiltsm3 :exports results
+#+BEGIN_SRC dot :file autfiltsm3.svg :var txt=autfiltsm3 :exports results
 $txt
 #+END_SRC
 #+RESULTS:
-[[file:autfiltsm3.png]]
+[[file:autfiltsm3.svg]]
 
 This is clearly smaller than the input automaton.  In this example the
 acceptance condition did not change.  The SAT-based minimization only
@@ -568,12 +568,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm4.png :cmdline -Tpng :var txt=autfiltsm4 :exports results
+#+BEGIN_SRC dot :file autfiltsm4.svg :var txt=autfiltsm4 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfiltsm4.png]]
+[[file:autfiltsm4.svg]]
 
 
 Note that instead of naming the acceptance condition, you can actually
@@ -586,12 +586,12 @@ autfilt -S --sat-minimize='acc="Fin(0)"' output.hoa --dot=.a
 #+END_SRC
 #+RESULTS: autfiltsm5
 
-#+BEGIN_SRC dot :file autfiltsm5.png :cmdline -Tpng :var txt=autfiltsm5 :exports results
+#+BEGIN_SRC dot :file autfiltsm5.svg :var txt=autfiltsm5 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfiltsm5.png]]
+[[file:autfiltsm5.svg]]
 
 
 When forcing an acceptance condition, you should keep in mind that the
@@ -639,12 +639,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm6.png :cmdline -Tpng :var txt=autfiltsm6 :exports results
+#+BEGIN_SRC dot :file autfiltsm6.svg :var txt=autfiltsm6 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfiltsm6.png]]
+[[file:autfiltsm6.svg]]
 
 
 If we attempt to minimize it into a transition-based Büchi automaton,
@@ -689,12 +689,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm8.png :cmdline -Tpng :var txt=autfiltsm8 :exports results
+#+BEGIN_SRC dot :file autfiltsm8.svg :var txt=autfiltsm8 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfiltsm8.png]]
+[[file:autfiltsm8.svg]]
 
 
 By default, the SAT-based minimization tries to find a smaller automaton by
@@ -785,12 +785,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm9.png :cmdline -Tpng :var txt=autfiltsm9 :exports results
+#+BEGIN_SRC dot :file autfiltsm9.svg :var txt=autfiltsm9 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfiltsm9.png]]
+[[file:autfiltsm9.svg]]
 
 ... to the following, where the automaton is colored, i.e., each state
 belong to exactly one acceptance set:
@@ -823,12 +823,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file autfiltsm10.png :cmdline -Tpng :var txt=autfiltsm10 :exports results
+#+BEGIN_SRC dot :file autfiltsm10.svg :var txt=autfiltsm10 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:autfiltsm10.png]]
+[[file:autfiltsm10.svg]]
 
 * Logging statistics
 
diff --git a/doc/org/satmin.tex b/doc/org/satmin.tex
index 06b43e9d8..41d3afcb6 100644
--- a/doc/org/satmin.tex
+++ b/doc/org/satmin.tex
@@ -1,4 +1,4 @@
-\documentclass[convert={size=640}]{standalone}
+\documentclass{standalone}
 \usepackage{tikz}
 \usetikzlibrary{arrows}
 \usetikzlibrary{shadows}
@@ -21,6 +21,7 @@
 \tikzstyle{outstep}=[iostep,fill=green!20]
 \tikzstyle{errstep}=[iostep,fill=red!20]
 
+\scalebox{1.2}{
 \begin{tikzpicture}[shorten >=1pt,>=stealth',semithick,node distance=5.5mm]
 %\tikzset{callout/.style={ellipse callout, callout pointer arc=30,
 %  callout absolute pointer={#1},fill=blue!30,draw}}
@@ -93,7 +94,7 @@
 
 %\node[fill=yellow,draw,ellipse callout,thin,inner sep=0.5pt,callout pointer arc=30,,yshift=6mm,callout absolute pointer={(c1)}] at (c1) {\footnotesize 1};
 
-\end{tikzpicture}
+\end{tikzpicture}}
 \end{document}
 %%% Local Variables:
 %%% mode: latex
diff --git a/doc/org/spot.css b/doc/org/spot.css
index 99472710b..e6affbb35 100644
--- a/doc/org/spot.css
+++ b/doc/org/spot.css
@@ -1,7 +1,8 @@
+@font-face{font-family:Lato;src:local("Lato"),local("Lato-Regular"),url("https://spot.lrde.epita.fr/Lato-Regular.ttf");}
 a{color:inherit;background-color:inherit;font:inherit;text-decoration:inherit}
 a:hover{text-decoration:underline}
 /* http://paletton.com/#uid=33i0X0kz3BrkeHdpSD1C7r1FAlb */
-body{font-family:Arial, sans-serif;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em;background-image:url(/img/spot64.png);background-repeat:no-repeat;background-position:.5em .5em}
+body{font-family:Lato, sans-serif;font-size:12pt;font-weight:normal;max-width:62em;margin:auto;padding:0 .5em;background-image:url(/img/spot64.png);background-repeat:no-repeat;background-position:.5em .5em}
 body.man{padding:0 .5em 3em .5em}
 body #content{padding-top:45px}
 body pre{background:#fbfbfb;border:none;font-family:monospace, courier}
@@ -23,6 +24,7 @@ pre.src-python:before{content:'Python'}
 pre.src-C\+\+:before{content:'C++'}
 pre.src-hoa:before{content:'HOA';border-color:#d70079}
 img{max-width:100%}
+svg.org-svg{width:auto;max-width:100%}
 @media screen{
 #table-of-contents{position:fixed;right:0em;top:0em;max-width:50%;max-height:80%;overflow:auto;z-index:10}
 #table-of-contents #text-table-of-contents{display:none}
diff --git a/doc/org/tut11.org b/doc/org/tut11.org
index 703664a73..8a3843663 100644
--- a/doc/org/tut11.org
+++ b/doc/org/tut11.org
@@ -17,12 +17,12 @@ immediately after *red*.
 ltl2tgba -D -M '!F(red & Xyellow)' -d
 #+END_SRC
 
-#+BEGIN_SRC dot :file tut11a.png :cmdline -Tpng :var txt=tut11a :exports results
+#+BEGIN_SRC dot :file tut11a.svg :var txt=tut11a :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut11a.png]]
+[[file:tut11a.svg]]
 
 This monitor stays in the initial state until *red* becomes true, it
 can then wait in the second state while *red* holds and *yellow* does
@@ -191,12 +191,12 @@ Nonetheless, we can still build a monitor for it:
 #+BEGIN_SRC sh :results verbatim :exports none
 ltl2tgba -D -M 'G(press -> red U green)' -d
 #+END_SRC
-#+BEGIN_SRC dot :file tut11b.png :cmdline -Tpng :var txt=tut11b :exports results
+#+BEGIN_SRC dot :file tut11b.svg :var txt=tut11b :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut11b.png]]
+[[file:tut11b.svg]]
 
 
 This monitor will report violations if both *red* and *green* are off
diff --git a/doc/org/tut23.org b/doc/org/tut23.org
index 11277fa34..ad258ddd3 100644
--- a/doc/org/tut23.org
+++ b/doc/org/tut23.org
@@ -14,12 +14,12 @@ $txt
 EOF
 #+END_SRC
 
-#+BEGIN_SRC dot :file tut23-aut.png :cmdline -Tpng :var txt=tut23-dot :exports results
+#+BEGIN_SRC dot :file tut23-aut.svg :var txt=tut23-dot :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut23-aut.png]]
+[[file:tut23-aut.svg]]
 
 
 Note that the code is very similar to the [[file:tut22.org][previous example]]: in Spot an
diff --git a/doc/org/tut24.org b/doc/org/tut24.org
index 4dc646596..72fd6c302 100644
--- a/doc/org/tut24.org
+++ b/doc/org/tut24.org
@@ -40,12 +40,12 @@ EOF
 autfilt --dot=.a tut24.hoa
 #+END_SRC
 
-#+BEGIN_SRC dot :file tut24in.png :cmdline -Tpng :var txt=tut24dot :exports results
+#+BEGIN_SRC dot :file tut24in.svg :var txt=tut24dot :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut24in.png]]
+[[file:tut24in.svg]]
 
 * C++
 
diff --git a/doc/org/tut30.org b/doc/org/tut30.org
index 118c7a6f4..982a3fb09 100644
--- a/doc/org/tut30.org
+++ b/doc/org/tut30.org
@@ -54,12 +54,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file tut30in.png :cmdline -Tpng :var txt=tut30in :exports results
+#+BEGIN_SRC dot :file tut30in.svg :var txt=tut30in :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut30in.png]]
+[[file:tut30in.svg]]
 
 Our goal is to generate an equivalent Büchi automaton, preserving
 determinism if possible.  However nothing of what we will write is
@@ -138,12 +138,12 @@ digraph G {
 }
 #+end_example
 
-#+BEGIN_SRC dot :file tut30out.png :cmdline -Tpng :var txt=tut30out :exports results
+#+BEGIN_SRC dot :file tut30out.svg :var txt=tut30out :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut30out.png]]
+[[file:tut30out.svg]]
 
 In the general case transforming an automaton with a complex
 acceptance condition into a Büchi automaton can make the output
diff --git a/doc/org/tut31.org b/doc/org/tut31.org
index 86ea66b26..4dc00e8a1 100644
--- a/doc/org/tut31.org
+++ b/doc/org/tut31.org
@@ -37,12 +37,12 @@ EOF
 autfilt --dot=.a tut31.hoa
 #+END_SRC
 
-#+BEGIN_SRC dot :file tut31in.png :cmdline -Tpng :var txt=tut31dot :exports results
+#+BEGIN_SRC dot :file tut31in.svg :var txt=tut31dot :exports results
   $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut31in.png]]
+[[file:tut31in.svg]]
 
 Our goal is to transform this alternating automaton into a
 non-alternating automaton.
@@ -86,12 +86,12 @@ State: 1
 autfilt --tgba -d tut31.hoa
 #+END_SRC
 
-#+BEGIN_SRC dot :file tut31out.png :cmdline -Tpng :var txt=tut31out :exports results
+#+BEGIN_SRC dot :file tut31out.svg :var txt=tut31out :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:tut31out.png]]
+[[file:tut31out.svg]]
 
 * Python
 
diff --git a/doc/org/tut50.org b/doc/org/tut50.org
index ac6427483..88753882f 100644
--- a/doc/org/tut50.org
+++ b/doc/org/tut50.org
@@ -29,7 +29,7 @@ Spot.
 
 The picture below gives a partial view of the classes involved:
 
-#+BEGIN_SRC plantuml :file uml-explicit-classes.png
+#+BEGIN_SRC plantuml :file uml-explicit-classes.svg
   package stl {
     class "Forward Iterator" <<Concept>>
     hide "Forward Iterator" members
@@ -119,7 +119,7 @@ The picture below gives a partial view of the classes involved:
 #+END_SRC
 
 #+RESULTS:
-[[file:uml-explicit-classes.png]]
+[[file:uml-explicit-classes.svg]]
 
 
 An ω-automaton can be defined as a labeled directed graph, plus an
@@ -452,7 +452,7 @@ previous one: =twa= and =twa_graph=, but this time the focus is on the
 abstract interface defined in =twa=, not in the explicit interface
 defined in =twa_graph=.
 
-#+BEGIN_SRC plantuml :file uml-otf-classes.png
+#+BEGIN_SRC plantuml :file uml-otf-classes.svg
 package spot {
   package internal {
     class succ_iterable {
@@ -532,7 +532,7 @@ package spot {
 #+END_SRC
 
 #+RESULTS:
-[[file:uml-otf-classes.png]]
+[[file:uml-otf-classes.svg]]
 
 
 To explore a =twa=, one would first call =twa::get_init_state()=,
diff --git a/doc/org/tut51.org b/doc/org/tut51.org
index 650568610..1cf58d628 100644
--- a/doc/org/tut51.org
+++ b/doc/org/tut51.org
@@ -53,7 +53,7 @@ us with a handful of methods to implement.
 The following class diagram is a simplified picture of the reality,
 but good enough for show what we have to implement.
 
-#+BEGIN_SRC plantuml :file uml-kripke.png
+#+BEGIN_SRC plantuml :file uml-kripke.svg
   package spot {
     together {
       abstract class twa {
@@ -132,7 +132,7 @@ kripke <|-- demo_kripke
 #+END_SRC
 
 #+RESULTS:
-[[file:uml-kripke.png]]
+[[file:uml-kripke.svg]]
 
 
 ** Implementing the =state= subclass
@@ -388,12 +388,12 @@ this reason.
  }
  #+END_SRC
 
- #+BEGIN_SRC dot :file kripke-1.png :cmdline -Tpng :cmd circo :var txt=demo-1 :exportss results
+ #+BEGIN_SRC dot :file kripke-1.svg :cmd circo :var txt=demo-1 :exports results
  $txt
  #+END_SRC
 
  #+RESULTS:
- [[file:kripke-1.png]]
+ q[[file:kripke-1.svg]]
 
 * Checking a property on this state space
 
@@ -520,12 +520,12 @@ passing the option "~k~" to =print_dot()= will fix that.
   }
 #+END_SRC
 
-#+BEGIN_SRC dot :file kripke-3.png :cmdline -Tpng :cmd circo :var txt=demo-3 :exportss results
+#+BEGIN_SRC dot :file kripke-3.svg :cmd circo :var txt=demo-3 :exports results
 $txt
 #+END_SRC
 
 #+RESULTS:
-[[file:kripke-3.png]]
+[[file:kripke-3.svg]]
 
 * Possible improvements