diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index 8d436e94c..15288128e 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -192,6 +192,7 @@ namespace spot
       {
 	copy_acceptance_conditions_of(other);
 	copy_ap_of(other);
+	prop_copy(other, true, true, true, true);
       }
 
     virtual ~tgba_digraph()
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index 77dd713ac..5eea8ed21 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -35,6 +35,112 @@ namespace spot
 {
   namespace
   {
+    class dotty_output
+    {
+      std::ostream& os_;
+      bool opt_force_acc_trans_ = false;
+      bool opt_horizontal_ = true;
+      bool opt_name_ = true;
+      bool opt_circles_ = false;
+      bool mark_states_ = false;
+      const_tgba_digraph_ptr aut_;
+
+    public:
+      dotty_output(std::ostream& os, const char* options)
+	: os_(os)
+      {
+	if (options)
+	  while (char c = *options++)
+	    switch (c)
+	      {
+	      case 'c':
+		opt_circles_ = true;
+		break;
+	      case 'h':
+		opt_horizontal_ = true;
+		break;
+	      case 'n':
+		opt_name_ = true;
+	        break;
+	      case 'N':
+		opt_name_ = false;
+	        break;
+	      case 'v':
+		opt_horizontal_ = false;
+		break;
+	      case 't':
+		opt_force_acc_trans_ = false;
+		break;
+	      default:
+		throw std::runtime_error
+		  (std::string("unknown option for dotty(): ") + c);
+	      }
+      }
+
+      void
+      start()
+      {
+	os_ << "digraph G {\n";
+	if (opt_horizontal_)
+	  os_ << "  rankdir=LR\n";
+	if (opt_name_)
+	  if (auto n = aut_->get_named_prop<std::string>("automaton-name"))
+	    escape_str(os_ << "  label=\"", *n) << "\"\n  labelloc=\"t\"\n";
+	if (opt_circles_)
+	  os_ << "  node [shape=\"circle\"]\n";
+	os_ << "  I [label=\"\", style=invis, ";
+	os_ << (opt_horizontal_ ? "width" : "height");
+	os_ << "=0]\n  I -> " << aut_->get_init_state_number() << '\n';
+      }
+
+      void
+      end()
+      {
+	os_ << '}' << std::endl;
+      }
+
+      void
+      process_state(unsigned s)
+      {
+	os_ << "  " << s << " [label=\"" << escape_str(aut_->format_state(s))
+	    << '"';
+	if (mark_states_ && aut_->state_is_accepting(s))
+	  os_ << ", peripheries=2";
+	os_ << "]\n";
+      }
+
+      void
+      process_link(const tgba_digraph::trans_storage_t& t)
+      {
+	std::string label = bdd_format_formula(aut_->get_dict(), t.cond);
+	label = escape_str(label);
+	if (!mark_states_)
+	  if (auto a = t.acc)
+	    {
+	      label += "\\n";
+	      label += aut_->acc().format(a);
+	    }
+	os_ << "  " << t.src << " -> " << t.dst
+	    << " [label=\"" + label + "\"]\n";
+      }
+
+      void print(const const_tgba_digraph_ptr& aut)
+      {
+	aut_ = aut;
+	mark_states_ = !opt_force_acc_trans_ && aut_->has_state_based_acc();
+	start();
+	unsigned ns = aut_->num_states();
+	for (unsigned n = 0; n < ns; ++n)
+	  {
+	    process_state(n);
+	    for (auto& t: aut_->out(n))
+	      process_link(t);
+	  }
+	end();
+      }
+    };
+
+
     class dotty_bfs : public tgba_reachable_iterator_breadth_first
     {
     public:
@@ -168,10 +274,17 @@ namespace spot
 		  bool assume_sba, const char* options,
 		  dotty_decorator* dd)
   {
-    if (!dd)
-      dd = dotty_decorator::instance();
-    dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), options, dd);
-    d.run();
+    if (dd)
+      {
+	dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), options, dd);
+	d.run();
+	return os;
+      }
+    dotty_output d(os, options);
+    auto aut = make_tgba_digraph(g);
+    if (assume_sba)
+      aut->prop_state_based_acc();
+    d.print(aut);
     return os;
   }
 
diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc
index 74cdf1356..d86058993 100644
--- a/src/tgbaalgos/dupexp.cc
+++ b/src/tgbaalgos/dupexp.cc
@@ -41,6 +41,7 @@ namespace spot
       {
 	out_->copy_acceptance_conditions_of(a);
 	out_->copy_ap_of(a);
+	out_->prop_copy(a, true, true, true, true);
       }
 
       tgba_digraph_ptr
diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test
index 0013ad751..edb617122 100755
--- a/src/tgbatest/det.test
+++ b/src/tgbatest/det.test
@@ -115,22 +115,28 @@ run 0 ../ltl2tgba -H -DC -XH in.hoa > out.hoa
 run 1 ../../bin/autfilt -q --are-isomorph in.hoa out.hoa
 run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa
 
+# FIXME: State 2 and 5 are unreachable and I'd rather
+# not show them.
 run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba
 cat >ex.tgba <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="1"]
-  2 [label="1"]
-  2 -> 2 [label="1"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="1"]
+  1 [label="1"]
+  1 -> 1 [label="1"]
+  1 -> 3 [label="!a"]
+  1 -> 4 [label="!b"]
+  2 [label="2", peripheries=2]
   2 -> 3 [label="!a"]
-  2 -> 4 [label="!b"]
   3 [label="3", peripheries=2]
   3 -> 3 [label="!a"]
   4 [label="4", peripheries=2]
   4 -> 4 [label="!b"]
+  5 [label="5", peripheries=2]
+  5 -> 5 [label="1"]
 }
 EOF
 diff out.tgba ex.tgba
diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test
index 43d80f1d1..d9c106396 100755
--- a/src/tgbatest/dstar.test
+++ b/src/tgbatest/dstar.test
@@ -61,16 +61,16 @@ run 0 ../ltl2tgba -XD dra.dstar | tee stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 1 [label="a & !b"]
-  1 -> 2 [label="!a & !b"]
-  1 -> 3 [label="b"]
-  2 [label="1"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="a & !b"]
+  0 -> 1 [label="!a & !b"]
+  0 -> 2 [label="b"]
+  1 [label="1"]
+  1 -> 1 [label="1"]
+  2 [label="2"]
   2 -> 2 [label="1"]
-  3 [label="2"]
-  3 -> 3 [label="1"]
 }
 EOF
 
@@ -82,13 +82,13 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 1 [label="a & !b"]
-  1 -> 2 [label="b"]
-  2 [label="1", peripheries=2]
-  2 -> 2 [label="1"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="a & !b"]
+  0 -> 1 [label="b"]
+  1 [label="1", peripheries=2]
+  1 -> 1 [label="1"]
 }
 EOF
 
@@ -126,33 +126,33 @@ run 0 ../ltl2tgba -XDB dsa.dstar | tee stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="1"]
-  1 -> 3 [label="1"]
-  2 [label="1"]
-  2 -> 2 [label="!a"]
-  2 -> 3 [label="!a"]
-  2 -> 4 [label="a"]
-  2 -> 5 [label="a"]
-  3 [label="2"]
-  3 -> 6 [label="!a"]
-  3 -> 5 [label="a\n{0}"]
-  4 [label="3"]
-  4 -> 2 [label="!a"]
-  4 -> 3 [label="!a"]
-  4 -> 4 [label="a"]
-  4 -> 5 [label="a"]
-  5 [label="4"]
-  5 -> 6 [label="!a"]
-  5 -> 5 [label="a\n{0}"]
-  6 [label="5"]
-  6 -> 6 [label="!a"]
-  6 -> 7 [label="a"]
-  7 [label="6"]
-  7 -> 6 [label="!a"]
-  7 -> 7 [label="a"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="1"]
+  0 -> 2 [label="1"]
+  1 [label="1"]
+  1 -> 1 [label="!a"]
+  1 -> 2 [label="!a"]
+  1 -> 3 [label="a"]
+  1 -> 4 [label="a"]
+  2 [label="2"]
+  2 -> 5 [label="!a"]
+  2 -> 4 [label="a\n{0}"]
+  3 [label="3"]
+  3 -> 1 [label="!a"]
+  3 -> 2 [label="!a"]
+  3 -> 3 [label="a"]
+  3 -> 4 [label="a"]
+  4 [label="4"]
+  4 -> 5 [label="!a"]
+  4 -> 4 [label="a\n{0}"]
+  5 [label="5"]
+  5 -> 5 [label="!a"]
+  5 -> 6 [label="a"]
+  6 [label="6"]
+  6 -> 5 [label="!a"]
+  6 -> 6 [label="a"]
 }
 EOF
 
