diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc
index ce09998ac..3e014c1bd 100644
--- a/src/tgba/bddprint.cc
+++ b/src/tgba/bddprint.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2009 Laboratoire de Recherche et Développement
+// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -36,6 +36,19 @@ namespace spot
   /// Global flag to enable Acc[x] output (instead of `x').
   static bool want_acc;
 
+  /// Global flag to enable UTF-8 output.
+  static bool utf8;
+
+  static
+  std::ostream& print_ltl(const ltl::formula* f, std::ostream& o)
+  {
+    if (utf8)
+      ltl::to_utf8_string(f, o);
+    else
+      ltl::to_string(f, o);
+    return o;
+  }
+
   /// Stream handler used by Buddy to display BDD variables.
   static void
   print_handler(std::ostream& o, int var)
@@ -52,12 +65,12 @@ namespace spot
 	    if (want_acc)
 	      {
 		o << "Acc[";
-		to_string(isi->second, o) << "]";
+		print_ltl(isi->second, o) << "]";
 	      }
 	    else
 	      {
 		o << "\"";
-		to_string(isi->second, o) << "\"";
+		print_ltl(isi->second, o) << "\"";
 	      }
 	  }
 	else
@@ -65,14 +78,16 @@ namespace spot
 	    isi = dict->now_formula_map.find(var);
 	    if (isi != dict->now_formula_map.end())
 	      {
-		o << "Now["; to_string(isi->second, o) << "]";
+		o << "Now[";
+		print_ltl(isi->second, o) << "]";
 	      }
 	    else
 	      {
 		isi = dict->now_formula_map.find(var - 1);
 		if (isi != dict->now_formula_map.end())
 		  {
-		    o << "Next["; to_string(isi->second, o) << "]";
+		    o << "Next[";
+		    print_ltl(isi->second, o) << "]";
 		  }
 		else
 		  {
@@ -202,7 +217,7 @@ namespace spot
   bdd_print_formula(std::ostream& os, const bdd_dict* d, bdd b)
   {
     const ltl::formula* f = bdd_to_formula(b, d);
-    to_string(f, os);
+    print_ltl(f, os);
     f->destroy();
     return os;
   }
@@ -237,4 +252,9 @@ namespace spot
     return os;
   }
 
+  void
+  enable_utf8()
+  {
+    utf8 = true;
+  }
 }
diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh
index e8fcc3cc4..f509a9c1d 100644
--- a/src/tgba/bddprint.hh
+++ b/src/tgba/bddprint.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2012  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -113,6 +113,8 @@ namespace spot
   std::ostream& bdd_print_table(std::ostream& os,
 				const bdd_dict* dict, bdd b);
 
+  /// \brief Enable UTF-8 output for bdd printers.
+  void enable_utf8();
 }
 
 #endif // SPOT_TGBA_BDDPRINT_HH
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index c3a3b95be..bece8aa0f 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -80,7 +80,7 @@ namespace spot
     {
     }
 
-    typedef Label Label_t;
+    typedef Label label_t;
     typedef label_hash label_hash_t;
 
     struct transition
@@ -154,12 +154,6 @@ namespace spot
     }
 
     static const int default_val;
-    static std::string to_string(int l)
-    {
-      std::stringstream ss;
-      ss << l;
-      return ss.str();
-    }
   };
 
   /// States labeled by a string
@@ -183,10 +177,6 @@ namespace spot
     }
 
     static const std::string default_val;
-    static std::string to_string(const std::string& l)
-    {
-      return l;
-    }
   };
 
   /// States labeled by a formula
@@ -210,10 +200,6 @@ namespace spot
     }
 
     static const ltl::formula* default_val;
-    static std::string to_string(const ltl::formula* l)
-    {
-      return ltl::to_string(l);
-    }
   };
 
   /// Successor iterators used by spot::tgba_explicit.
@@ -280,19 +266,22 @@ namespace spot
     bdd all_acceptance_conditions_;
   };
 
