diff --git a/README b/README
index b6d127ee5..73e549914 100644
--- a/README
+++ b/README
@@ -148,6 +148,8 @@ src/ Sources for libspot.
dstarparse/ Parser for the output of ltl2dstar.
eltlparse/ Parser for ELTL formulae.
eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
+ graph/ Graph representations.
+ graphtest/ Graph representations.
kripke/ Kripke Structure interface.
kripkeparse/ Parser for explicit Kripke.
kripketest/ Tests for kripke explicit.
diff --git a/configure.ac b/configure.ac
index 2970c4acc..9410b3fac 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1,9 +1,9 @@
# -*- coding: utf-8 -*-
# Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
# de Recherche et Développement de l'Epita (LRDE).
-# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
-# Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
-# Pierre et Marie Curie.
+# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
+# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
+# Coopératifs (SRC), Université Pierre et Marie Curie.
#
# This file is part of Spot, a model checking library.
#
@@ -181,6 +181,9 @@ AC_CONFIG_FILES([
src/eltltest/defs
src/eltltest/Makefile
src/kripke/Makefile
+ src/graph/Makefile
+ src/graphtest/Makefile
+ src/graphtest/defs
src/ltlast/Makefile
src/ltlenv/Makefile
src/ltlparse/Makefile
diff --git a/src/Makefile.am b/src/Makefile.am
index a7aba7799..5a2302b22 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,6 +1,6 @@
## -*- coding: utf-8 -*-
-## Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
-## Développement de l'Epita (LRDE).
+## Copyright (C) 2009, 2010, 2012, 2013, 2014 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
## et Marie Curie.
@@ -25,10 +25,10 @@ AUTOMAKE_OPTIONS = subdir-objects
# List directories in the order they must be built. Keep tests at the
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
-SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
- tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
+SUBDIRS = misc priv ltlenv ltlast ltlvisit ltlparse eltlparse graph \
+ tgba tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
neverparse kripkeparse dstarparse . bin ltltest eltltest \
- tgbatest sabatest kripketest sanity
+ graphtest tgbatest sabatest kripketest sanity
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
diff --git a/src/graph/Makefile.am b/src/graph/Makefile.am
new file mode 100644
index 000000000..858cc6980
--- /dev/null
+++ b/src/graph/Makefile.am
@@ -0,0 +1,27 @@
+## -*- 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 .
+
+
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+graphdir = $(pkgincludedir)/graph
+
+graph_HEADERS = \
+ graph.hh
diff --git a/src/graph/graph.hh b/src/graph/graph.hh
new file mode 100644
index 000000000..17c1356cc
--- /dev/null
+++ b/src/graph/graph.hh
@@ -0,0 +1,371 @@
+// -*- 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 .
+
+#ifndef SPOT_GRAPH_GRAPH_HH
+# define SPOT_GRAPH_GRAPH_HH
+
+#include
+#include
+#include
+
+
+namespace spot
+{
+ template
+ class digraph;
+
+ namespace internal
+ {
+ // The boxed_label class stores Data as an attribute called
+ // "label" if boxed is true. It is an empty class if Data is
+ // void, and it simply inherits from Data if boxed is false.
+ //
+ // The data() method offers an homogeneous access to the Data
+ // instance.
+
+ template ::value>
+ struct boxed_label
+ {
+ Data label;
+
+ template
+ boxed_label(Args&&... args):
+ label{std::forward(args)...}
+ {
+ }
+
+ // if Data is a POD type, G++ 4.8.2 wants default values for all
+ // label fields unless we define this default constructor here.
+ explicit boxed_label()
+ {
+ }
+
+ Data& data()
+ {
+ return label;
+ }
+
+ const Data& data() const
+ {
+ return label;
+ }
+ };
+
+ template <>
+ struct boxed_label
+ {
+ };
+
+ template
+ struct boxed_label: public Data
+ {
+ template
+ boxed_label(Args&&... args):
+ Data{std::forward(args)...}
+ {
+ }
+
+ // if Data is a POS type, G++ 4.8.2 wants default values for all
+ // label fields unless we define this default constructor here.
+ explicit boxed_label()
+ {
+ }
+
+ Data& data()
+ {
+ return *this;
+ }
+
+ const Data& data() const
+ {
+ return *this;
+ }
+ };
+
+ //////////////////////////////////////////////////
+ // State storage for digraphs
+ //////////////////////////////////////////////////
+
+ // We have two implementations, one with attached State_Data, and
+ // one without.
+
+ template
+ struct distate_storage: public State_Data
+ {
+ Transition succ; // First outgoing transition (used when iterating)
+ Transition succ_tail; // Last outgoing transition (used for
+ // appending new transitions)
+
+ template
+ distate_storage(Args&&... args):
+ State_Data{std::forward(args)...},
+ succ(0),
+ succ_tail(0)
+ {
+ }
+ };
+
+ //////////////////////////////////////////////////
+ // Transition storage
+ //////////////////////////////////////////////////
+
+ // Again two implementation: one with label, and one without.
+
+ template
+ struct trans_storage: public Trans_Data
+ {
+ typedef Transition transition;
+
+ State dst; // destination
+ Transition next_succ; // next outgoing transition with same
+ // source, or 0
+ explicit trans_storage()
+ : Trans_Data{}
+ {
+ }
+
+ template
+ trans_storage(State dst, Transition next_succ, Args&&... args)
+ : Trans_Data{std::forward(args)...},
+ dst(dst), next_succ(next_succ)
+ {
+ }
+ };
+
+ //////////////////////////////////////////////////
+ // Transition iterator
+ //////////////////////////////////////////////////
+
+ // This holds a graph and a transition number that is the start of
+ // a list, and it iterates over all the trans_storage_t elements
+ // of that list.
+
+ template
+ class trans_iterator
+ {
+ public:
+ typedef typename Graph::transition transition;
+ typedef typename Graph::trans_storage_t trans_storage_t;
+
+ trans_iterator(Graph* g, transition t): t_(t), g_(g)
+ {
+ }
+
+ bool operator==(trans_iterator o)
+ {
+ return t_ == o.t_;
+ }
+
+ bool operator!=(trans_iterator o)
+ {
+ return t_ != o.t_;
+ }
+
+ typename std::conditional::value,
+ const trans_storage_t&,
+ trans_storage_t&>::type
+ operator*()
+ {
+ return g_->transitions_[t_];
+ }
+
+ trans_iterator operator++()
+ {
+ t_ = operator*().next_succ;
+ return *this;
+ }
+
+ trans_iterator operator++(int)
+ {
+ trans_iterator ti = *this;
+ t_ = operator*().next_succ;
+ return ti;
+ }
+
+ protected:
+ transition t_;
+ Graph* g_;
+ };
+
+ //////////////////////////////////////////////////
+ // State OUT
+ //////////////////////////////////////////////////
+
+ // Fake container listing the outgoing transitions of a state.
+
+ template
+ class state_out
+ {
+ public:
+ typedef typename Graph::transition transition;
+ state_out(Graph* g, transition t):
+ t_(t), g_(g)
+ {
+ }
+
+ trans_iterator begin()
+ {
+ return {g_, t_};
+ }
+
+ trans_iterator end()
+ {
+ return {nullptr, 0};
+ }
+
+ protected:
+ transition t_;
+ Graph* g_;
+ };
+
+ }
+
+ // The actual graph implementation
+
+ template
+ class digraph
+ {
+ friend class internal::trans_iterator;
+ friend class internal::trans_iterator;
+ public:
+ static constexpr bool alternating()
+ {
+ return Alternating;
+ }
+
+ // Extra data to store on each state or transition.
+ typedef State_Data state_data_t;
+ typedef Trans_Data trans_data_t;
+
+ // State and transitions are identified by their indices in some
+ // vector.
+ typedef unsigned state;
+ typedef unsigned transition;
+
+ // The type of an output state (when seen from a transition)
+ // depends on the kind of graph we build
+ typedef typename std::conditional,
+ state>::type out_state;
+
+ typedef internal::distate_storage>
+ state_storage_t;
+ typedef internal::trans_storage>
+ trans_storage_t;
+ typedef std::vector state_vector;
+ typedef std::vector trans_vector;
+ protected:
+ state_vector states_;
+ trans_vector transitions_;
+
+ public:
+ /// \brief construct an empty graph
+ ///
+ /// Construct an empty graph, and reserve space for \a max_states
+ /// states and \a max_trans transitions. These are not hard
+ /// limits, but just hints to pre-allocate a data structure that
+ /// may hold that much items.
+ digraph(unsigned max_states = 10, unsigned max_trans = 0)
+ {
+ states_.reserve(max_states);
+ if (max_trans == 0)
+ max_trans = max_states * 2;
+ transitions_.reserve(max_trans + 1);
+ // Transition number 0 is not used, because we use this index
+ // to mark the absence of a transition.
+ transitions_.resize(1);
+ }
+
+ template
+ state new_state(Args&&... args)
+ {
+ state s = states_.size();
+ states_.emplace_back(std::forward(args)...);
+ return s;
+ }
+
+ // May not be called on states with no data.
+ State_Data
+ state_data(state s)
+ {
+ return states_[s].data();
+ }
+
+ // May not be called on states with no data.
+ State_Data
+ state_data(state s) const
+ {
+ return states_[s].data();
+ }
+
+ template
+ transition
+ new_transition(state src, out_state dst, Args&&... args)
+ {
+ transition t = transitions_.size();
+ transitions_.emplace_back(dst, 0, std::forward(args)...);
+
+ transition st = states_[src].succ_tail;
+ if (!st)
+ states_[src].succ = t;
+ else
+ transitions_[st].next_succ = t;
+ states_[src].succ_tail = t;
+ return t;
+ }
+
+ internal::state_out
+ out(state src)
+ {
+ return {this, states_[src].succ};
+ }
+
+ internal::state_out
+ out(state src) const
+ {
+ return {this, states_[src].succ};
+ }
+
+ unsigned nb_states() const
+ {
+ return states_.size();
+ }
+
+ unsigned nb_trans() const
+ {
+ return transitions_.size();
+ }
+
+ const state_vector& states() const
+ {
+ return states_;
+ }
+
+ state_vector& states()
+ {
+ return states_;
+ }
+
+ };
+
+}
+
+#endif // SPOT_GRAPH_GRAPH_HH
diff --git a/src/graphtest/.gitignore b/src/graphtest/.gitignore
new file mode 100644
index 000000000..7fd396885
--- /dev/null
+++ b/src/graphtest/.gitignore
@@ -0,0 +1,2 @@
+graphtest
+defs
diff --git a/src/graphtest/Makefile.am b/src/graphtest/Makefile.am
new file mode 100644
index 000000000..f1c5ba60d
--- /dev/null
+++ b/src/graphtest/Makefile.am
@@ -0,0 +1,34 @@
+## -*- 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 .
+
+
+AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+LDADD = ../libspot.la
+
+noinst_PROGRAMS = graph
+
+graph_SOURCES = graph.cc
+
+TESTS = graph.test
+
+EXTRA_DIST = $(TESTS)
+
+distclean-local:
+ rm -rf $(TESTS:.test=.dir)
diff --git a/src/graphtest/defs.in b/src/graphtest/defs.in
new file mode 100644
index 000000000..5169462fe
--- /dev/null
+++ b/src/graphtest/defs.in
@@ -0,0 +1,85 @@
+# -*- mode: shell-script; coding: utf-8 -*-
+# Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
+# et Développement de l'Epita (LRDE).
+# Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6
+# (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
+# Pierre et Marie Curie.
+#
+# 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 .
+
+# Ensure we are running from the right directory.
+test -f ./defs || {
+ echo "defs: not found in current directory" 1>&2
+ exit 1
+}
+
+# If srcdir is not set, then we are not running from `make check'.
+if test -z "$srcdir"; then
+ # compute $srcdir.
+ srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
+ test $srcdir = $0 && srcdir=.
+fi
+
+# Ensure $srcdir is set correctly.
+test -f $srcdir/defs.in || {
+ echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
+ exit 1
+}
+
+echo "== Running test $0"
+
+me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
+
+testSubDir=$me.dir
+chmod -R a+rwx $testSubDir > /dev/null 2>&1
+rm -rf $testSubDir > /dev/null 2>&1
+mkdir $testSubDir
+cd $testSubDir
+
+# Adjust srcdir now that we are in a subdirectory. We still want
+# $srcdir to point to the source directory corresponding to the build
+# directory that contains $testSubDir.
+case $srcdir in
+ [\\/$]* | ?:[\\/]* );;
+ *) srcdir=../$srcdir
+esac
+
+DOT='@DOT@'
+top_builddir='../@top_builddir@'
+VALGRIND='@VALGRIND@'
+PYTHON='@PYTHON@'
+
+run()
+{
+ expected_exitcode=$1
+ shift
+ exitcode=0
+ if test -n "$VALGRIND"; then
+ exec 6>valgrind.err
+ GLIBCPP_FORCE_NEW=1 \
+ ../../../libtool --mode=execute \
+ $VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" ||
+ exitcode=$?
+ cat valgrind.err 1>&2
+ test -z "`sed 1q valgrind.err`" || exit 50
+ rm -f valgrind.err
+ else
+ "$@" || exitcode=$?
+ fi
+ test $exitcode = $expected_exitcode || exit 1
+}
+
+set -x
diff --git a/src/graphtest/graph.cc b/src/graphtest/graph.cc
new file mode 100644
index 000000000..4a7d0bbc9
--- /dev/null
+++ b/src/graphtest/graph.cc
@@ -0,0 +1,312 @@
+// -*- 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 .
+
+
+#include
+#include "graph/graph.hh"
+
+template
+void
+dot_state(std::ostream& out, spot::digraph& g, unsigned n)
+{
+ out << " [label=\"" << g.state_data(n) << "\"]\n";
+}
+
+template
+void
+dot_state(std::ostream& out, spot::digraph&, unsigned)
+{
+ out << '\n';
+}
+
+template
+void
+dot_trans(std::ostream& out, spot::digraph&, TR& tr)
+{
+ out << " [label=\"" << tr.data() << "\"]\n";
+}
+
+template
+void
+dot_trans(std::ostream& out, spot::digraph&, TR&)
+{
+ out << '\n';
+}
+
+
+template
+void
+dot(std::ostream& out, spot::digraph& 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";
+}
+
+
+bool g1(const spot::digraph& g,
+ unsigned s, int e)
+{
+ int f = 0;
+ for (auto& t: g.out(s))
+ {
+ (void) t;
+ ++f;
+ }
+ return f == e;
+}
+
+bool f1()
+{
+ spot::digraph g(3);
+
+ auto s1 = g.new_state();
+ auto s2 = g.new_state();
+ auto s3 = g.new_state();
+ g.new_transition(s1, s2);
+ g.new_transition(s1, s3);
+ g.new_transition(s2, s3);
+ g.new_transition(s3, s1);
+ g.new_transition(s3, s2);
+ g.new_transition(s3, s3);
+
+ dot(std::cout, g);
+
+ 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 g(3);
+
+ auto s1 = g.new_state(1);
+ auto s2 = g.new_state(2);
+ auto s3 = g.new_state(3);
+ g.new_transition(s1, s2);
+ g.new_transition(s1, s3);
+ g.new_transition(s2, s3);
+ g.new_transition(s3, s2);
+
+ dot(std::cout, g);
+
+ int f = 0;
+ for (auto& t: g.out(s1))
+ {
+ f += g.state_data(t.dst);
+ }
+ return f == 5;
+}
+
+bool f3()
+{
+ spot::digraph g(3);
+
+ auto s1 = g.new_state();
+ auto s2 = g.new_state();
+ auto s3 = g.new_state();
+ g.new_transition(s1, s2, 1);
+ g.new_transition(s1, s3, 2);
+ g.new_transition(s2, s3, 3);
+ g.new_transition(s3, s2, 4);
+
+ dot(std::cout, g);
+
+ int f = 0;
+ for (auto& t: g.out(s1))
+ {
+ f += t.label;
+ }
+ return f == 3 && g.states().size() == 3;
+}
+
+bool f4()
+{
+ spot::digraph g(3);
+
+ auto s1 = g.new_state(2);
+ auto s2 = g.new_state(3);
+ auto s3 = g.new_state(4);
+ g.new_transition(s1, s2, 1);
+ g.new_transition(s1, s3, 2);
+ g.new_transition(s2, s3, 3);
+ g.new_transition(s3, s2, 4);
+
+ dot(std::cout, g);
+
+ int f = 0;
+ for (auto& t: g.out(s1))
+ {
+ f += t.label * g.state_data(t.dst);
+ }
+ return f == 11;
+}
+
+bool f5()
+{
+ spot::digraph> g(3);
+
+ auto s1 = g.new_state();
+ auto s2 = g.new_state();
+ auto s3 = g.new_state();
+ g.new_transition(s1, s2, std::make_pair(1, 1.2f));
+ g.new_transition(s1, s3, std::make_pair(2, 1.3f));
+ g.new_transition(s2, s3, std::make_pair(3, 1.4f));
+ g.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()
+{
+ spot::digraph> g(3);
+
+ auto s1 = g.new_state();
+ auto s2 = g.new_state();
+ auto s3 = g.new_state();
+ g.new_transition(s1, s2, 1, 1.2f);
+ g.new_transition(s1, s3, 2, 1.3f);
+ g.new_transition(s2, s3, 3, 1.4f);
+ g.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()
+{
+ spot::digraph g(3);
+ auto s1 = g.new_state(2);
+ auto s2 = g.new_state(3);
+ auto s3 = g.new_state(4);
+ g.new_transition(s1, {s2, s3}, 1);
+ g.new_transition(s1, {s3}, 2);
+ g.new_transition(s2, {s3}, 3);
+ g.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()
+{
+ spot::digraph g(3);
+ auto s1 = g.new_state(2, 4);
+ auto s2 = g.new_state(3, 6);
+ auto s3 = g.new_state(4, 8);
+ g.new_transition(s1, s2, 1, 3);
+ g.new_transition(s1, s3, 2, 5);
+ g.new_transition(s2, s3, 3, 7);
+ g.new_transition(s3, s2, 4, 9);
+
+ dot(std::cout, g);
+
+ 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/graph.test b/src/graphtest/graph.test
new file mode 100755
index 000000000..ca1c199a8
--- /dev/null
+++ b/src/graphtest/graph.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 .
+
+# 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 ../graph > stdout
+
+cat >expected < 1
+ 0 -> 2
+ 1
+ 1 -> 2
+ 2
+ 2 -> 0
+ 2 -> 1
+ 2 -> 2
+}
+digraph {
+ 0 [label="1"]
+ 0 -> 1
+ 0 -> 2
+ 1 [label="2"]
+ 1 -> 2
+ 2 [label="3"]
+ 2 -> 1
+}
+digraph {
+ 0
+ 0 -> 1 [label="1"]
+ 0 -> 2 [label="2"]
+ 1
+ 1 -> 2 [label="3"]
+ 2
+ 2 -> 1 [label="4"]
+}
+digraph {
+ 0 [label="2"]
+ 0 -> 1 [label="1"]
+ 0 -> 2 [label="2"]
+ 1 [label="3"]
+ 1 -> 2 [label="3"]
+ 2 [label="4"]
+ 2 -> 1 [label="4"]
+}
+digraph {
+ 0 [label="(2,4)"]
+ 0 -> 1 [label="(1,3)"]
+ 0 -> 2 [label="(2,5)"]
+ 1 [label="(3,6)"]
+ 1 -> 2 [label="(3,7)"]
+ 2 [label="(4,8)"]
+ 2 -> 1 [label="(4,9)"]
+}
+1 1 1 1 1 1 1 1
+EOF
+
+diff stdout expected
+