@@ -215,26 +215,26 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="!a & !b"]
-  1 -> 3 [label="a & !b"]
-  1 -> 4 [label="!a & b"]
-  1 -> 5 [label="a & b"]
-  2 [label="1"]
-  2 -> 2 [label="!b"]
-  2 -> 4 [label="b"]
-  3 [label="2", peripheries=2]
-  3 -> 2 [label="!a & !b"]
-  3 -> 3 [label="a & !b"]
-  3 -> 4 [label="!a & b"]
-  3 -> 5 [label="a & b"]
-  4 [label="3", peripheries=2]
-  4 -> 4 [label="1"]
-  5 [label="4", peripheries=2]
-  5 -> 4 [label="!a"]
-  5 -> 5 [label="a"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="!a & !b"]
+  0 -> 2 [label="a & !b"]
+  0 -> 3 [label="!a & b"]
+  0 -> 4 [label="a & b"]
+  1 [label="1"]
+  1 -> 1 [label="!b"]
+  1 -> 3 [label="b"]
+  2 [label="2", peripheries=2]
+  2 -> 1 [label="!a & !b"]
+  2 -> 2 [label="a & !b"]
+  2 -> 3 [label="!a & b"]
+  2 -> 4 [label="a & b"]
+  3 [label="3", peripheries=2]
+  3 -> 3 [label="1"]
+  4 [label="4", peripheries=2]
+  4 -> 3 [label="!a"]
+  4 -> 4 [label="a"]
 }
 EOF
 
@@ -261,13 +261,13 @@ run 0 ../ltl2tgba -XDD aut.dsa | tee stdout
 cat >expected<<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 0 [label="1"]
+  0 -> 1 [label="1"]
+  1 [label="1"]
   1 -> 1 [label="1"]
-  1 -> 2 [label="1"]
-  2 [label="1"]
-  2 -> 2 [label="1"]
 }
 EOF
 
diff --git a/src/tgbatest/ltl2tgba.test b/src/tgbatest/ltl2tgba.test
index 9fde26354..991cd0400 100755
--- a/src/tgbatest/ltl2tgba.test
+++ b/src/tgbatest/ltl2tgba.test
@@ -159,8 +159,8 @@ grep 'states: 1$' stdout
 # Make sure a monitor for F(a & F(b)) accepts everything.
 run 0 ../ltl2tgba -M -f "F(a & F(b))" | grep ' ->' > stdout
 cat >expected <<EOF
-  0 -> 1
-  1 -> 1 [label="1"]
+  I -> 0
+  0 -> 0 [label="1"]
 EOF
 cmp stdout expected
 
diff --git a/src/tgbatest/monitor.test b/src/tgbatest/monitor.test
index 712a58b5d..4c1647d27 100755
--- a/src/tgbatest/monitor.test
+++ b/src/tgbatest/monitor.test
@@ -34,12 +34,12 @@ expect()
 expect ../../bin/ltl2tgba --monitor a <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
+  I [label="", style=invis, width=0]
+  I -> 1
+  0 [label="0", peripheries=2]
+  0 -> 0 [label="1"]
   1 [label="1", peripheries=2]
-  1 -> 2 [label="a"]
-  2 [label="0", peripheries=2]
-  2 -> 2 [label="1"]
+  1 -> 0 [label="a"]
 }
 EOF
 
diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test
index 966bd9039..6bc59505b 100755
--- a/src/tgbatest/neverclaimread.test
+++ b/src/tgbatest/neverclaimread.test
@@ -134,12 +134,12 @@ run 0 ../ltl2tgba -XN input > stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0", peripheries=2]
-  1 -> 2 [label="p1"]
-  2 [label="1", peripheries=2]
-  2 -> 2 [label="1"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0", peripheries=2]
+  0 -> 1 [label="p1"]
+  1 [label="1", peripheries=2]
+  1 -> 1 [label="1"]
 }
 EOF
 
@@ -326,13 +326,13 @@ EOF
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="b"]
-  1 -> 1 [label="0"]
-  2 [label="1", peripheries=2]
-  2 -> 2 [label="1"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="b"]
+  0 -> 0 [label="0"]
+  1 [label="1", peripheries=2]
+  1 -> 1 [label="1"]
 }
 EOF
 diff stdout expected
diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test
index 62bd995d9..c77a0653f 100755
--- a/src/tgbatest/tgbaread.test
+++ b/src/tgbatest/tgbaread.test
@@ -37,14 +37,14 @@ run 0 ../tgbaread input > stdout
 cat >expected <<EOF
 digraph G {
   rankdir=LR
-  0 [label="", style=invis, width=0]
-  0 -> 1
-  1 [label="0"]
-  1 -> 2 [label="a & !b\n{0,1}"]
-  2 [label="1"]
-  2 -> 3 [label="a\n{0}"]
-  3 [label="2"]
-  3 -> 1 [label="1"]
+  I [label="", style=invis, width=0]
+  I -> 0
+  0 [label="0"]
+  0 -> 1 [label="a & !b\n{0,1}"]
+  1 [label="1"]
+  1 -> 2 [label="a\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="1"]
 }
 EOF