diff --git a/src/graph/Makefile.am b/src/graph/Makefile.am
index 858cc6980..04e01c39c 100644
--- a/src/graph/Makefile.am
+++ b/src/graph/Makefile.am
@@ -24,4 +24,6 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 graphdir = $(pkgincludedir)/graph
 
 graph_HEADERS = \
-  graph.hh
+  graph.hh \
+  ngraph.hh
+
diff --git a/src/graph/ngraph.hh b/src/graph/ngraph.hh
new file mode 100644
index 000000000..0eb3c505f
--- /dev/null
+++ b/src/graph/ngraph.hh
@@ -0,0 +1,125 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche et Développement de
+// l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#ifndef SPOT_GRAPH_NGRAPH_HH
+# define SPOT_GRAPH_NGRAPH_HH
+
+#include <unordered_map>
+#include <vector>
+#include "graph.hh"
+
+namespace spot
+{
+  template <typename Graph,
+	    typename State_Name,
+	    typename Name_Hash = std::hash<State_Name>,
+	    typename Name_Equal = std::equal_to<State_Name>>
+  class named_graph
+  {
+  protected:
+    Graph& g_;
+  public:
+
+    typedef typename Graph::state state;
+    typedef typename Graph::transition transition;
+    typedef State_Name name;
+
+    typedef std::unordered_map<name, state,
+			       Name_Hash, Name_Equal> name_to_state_t;
+    name_to_state_t name_to_state;
+    typedef std::vector<name> state_to_name_t;
+    state_to_name_t state_to_name;
+
+    named_graph(Graph& g)
+      : g_(g)
+    {
+    }
+
+    Graph& graph()
+    {
+      return g_;
+    }
+
+    Graph& graph() const
+    {
+      return g_;
+    }
+
+    template <typename... Args>
+    state new_state(name n, Args&&... args)
+    {
+      auto p = name_to_state.insert(std::make_pair(n, 0U));
+      if (p.second)
+	{
+	  unsigned s = g_.new_state(std::forward<Args>(args)...);
+	  p.first->second = s;
+	  if (state_to_name.size() < s + 1)
+	    state_to_name.resize(s + 1);
+	  state_to_name[s] = n;
+	  return s;
+	}
+      return p.first->second;
+    }
+
+    state get_state(name n) const
+    {
+      return name_to_state.at(n);
+    }
+
+    name get_name(state s) const
+    {
+      return state_to_name.at(s);
+    }
+
+    template <typename... Args>
+    transition
+    new_transition(name src, name dst, Args&&... args)
+    {
+      return g_.new_transition(get_state(src), get_state(dst),
+			       std::forward<Args>(args)...);
+    }
+
+    template <typename... Args>
+    transition
+    new_transition(name src,
+		   const std::vector<State_Name>& dst, Args&&... args)
+    {
+      std::vector<State_Name> d;
+      d.reserve(dst.size());
+      for (auto n: dst)
+	d.push_back(get_state(n));
+      return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
+    }
+
+    template <typename... Args>
+    transition
+    new_transition(name src,
+		   const std::initializer_list<State_Name>& dst, Args&&... args)
+    {
+      std::vector<state> d;
+      d.reserve(dst.size());
+      for (auto n: dst)
+	d.push_back(get_state(n));
+      return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
+    }
+  };
+
+}
+
+#endif // SPOT_GRAPH_NGRAPH_HH
diff --git a/src/graphtest/Makefile.am b/src/graphtest/Makefile.am
index f1c5ba60d..2863c728e 100644
--- a/src/graphtest/Makefile.am
+++ b/src/graphtest/Makefile.am
@@ -22,11 +22,12 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
 AM_CXXFLAGS = $(WARNING_CXXFLAGS)
 LDADD = ../libspot.la
 
-noinst_PROGRAMS = graph
+noinst_PROGRAMS = graph ngraph
 
 graph_SOURCES = graph.cc
+ngraph_SOURCES = ngraph.cc
 