-  /// Graph implementation for automata representation
+  /// Graph implementation for explicit automgon
   /// \ingroup tgba_representation
   template<typename State, typename Type>
   class explicit_graph: public Type
   {
+  public:
+    typedef typename State::label_t label_t;
+    typedef typename State::label_hash_t label_hash_t;
+    typedef typename State::transitions_t transitions_t;
+    typedef typename State::transition transition;
+    typedef State state;
   protected:
-    typedef Sgi::hash_map<typename State::Label_t, State,
-			  typename State::label_hash_t> ls_map;
-    typedef Sgi::hash_map<const State*, typename State::Label_t,
-			  ptr_hash<State> > sl_map;
+    typedef Sgi::hash_map<label_t, State, label_hash_t> ls_map;
+    typedef Sgi::hash_map<const State*, label_t, ptr_hash<State> > sl_map;
 
   public:
-    typedef typename State::transition transition;
 
     explicit_graph(bdd_dict* dict)
       : ls_(),
@@ -319,15 +308,14 @@ namespace spot
       t.condition = bddtrue;
       t.acceptance_conditions = bddfalse;
 
-      typename State::transitions_t::iterator i =
+      typename transitions_t::iterator i =
 	source->successors.insert(source->successors.end(), t);
 
       return &*i;
     }
 
     transition*
-    create_transition(const typename State::Label_t& source,
-		      const typename State::Label_t& dest)
+    create_transition(const label_t& source, const label_t& dest)
     {
       // It's important that the source be created before the
       // destination, so the first source encountered becomes the
@@ -361,19 +349,19 @@ namespace spot
     }
 
     //old tgba explicit labelled interface
-    bool has_state(const typename State::Label_t& name)
+    bool has_state(const label_t& name)
     {
       return ls_.find(name) != ls_.end();
     }
 
-    const typename State::Label_t& get_label(const State* s) const
+    const label_t& get_label(const State* s) const
     {
       typename sl_map::const_iterator i = sl_.find(s);
       assert(i != sl_.end());
       return i->second;
     }
 
-    const typename State::Label_t& get_label(const spot::state* s) const
+    const label_t& get_label(const spot::state* s) const
     {
       const State* se = down_cast<const State*>(s);
       assert(se);
@@ -381,8 +369,7 @@ namespace spot
     }
 
     transition*