-TESTS = graph.test
+TESTS = graph.test ngraph.test
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/src/graphtest/ngraph.cc b/src/graphtest/ngraph.cc
new file mode 100644
index 000000000..70e324887
--- /dev/null
+++ b/src/graphtest/ngraph.cc
@@ -0,0 +1,362 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2014 Laboratoire de Recherche et Développement de
+// l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+#include <iostream>
+#include "graph/ngraph.hh"
+
+template <typename SL, typename TL>
+void
+dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n)
+{
+  out << " [label=\"" << g.state_data(n) << "\"]\n";
+}
+
+template <typename TL>
+void
+dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned)
+{
+  out << '\n';
+}
+
+template <typename SL, typename TL>
+void
+dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n,
+	  std::string name)
+{
+  out << " [label=\"" << name << "\\n" << g.state_data(n) << "\"]\n";
+}
+
+template <typename TL>
+void
+dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned,
+	  std::string name)
+{
+  out << " [label=\"" << name << "\"]\n";
+}
+
+
+template <typename SL, typename TL, typename TR>
+void
+dot_trans(std::ostream& out, const spot::digraph<SL, TL>&, TR& tr)
+{
+  out << " [label=\"" << tr.data() << "\"]\n";
+}
+
+template <typename SL, typename TR>
+void
+dot_trans(std::ostream& out, const spot::digraph<SL, void>&, TR&)
+{
+  out << '\n';
+}
+
+
+template <typename SL, typename TL>
+void
+dot(std::ostream& out, const spot::digraph<SL, TL>& g)
+{
+  out << "digraph {\n";
+  unsigned c = g.nb_states();
+  for (unsigned s = 0; s < c; ++s)
+    {
+      out << ' ' << s;
+      dot_state(out, g, s);
+      for (auto& t: g.out(s))
+	{
+	  out << ' ' << s << " -> " << t.dst;
+	  dot_trans(out, g, t);
+	}
+    }
+  out << "}\n";
+}
+
+template <typename G1, typename G2, typename G3, typename G4>
+void
+dot(std::ostream& out, const spot::named_graph<G1, G2, G3, G4>& g)
+{
+  out << "digraph {\n";
+  auto& gg = g.graph();
+  unsigned c = gg.nb_states();
+  for (unsigned s = 0; s < c; ++s)
+    {
+      out << ' ' << s;
+      dot_state(out, gg, s, g.get_name(s));
+      for (auto& t: gg.out(s))
+	{
+	  out << ' ' << s << " -> " << t.dst;
+	  dot_trans(out, gg, t);
+	}
+    }
+  out << "}\n";
+}
+
+
+bool g1(const spot::digraph<void, void>& g,
+	unsigned s, int e)
+{
+  int f = 0;
+  for (auto& t: g.out(s))
+    {
+      (void) t;
+      ++f;
+    }
+  return f == e;
+}
+
+bool f1()
+{
+  spot::digraph<void, void> g(3);
+  spot::named_graph<spot::digraph<void, void>, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1");
+  auto s2 = gg.new_state("s2");
+  auto s3 = gg.new_state("s3");
+  gg.new_transition("s1", "s2");
+  gg.new_transition("s1", "s3");
+  gg.new_transition("s2", "s3");
+  gg.new_transition("s3", "s1");
+  gg.new_transition("s3", "s2");
+  gg.new_transition("s3", "s3");
+
+  dot(std::cout, gg);
+
+  int f = 0;
+  for (auto& t: g.out(s1))
+    {
+      (void) t;
+      ++f;
+    }
+  return f == 2
+    && g1(g, s3, 3)
+    && g1(g, s2, 1)
+    && g1(g, s1, 2);
+}
+
+
+bool f2()
+{
+  spot::digraph<int, void> g(3);
+  spot::named_graph<spot::digraph<int, void>, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1", 1);
+  gg.new_state("s2", 2);
+  gg.new_state("s3", 3);
+  gg.new_transition("s1", "s2");
+  gg.new_transition("s1", "s3");
+  gg.new_transition("s2", "s3");
+  gg.new_transition("s3", "s2");
+
+  dot(std::cout, gg);
+
+  int f = 0;
+  for (auto& t: g.out(s1))
+    {
+      f += g.state_data(t.dst);
+    }
+  return f == 5;
+}
+
+bool f3()
+{
+  spot::digraph<void, int> g(3);
+  spot::named_graph<spot::digraph<void, int>, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1");
+  gg.new_state("s2");
+  gg.new_state("s3");
+  gg.new_transition("s1", "s2", 1);
+  gg.new_transition("s1", "s3", 2);
+  gg.new_transition("s2", "s3", 3);
+  gg.new_transition("s3", "s2", 4);
+
+  dot(std::cout, gg);
+
+  int f = 0;
+  for (auto& t: g.out(s1))
+    {
+      f += t.label;
+    }
+  return f == 3 && g.states().size() == 3;
+}
+
+bool f4()
+{
+  spot::digraph<int, int> g(3);
+  spot::named_graph<spot::digraph<int, int>, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1", 2);
+  gg.new_state("s2", 3);
+  gg.new_state("s3", 4);
+  gg.new_transition("s1", "s2", 1);
+  gg.new_transition("s1", "s3", 2);
+  gg.new_transition("s2", "s3", 3);
+  gg.new_transition("s3", "s2", 4);
+
+  dot(std::cout, gg);
+
+  int f = 0;
+  for (auto& t: g.out(s1))
+    {
+      f += t.label * g.state_data(t.dst);
+    }
+  return f == 11;
+}
+
+bool f5()
+{
+  typedef spot::digraph<void, std::pair<int, float>> graph_t;
+  graph_t g(3);
+  spot::named_graph<graph_t, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1");
+  gg.new_state("s2");
+  gg.new_state("s3");
+  gg.new_transition("s1", "s2", std::make_pair(1, 1.2f));
+  gg.new_transition("s1", "s3", std::make_pair(2, 1.3f));
+  gg.new_transition("s2", "s3", std::make_pair(3, 1.4f));
+  gg.new_transition("s3", "s2", std::make_pair(4, 1.5f));
+
+  int f = 0;
+  float h = 0;
+  for (auto& t: g.out(s1))
+    {
+      f += std::get<0>(t);
+      h += std::get<1>(t);
+    }
+  return f == 3 && (h > 2.49 && h < 2.51);
+}
+
+bool f6()
+{
+  typedef spot::digraph<void, std::pair<int, float>> graph_t;
+  graph_t g(3);
+  spot::named_graph<graph_t, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1");
+  gg.new_state("s2");
+  gg.new_state("s3");
+  gg.new_transition("s1", "s2", 1, 1.2f);
+  gg.new_transition("s1", "s3", 2, 1.3f);
+  gg.new_transition("s2", "s3", 3, 1.4f);
+  gg.new_transition("s3", "s2", 4, 1.5f);
+
+  int f = 0;
+  float h = 0;
+  for (auto& t: g.out(s1))
+    {
+      f += t.first;
+      h += t.second;
+    }
+  return f == 3 && (h > 2.49 && h < 2.51);
+}
+
+bool f7()
+{
+  typedef spot::digraph<int, int, true> graph_t;
+  graph_t g(3);
+  spot::named_graph<graph_t, std::string> gg(g);
+
+  auto s1 = gg.new_state("s1", 2);
+  gg.new_state("s2", 3);
+  gg.new_state("s3", 4);
+  gg.new_transition("s1", {"s2", "s3"}, 1);
+  gg.new_transition("s1", {"s3"}, 2);
+  gg.new_transition("s2", {"s3"}, 3);
+  gg.new_transition("s3", {"s2"}, 4);
+
+  int f = 0;
+  for (auto& t: g.out(s1))
+    {
+      for (auto& tt: t.dst)
+	{
+	  f += t.label * g.state_data(tt);
+	}
+    }
+  return f == 15;
+}
+
+
+struct int_pair
+{
+  int one;
+  int two;
+
+  friend std::ostream& operator<<(std::ostream& os, int_pair p)
+  {
+    os << '(' << p.one << ',' << p.two << ')';
+    return os;
+  }
+
+#if __GNUC__ <= 4 && __GNUC_MINOR__ <= 6
+  int_pair(int one, int two)
+    : one(one), two(two)
+  {
+  }
+
+  int_pair()
+  {
+  }
+#endif
+};
+
+bool f8()
+{
+  typedef spot::digraph<int_pair, int_pair> graph_t;
+  graph_t g(3);
+  spot::named_graph<graph_t, std::string> gg(g);
+  auto s1 = gg.new_state("s1", 2, 4);
+  gg.new_state("s2", 3, 6);
+  gg.new_state("s3", 4, 8);
+  gg.new_transition("s1", "s2", 1, 3);
+  gg.new_transition("s1", "s3", 2, 5);
+  gg.new_transition("s2", "s3", 3, 7);
+  gg.new_transition("s3", "s2", 4, 9);
+
+  dot(std::cout, gg);
+
+  int f = 0;
+  for (auto& t: g.out(s1))
+    {
+      f += t.one * g.state_data(t.dst).one;
+      f += t.two * g.state_data(t.dst).two;
+    }
+  return f == 69;
+}
+
+
+int main()
+{
+  bool a1 = f1();
+  bool a2 = f2();
+  bool a3 = f3();
+  bool a4 = f4();
+  bool a5 = f5();
+  bool a6 = f6();
+  bool a7 = f7();
+  bool a8 = f8();
+  std::cout << a1 << ' '
+	    << a2 << ' '
+	    << a3 << ' '
+	    << a4 << ' '
+	    << a5 << ' '
+	    << a6 << ' '
+	    << a7 << ' '
+	    << a8 << '\n';
+  return !(a1 && a2 && a3 && a4 && a5 && a6 && a7 && a8);
+}
diff --git a/src/graphtest/ngraph.test b/src/graphtest/ngraph.test
new file mode 100755
index 000000000..1ce2c6206
--- /dev/null
+++ b/src/graphtest/ngraph.test
@@ -0,0 +1,87 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2014 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+# While running some benchmark, Tomáš Babiak found that Spot took too
+# much time (i.e. >1h) to translate those six formulae.  It turns out
+# that the WDBA minimization was performed after the degeneralization
+# algorithm, while this is not necessary (WDBA will produce a BA, so
+# we may as well skip degeneralization).  Translating these formulae
+# in the test-suite ensure that they don't take too much time (the
+# buildfarm will timeout if it does).
+
+. ./defs
+
+set -e
+
+run 0 ../ngraph > stdout
+
+cat >expected <<EOF
+digraph {
+ 0 [label="s1"]
+ 0 -> 1
+ 0 -> 2
+ 1 [label="s2"]
+ 1 -> 2
+ 2 [label="s3"]
+ 2 -> 0
+ 2 -> 1
+ 2 -> 2
+}
+digraph {
+ 0 [label="s1\n1"]
+ 0 -> 1
+ 0 -> 2
+ 1 [label="s2\n2"]
+ 1 -> 2
+ 2 [label="s3\n3"]
+ 2 -> 1
+}
+digraph {
+ 0 [label="s1"]
+ 0 -> 1 [label="1"]
+ 0 -> 2 [label="2"]
+ 1 [label="s2"]
+ 1 -> 2 [label="3"]
+ 2 [label="s3"]
+ 2 -> 1 [label="4"]
+}
+digraph {
+ 0 [label="s1\n2"]
+ 0 -> 1 [label="1"]
+ 0 -> 2 [label="2"]
+ 1 [label="s2\n3"]
+ 1 -> 2 [label="3"]
+ 2 [label="s3\n4"]
+ 2 -> 1 [label="4"]
+}
+digraph {
+ 0 [label="s1\n(2,4)"]
+ 0 -> 1 [label="(1,3)"]
+ 0 -> 2 [label="(2,5)"]
+ 1 [label="s2\n(3,6)"]
+ 1 -> 2 [label="(3,7)"]
+ 2 [label="s3\n(4,8)"]
+ 2 -> 1 [label="(4,9)"]
+}
+1 1 1 1 1 1 1 1
+EOF
+
+diff stdout expected
+