-    create_trainsition(const typename State::Label_t& source,
-		       const typename State::Label_t& dest)
+    create_trainsition(const label_t& source, const label_t& dest)
     {
       // It's important that the source be created before the
       // destination, so the first source encountered becomes the
@@ -398,7 +385,7 @@ namespace spot
       typename ls_map::iterator i;
       for (i = ls_.begin(); i != ls_.end(); ++i)
 	{
-	  typename State::transitions_t::iterator i2;
+	  typename transitions_t::iterator i2;
 	  for (i2 = i->second.successors.begin();
 	       i2 != i->second.successors.end(); ++i2)
 	    i2->acceptance_conditions = all - i2->acceptance_conditions;
@@ -411,21 +398,20 @@ namespace spot
       typename ls_map::iterator i;
       for (i = ls_.begin(); i != ls_.end(); ++i)
       {
-	typename State::transitions_t::iterator t1;
+	typename transitions_t::iterator t1;
 	for (t1 = i->second.successors.begin();
 	     t1 != i->second.successors.end(); ++t1)
 	{
 	  bdd acc = t1->acceptance_conditions;
-	  const state_explicit<typename State::Label_t,
-			       typename State::label_hash_t>* dest = t1->dest;
+	  const state_explicit<label_t, label_hash_t>* dest = t1->dest;
 
 	  // Find another transition with the same destination and
 	  // acceptance conditions.
-	  typename State::transitions_t::iterator t2 = t1;
+	  typename transitions_t::iterator t2 = t1;
 	  ++t2;
 	  while (t2 != i->second.successors.end())
 	  {
-	    typename State::transitions_t::iterator t2copy = t2++;
+	    typename transitions_t::iterator t2copy = t2++;
 	    if (t2copy->acceptance_conditions == acc && t2copy->dest == dest)
 	    {
 	      t1->condition |= t2copy->condition;
@@ -438,7 +424,7 @@ namespace spot
 
     /// Return the state_explicit for \a name, creating the state if
     /// it does not exist.
-    State* add_state(const typename State::Label_t& name)
+    State* add_state(const label_t& name)
     {
       typename ls_map::iterator i = ls_.find(name);
       if (i == ls_.end())
@@ -458,7 +444,7 @@ namespace spot
     }
 
     State*
-    set_init_state(const typename State::Label_t& state)
+    set_init_state(const label_t& state)
     {
       State* s = add_state(state);
       init_ = s;
@@ -472,14 +458,14 @@ namespace spot
 
       while (i != ls_.end())
       {
-	typename State::Label_t s = i->first;
+	label_t s = i->first;
 
 	// Do not erase the same state twice(Because of possible aliases).
 	if (sl_.erase(&(i->second)))
 	  i->second.destroy();
 
 	++i;
-	destroy_key<typename State::Label_t> dest;
+	destroy_key<label_t> dest;
 	dest.destroy(s);
       }
 
@@ -515,21 +501,33 @@ namespace spot
 					       ->all_acceptance_conditions());
     }
 
-    //no need?
+
+    typedef std::string (*to_string_func_t)(const label_t& t);
+
+    void set_to_string_func(to_string_func_t f)
+    {
+      to_string_func_ = f;
+    }
+
+    to_string_func_t get_to_string_func() const
+    {
+      return to_string_func_;
+    }
+
     virtual std::string format_state(const spot::state* state) const
     {
       const State* se = down_cast<const State*>(state);
       assert(se);
       typename sl_map::const_iterator i = sl_.find(se);
       assert(i != sl_.end());
-      return State::to_string(i->second);
+      assert(to_string_func_);
+      return to_string_func_(i->second);
     }
 
     /// old implementation in tgba_explicit_string
     /// Create an alias for a state.  Any reference to \a alias_name
     /// will act as a reference to \a real_name.
-    void add_state_alias(const typename State::Label_t& alias,
-			 const typename State::Label_t& real)
+    void add_state_alias(const label_t& alias, const label_t& real)
     {
       ls_[alias] = *(add_state(real));
     }
@@ -614,7 +612,7 @@ namespace spot
       typename explicit_graph<State, tgba>::ls_map::iterator i;
       for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
 	{
-	  typename State::transitions_t::iterator i2;
+	  typename transitions_t::iterator i2;
 	  for (i2 = i->second.successors.begin();
 	       i2 != i->second.successors.end(); ++i2)
 	    i2->acceptance_conditions &= neg;
@@ -639,11 +637,11 @@ namespace spot
     {
       const State* s = down_cast<const State*>(in);
       assert(s);
-      const typename State::transitions_t& st = s->successors;
+      const transitions_t& st = s->successors;
 
       bdd res = bddfalse;
 
-      typename State::transitions_t::const_iterator i;
+      typename transitions_t::const_iterator i;
       for (i = st.begin(); i != st.end(); ++i)
 	res |= i->condition;
 
@@ -654,11 +652,11 @@ namespace spot
     {
       const State* s = down_cast<const State*>(in);
       assert(s);
-      const typename State::transitions_t& st = s->successors;
+      const transitions_t& st = s->successors;
 
       bdd res = bddtrue;
 
-      typename State::transitions_t::const_iterator i;
+      typename transitions_t::const_iterator i;
       for (i = st.begin(); i != st.end(); ++i)
 	res &= bdd_support(i->condition);
 
@@ -674,17 +672,14 @@ namespace spot
     mutable bdd all_acceptance_conditions_;
     mutable bool all_acceptance_conditions_computed_;
     bdd neg_acceptance_conditions_;
+    to_string_func_t to_string_func_;
   };
 
   template <typename State>
   class tgba_explicit: public explicit_graph<State, tgba>
   {
   public:
-    typedef typename State::transition transition;
-    typedef State state;
-
-    tgba_explicit(bdd_dict* dict):
-      explicit_graph<State,tgba>(dict)
+    tgba_explicit(bdd_dict* dict): explicit_graph<State,tgba>(dict)
     {
     }
 
@@ -702,11 +697,7 @@ namespace spot
   class sba_explicit: public explicit_graph<State, sba>
   {
   public:
-    typedef typename State::transition transition;
-    typedef State state;
-
-    sba_explicit(bdd_dict* dict):
-      explicit_graph<State, sba>(dict)
+    sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
     {
     }
 
@@ -741,15 +732,90 @@ namespace spot
   };
 
 
+  // It is tempting to write
+  //
+  // template<template<typename T>class graph, typename Type>
+  // class explicit_conf: public graph<T>
+  //
+  // to simplify the typedefs at the end of the file, however swig
+  // cannot parse this syntax.
+
+  /// Configuration of graph automata
+  /// \ingroup tgba_representation
+  template<class graph, typename Type>
+  class explicit_conf: public graph
+  {
+  public:
+    explicit_conf(bdd_dict* d): graph(d)
+    {
+      set_to_string_func(to_string);
+    };
+
+    static std::string to_string(const typename Type::label_t& l)
+    {
+      std::stringstream ss;
+      ss << l;
+      return ss.str();
+    }
+  };
+
+  template<class graph>
+  class explicit_conf<graph, state_explicit_string>: public graph
+  {
+  public:
+    explicit_conf(bdd_dict* d): graph(d)
+    {
+      set_to_string_func(to_string);
+    };
+
+    static std::string to_string(const std::string& l)
+    {
+      return l;
+    }
+  };
+
+  template<class graph>
+  class explicit_conf<graph, state_explicit_formula>: public graph
+  {
+  public:
+    explicit_conf(bdd_dict* d): graph(d)
+    {
+      set_to_string_func(to_string);
+    };
+
+    // Enable UTF8 output for the formulae that label states.
+    void enable_utf8()
+    {
+      set_to_string_func(to_utf8_string);
+    }
+
+    static std::string to_string(const ltl::formula* const& l)
+    {
+      return ltl::to_string(l);
+    }
+
+    static std::string to_utf8_string(const ltl::formula* const& l)
+    {
+      return ltl::to_utf8_string(l);
+    }
+  };
+
+
   // Typedefs for tgba
-  typedef tgba_explicit<state_explicit_string> tgba_explicit_string;
-  typedef tgba_explicit<state_explicit_formula> tgba_explicit_formula;
-  typedef tgba_explicit<state_explicit_number> tgba_explicit_number;
+  typedef explicit_conf<tgba_explicit<state_explicit_string>,
+			state_explicit_string> tgba_explicit_string;
+  typedef explicit_conf<tgba_explicit<state_explicit_formula>,
+			state_explicit_formula> tgba_explicit_formula;
+  typedef explicit_conf<tgba_explicit<state_explicit_number>,
+			state_explicit_number> tgba_explicit_number;
 
   // Typedefs for sba
-  typedef sba_explicit<state_explicit_string> sba_explicit_string;
-  typedef sba_explicit<state_explicit_formula> sba_explicit_formula;
-  typedef sba_explicit<state_explicit_number> sba_explicit_number;
+  typedef explicit_conf<sba_explicit<state_explicit_string>,
+			state_explicit_string> sba_explicit_string;
+  typedef explicit_conf<sba_explicit<state_explicit_formula>,
+			state_explicit_formula> sba_explicit_formula;
+  typedef explicit_conf<sba_explicit<state_explicit_number>,
+			state_explicit_number> sba_explicit_number;
 }
 
 #endif // SPOT_TGBA_TGBAEXPLICIT_HH
diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index f6be911f9..f125dcb72 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -24,10 +24,12 @@
 #include <ostream>
 #include "tgba/tgba.hh"
 #include "dotty.hh"
+#include "dottydec.hh"
 #include "tgba/bddprint.hh"
 #include "reachiter.hh"
 #include "misc/escape.hh"
 #include "tgba/tgbatba.hh"
+#include "tgba/formula2bdd.hh"
 
 namespace spot
 {
@@ -126,6 +128,8 @@ namespace spot
   dotty_reachable(std::ostream& os, const tgba* g,
 		  bool assume_sba, dotty_decorator* dd)
   {
+    if (!dd)
+      dd = dotty_decorator::instance();
     dotty_bfs d(os, g, assume_sba, dd);
     d.run();
     return os;
diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh
index 71901d0eb..caeac0d61 100644
--- a/src/tgbaalgos/dotty.hh
+++ b/src/tgbaalgos/dotty.hh
@@ -1,4 +1,7 @@
-// Copyright (C) 2003, 2004, 2011  Laboratoire d'Informatique de Paris 6 (LIP6),
+// -*- coding: utf-
+// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de
+// l'Epita (LRDE).
+// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -22,27 +25,29 @@
 #ifndef SPOT_TGBAALGOS_DOTTY_HH
 # define SPOT_TGBAALGOS_DOTTY_HH
 
-#include "dottydec.hh"
 #include <iosfwd>
 
 namespace spot
 {
   class tgba;
+  class dotty_decorator;
 
   /// \brief Print reachable states in dot format.
   /// \ingroup tgba_io
   ///
-  /// If assume_sba is set, this assumes that the automaton
+  /// If \a assume_sba is set, this assumes that the automaton
   /// is an SBA and use double elipse to mark accepting states.
   ///
   /// The \a dd argument allows to customize the output in various
   /// ways.  See \ref tgba_dotty "this page" for a list of available
-  /// decorators.
+  /// decorators.  If no decorator is specified, the dotty_decorator
+  /// is used.
+  /// labels the transitions are encoded in UTF-8.
   std::ostream&
   dotty_reachable(std::ostream& os,
 		  const tgba* g,
 		  bool assume_sba = false,
-		  dotty_decorator* dd = dotty_decorator::instance());
+		  dotty_decorator* dd = 0);
 }
 
 #endif // SPOT_TGBAALGOS_DOTTY_HH
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 884d1976e..58564f0c0 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -266,6 +266,7 @@ syntax(char* prog)
 	    << "Miscellaneous options:" << std::endl
 	    << "  -0    produce minimal output dedicated to the paper"
 	    << std::endl
+	    << "  -8    output UTF-8 formulae" << std::endl
 	    << "  -d    turn on traces during parsing" << std::endl
             << "  -T    time the different phases of the translation"
 	    << std::endl
@@ -281,6 +282,7 @@ main(int argc, char** argv)
 
   bool debug_opt = false;
   bool paper_opt = false;
+  bool utf8_opt = false;
   enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
   enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
   enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
@@ -304,7 +306,7 @@ main(int argc, char** argv)
   spot::ltl::ltl_simplifier_options redopt(false, false, false, false, false);
   bool scc_filter_all = false;
   bool symbolic_scc_pruning = false;
-  bool display_reduce_form = false;
+  bool display_reduced_form = false;
   bool post_branching = false;
   bool fair_loop_approx = false;
   bool graph_run_opt = false;
@@ -339,6 +341,11 @@ main(int argc, char** argv)
 	{
 	  paper_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-8"))
+	{
+	  utf8_opt = true;
+	  spot::enable_utf8();
+	}
       else if (!strcmp(argv[formula_index], "-a"))
 	{
 	  output = 2;
@@ -609,7 +616,7 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[formula_index], "-rd"))
 	{
-	  display_reduce_form = true;
+	  display_reduced_form = true;
 	}
       else if (!strcmp(argv[formula_index], "-RDS"))
         {
@@ -772,9 +779,9 @@ main(int argc, char** argv)
 
   if (f || from_file)
     {
-      const spot::tgba_bdd_concrete* concrete = 0;
+      spot::tgba_bdd_concrete* concrete = 0;
       const spot::tgba* to_free = 0;
-      const spot::tgba* a = 0;
+      spot::tgba* a = 0;
 
       if (from_file)
 	{
@@ -822,8 +829,13 @@ main(int argc, char** argv)
 	      f->destroy();
 	      tm.stop("reducing formula");
 	      f = t;
-	      if (display_reduce_form)
-		std::cout << spot::ltl::to_string(f) << std::endl;
+	      if (display_reduced_form)
+		{
+		  if (utf8_opt)
+		    std::cout << spot::ltl::to_utf8_string(f) << std::endl;
+		  else
+		    std::cout << spot::ltl::to_string(f) << std::endl;
+		}
 	    }
 
 	  if (f->is_psl_formula()
@@ -900,14 +912,13 @@ main(int argc, char** argv)
       if (scc_filter)
 	{
 	  tm.start("reducing A_f w/ SCC");
-	  a = aut_scc = spot::scc_filter(a, scc_filter_all);
+	  aut_scc = a = spot::scc_filter(a, scc_filter_all);
 	  tm.stop("reducing A_f w/ SCC");
 	}
 
-      const spot::tgba_tba_proxy* degeneralized = 0;
-      const spot::tgba_sgba_proxy* state_labeled = 0;
+      const spot::tgba* degeneralized = 0;
 
-      const spot::tgba* minimized = 0;
+      spot::tgba* minimized = 0;
       if (opt_minimize)
 	{
 	  tm.start("obligation minimization");
@@ -961,39 +972,39 @@ main(int argc, char** argv)
 	{
 	  if (degeneralize_opt == DegenTBA)
 	    {
-	      a = degeneralized = new spot::tgba_tba_proxy(a);
+	      degeneralized = a = new spot::tgba_tba_proxy(a);
 	    }
 	  else if (degeneralize_opt == DegenSBA)
 	    {
-	      a = degeneralized = new spot::tgba_sba_proxy(a);
+	      degeneralized = a = new spot::tgba_sba_proxy(a);
 	      assume_sba = true;
 	    }
 	  else if (labeling_opt == StateLabeled)
 	    {
-	      a = state_labeled = new spot::tgba_sgba_proxy(a);
+	      degeneralized = a = new spot::tgba_sgba_proxy(a);
 	    }
 	}
 
       if (opt_monitor)
 	{
 	  tm.start("Monitor minimization");
-	  a = minimized = minimize_monitor(a);
+	  minimized = a = minimize_monitor(a);
 	  tm.stop("Monitor minimization");
 	  assume_sba = false; 	// All states are accepting, so double
 				// circles in the dot output are
 				// pointless.
 	}
 
-      const spot::tgba_explicit_string* expl = 0;
+      const spot::tgba* expl = 0;
       switch (dupexp)
 	{
 	case NoneDup:
 	  break;
 	case BFS:
-	  a = expl = tgba_dupexp_bfs(a);
+	  expl = a = tgba_dupexp_bfs(a);
 	  break;
 	case DFS:
-	  a = expl = tgba_dupexp_dfs(a);
+	  expl = a = tgba_dupexp_dfs(a);
 	  break;
 	}
 
@@ -1001,7 +1012,7 @@ main(int argc, char** argv)
 
       if (system)
         {
-          a = product = product_to_free = new spot::tgba_product(system, a);
+          product = product_to_free = a = new spot::tgba_product(system, a);
 
 	  assume_sba = false;
 
@@ -1013,12 +1024,12 @@ main(int argc, char** argv)
             degeneralize_opt = DegenTBA;
           if (degeneralize_opt == DegenTBA)
 	    {
-	      a = product = product_degeneralized =
+	      product = product_degeneralized = a =
 		new spot::tgba_tba_proxy(product);
 	    }
           else if (degeneralize_opt == DegenSBA)
 	    {
-	      a = product = product_degeneralized =
+	      product = product_degeneralized = a =
 		new spot::tgba_sba_proxy(product);
 	      assume_sba = true;
 	    }
@@ -1047,6 +1058,11 @@ main(int argc, char** argv)
 	  a = new spot::future_conditions_collector(a, true);
 	}
 
+      if (utf8_opt)
+	if (spot::tgba_explicit_formula* tef =
+	    dynamic_cast<spot::tgba_explicit_formula*>(a))
+	  tef->enable_utf8();
+
       if (output != -1)
 	{
 	  tm.start("producing output");
@@ -1266,7 +1282,7 @@ main(int argc, char** argv)
 				{
 				  spot::tgba* ar =
 				    spot::tgba_run_to_tgba(a, run);
-				  spot::dotty_reachable(std::cout, ar);
+				  spot::dotty_reachable(std::cout, ar, false);
 				  delete ar;
 				}
 			      else
@@ -1301,7 +1317,6 @@ main(int argc, char** argv)
       delete minimized;
       delete degeneralized;
       delete aut_scc;
-      delete state_labeled;
       delete to_free;
       delete echeck_inst;
       delete temp_dir_sim;
diff --git a/wrap/python/spot.i b/wrap/python/spot.i
index 04df12d10..05f566b48 100644
--- a/wrap/python/spot.i
+++ b/wrap/python/spot.i
@@ -213,9 +213,23 @@ using namespace spot;
   spot::explicit_graph<state_explicit_number, tgba>;
 %template(explicit_graph__formula_tgba)
   spot::explicit_graph<state_explicit_formula, tgba>;
-%template(tgba_explicit__string) spot::tgba_explicit<state_explicit_string>;
-%template(tgba_explicit__number) spot::tgba_explicit<state_explicit_number>;
-%template(tgba_explicit__formula) spot::tgba_explicit<state_explicit_formula>;
+
+%template(explicit_string_tgba)
+  spot::explicit_graph<state_explicit_string, tgba>;
+%template(explicit_number_tgba)
+  spot::tgba_explicit<state_explicit_formula>;
+%template(explicit__number_tgba)
+  spot::tgba_explicit<state_explicit_number>;
+
+%template(explicit_string__tgba)
+  spot::explicit_conf<tgba_explicit<state_explicit_string>,
+                      state_explicit_string>;
+%template(explicit_number__tgba)
+  spot::explicit_conf<tgba_explicit<state_explicit_number>,
+		      state_explicit_number>;
+%template(explicit_formula__tgba)
+  spot::explicit_conf<tgba_explicit<state_explicit_formula>,
+		      state_explicit_formula>;
 
 %include "tgbaalgos/dottydec.hh"
 %include "tgbaalgos/dotty.hh"
@@ -302,6 +316,14 @@ minimize_obligation_new(const spot::tgba* a, const spot::ltl::formula* f)
     return res;
 }
 
+void
+tgba_enable_utf8(spot::tgba* a)
+{
+  if (spot::tgba_explicit_formula* tef =
+      dynamic_cast<spot::tgba_explicit_formula*>(a))
+    tef->enable_utf8();
+}
+
 spot::ltl::parse_error_list
 empty_parse_error_list()
 {