Template ltlast/ & ltlenv/ classes in internal/ & Add ELTL parser.

2008-03-25 16:52:06 +01:00 · 2008-03-25 16:52:06 +01:00 · 543190f2bc
commit 543190f2bc
parent 21c98c0a01
74 changed files with 4299 additions and 468 deletions
--- a/24
+++ b/24
@ -1,3 +1,27 @@
+2008-04-16  Damien Lefortier <dam@lrde.epita.fr>
+
+	* configure.ac, Makefile.am: Add src/eltltest/ support.
+	* src/eltlast/Makefile.am, src/eltlast/formula.hh,
+	src/eltlast/nfa.cc, src/eltlast/nfa.hh: Update nfa implementation.
+	* src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
+	src/eltlparse/eltlscan.ll, src/eltlparse/parsedecl.hh,
+	src/eltlparse/public.hh: Finish the parser for ELTL files.
+	* src/eltltest/Makefile.am, src/eltltest/acc.cc,
+	src/eltltest/acc.test: Add tests for the ELTL parser.
+	* src/internal/atomic_prop.hh, src/internal/atomic_prop.hxx,
+	src/internal/binop.hh, src/internal/binop.hxx,
+	src/internal/constant.hh, src/internal/constant.hxx,
+	src/internal/defaultenv.hh, src/internal/defaultenv.hxx,
+	src/internal/environment.hh, src/internal/formula.hh,
+	src/internal/formula.hxx, src/internal/multop.hh,
+	src/internal/multop.hxx, src/internal/predecl.hh,
+	src/internal/refformula.hh, src/internal/refformula.hxx,
+	src/internal/unop.hh src/internal/unop.hxx: Clean and update
+	documentation.
+	* src/ltlast/formula.hh, src/ltlenv/Makefile.am,
+	src/ltlenv/declenv.hh, src/tgbaalgos/randomgraph.hh: Fix make
+	check issues.
+
 2008-04-14  Alexandre Duret-Lutz  <adl@lrde.epita.fr>

 	Kill some FIXMEs.
--- a/configure.ac
+++ b/configure.ac
@ -79,11 +79,17 @@ AC_CONFIG_FILES([
  iface/gspn/Makefile
  iface/gspn/defs
  src/Makefile
+  src/eltlast/Makefile
+  src/eltlenv/Makefile
+  src/eltlparse/Makefile
+  src/eltltest/Makefile
+  src/eltltest/defs
  src/evtgba/Makefile
  src/evtgbaalgos/Makefile
  src/evtgbaparse/Makefile
  src/evtgbatest/Makefile
  src/evtgbatest/defs
+  src/internal/Makefile
  src/ltlast/Makefile
  src/ltlenv/Makefile
  src/ltlparse/Makefile
--- a/src/Makefile.am
+++ b/src/Makefile.am
@ -23,20 +23,21 @@ AUTOMAKE_OPTIONS = subdir-objects

 # List directories in the order they must be built.
 # Keep tests at the end.
-SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse \
+SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse internal \
+	  eltlenv eltlast eltlparse \
          tgba tgbaalgos tgbaparse \
 	  evtgba evtgbaalgos evtgbaparse . \
-	  ltltest tgbatest evtgbatest sanity
+	  ltltest eltltest tgbatest evtgbatest sanity

 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =
 libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined
 libspot_la_LIBADD =  \
  misc/libmisc.la \
-  ltlenv/libltlenv.la \
  ltlparse/libltlparse.la \
  ltlvisit/libltlvisit.la \
-  ltlast/libltlast.la \
+  eltlast/libeltlast.la \
+  eltlparse/libeltlparse.la \
  tgba/libtgba.la \
  tgbaalgos/libtgbaalgos.la \
  tgbaparse/libtgbaparse.la \
--- a/src/eltlast/Makefile.am
+++ b/src/eltlast/Makefile.am
@ -0,0 +1,44 @@
+## Copyright (C) 2008  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+eltlastdir = $(pkgincludedir)/eltlast
+
+eltlast_HEADERS = \
+  allnodes.hh \
+  atomic_prop.hh \
+  automatop.hh \
+  binop.hh \
+  constant.hh \
+  formula.hh \
+  multop.hh \
+  nfa.hh \
+  refformula.hh \
+  unop.hh \
+  visitor.hh
+
+
+noinst_LTLIBRARIES = libeltlast.la
+libeltlast_la_SOURCES = \
+  automatop.cc \
+  nfa.cc
--- a/src/eltlast/allnodes.hh
+++ b/src/eltlast/allnodes.hh
@ -0,0 +1,36 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/allnodes.hh
+/// \brief Define all ELTL node types.
+///
+/// This file is usually needed when \b defining a visitor.
+#ifndef SPOT_ELTLAST_ALLNODES_HH
+# define SPOT_ELTLAST_ALLNODES_HH
+
+# include "binop.hh"
+# include "unop.hh"
+# include "multop.hh"
+# include "atomic_prop.hh"
+# include "constant.hh"
+# include "automatop.hh"
+
+#endif // SPOT_ELTLAST_ALLNODES_HH
--- a/src/eltlast/atomic_prop.hh
+++ b/src/eltlast/atomic_prop.hh
@ -0,0 +1,42 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/atomic_prop.hh
+/// \brief ELTL atomic propositions
+#ifndef SPOT_ELTLAST_ATOMIC_PROP_HH
+# define SPOT_ELTLAST_ATOMIC_PROP_HH
+
+# include "formula.hh"
+# include "internal/atomic_prop.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief Atomic propositions.
+    /// \ingroup eltl_ast
+    typedef spot::internal::atomic_prop<eltl_t> atomic_prop;
+
+  }
+}
+
+#endif // SPOT_ELTLAST_ATOMICPROP_HH
--- a/src/eltlast/automatop.cc
+++ b/src/eltlast/automatop.cc
@ -0,0 +1,121 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "visitor.hh"
+#include "automatop.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+    automatop::automatop(vec* v)
+      : nfa_(), children_(v)
+    {
+      dump_ = "automatop(";
+      dump_ += (*v)[0]->dump();
+      for (unsigned n = 1; n < v->size(); ++n)
+	dump_ += ", " + (*v)[n]->dump();
+      dump_ += ")";
+      set_key_();
+    }
+
+    automatop::~automatop()
+    {
+      delete children_;
+    }
+
+    void
+    automatop::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    void
+    automatop::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    automatop*
+    automatop::instance(nfa::ptr nfa, formula* autop)
+    {
+      vec* v = new vec;
+      v->push_back(autop);
+      automatop* res = instance(v);
+      res->nfa_ = nfa;
+      return res;
+    }
+
+    automatop*
+    automatop::instance(formula* first, formula* second)
+    {
+      vec* v = new vec;
+      v->push_back(first);
+      v->push_back(second);
+      return instance(v);
+    }
+
+    automatop*
+    automatop::instance(vec* v)
+    {
+      // Inline children of same kind.
+      {
+	vec inlined;
+	vec::iterator i = v->begin();
+	while (i != v->end())
+	{
+	  if (automatop* p = dynamic_cast<automatop*>(*i))
+	  {
+	    unsigned ps = p->size();
+	    for (unsigned n = 0; n < ps; ++n)
+	      inlined.push_back(p->nth(n));
+	    formula::unref(*i);
+	    i = v->erase(i);
+	  }
+	  else
+	    ++i;
+	}
+	v->insert(v->end(), inlined.begin(), inlined.end());
+      }
+
+      automatop* res = new automatop(v);
+      return static_cast<automatop*>(res->ref());
+    }
+
+    unsigned
+    automatop::size() const
+    {
+      return children_->size();
+    }
+
+    const formula*
+    automatop::nth(unsigned n) const
+    {
+      return (*children_)[n];
+    }
+
+  formula*
+    automatop::nth(unsigned n)
+    {
+      return (*children_)[n];
+    }
+  }
+}
--- a/src/eltlast/automatop.hh
+++ b/src/eltlast/automatop.hh
@ -0,0 +1,84 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/automatop.hh
+/// \brief ELTL automaton operators
+#ifndef SPOT_ELTLAST_AUTOMATOP_HH
+# define SPOT_ELTLAST_AUTOMATOP_HH
+
+# include "multop.hh"
+# include "refformula.hh"
+# include "nfa.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief Automaton operators.
+    /// \ingroup eltl_ast
+    ///
+    class automatop : public ref_formula
+    {
+    public:
+      /// List of formulae.
+      typedef std::vector<formula*> vec;
+
+      /// \brief Build a spot::eltl::automatop with automaton \c nfa
+      /// and children of \c autop.
+      static automatop* instance(nfa::ptr nfa, formula* autop);
+
+      /// \brief Build a spot::eltl::automatop with two children.
+      ///
+      /// If one of the children itself is a spot::eltl::automatop,
+      /// it will be merged. This allows incremental building of
+      /// n-ary eltl::automatop.
+      static automatop* instance(formula* first, formula* second);
+
+      /// \brief Build a spot::eltl::automatop with many children.
+      static automatop* instance(vec* v);
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      /// Get the number of argument.
+      unsigned size() const;
+      /// \brief Get the nth argument.
+      ///
+      /// Starting with \a n = 0.
+      const formula* nth(unsigned n) const;
+      /// \brief Get the nth argument.
+      ///
+      /// Starting with \a n = 0.
+      formula* nth(unsigned n);
+
+    protected:
+      automatop(vec* v);
+      virtual ~automatop();
+
+    private:
+      nfa::ptr nfa_;
+      vec* children_;
+    };
+  }
+}
+
+#endif // SPOT_ELTLAST_AUTOMATOP_HH
--- a/src/eltlast/binop.hh
+++ b/src/eltlast/binop.hh
@ -0,0 +1,45 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/binop.hh
+/// \brief ELTL binary operators
+///
+/// This does not include \c AND and \c OR operators.  These are
+/// considered to be multi-operand operators (see spot::eltl::multop).
+#ifndef SPOT_ELTLAST_BINOP_HH
+# define SPOT_ELTLAST_BINOP_HH
+
+# include "formula.hh"
+# include "internal/binop.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief Binary operator.
+    /// \ingroup eltl_ast
+    typedef spot::internal::binop<eltl_t> binop;
+
+  }
+}
+
+#endif // SPOT_ELTLAST_BINOP_HH
--- a/src/eltlast/constant.hh
+++ b/src/eltlast/constant.hh
@ -0,0 +1,42 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/constant.hh
+/// \brief ELTL constants
+#ifndef SPOT_ELTLAST_CONSTANT_HH
+# define SPOT_ELTLAST_CONSTANT_HH
+
+# include "formula.hh"
+# include "internal/constant.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief A constant (True or False)
+    /// \ingroup eltl_ast
+    typedef spot::internal::constant<eltl_t> constant;
+
+  }
+}
+
+#endif // SPOT_ELTLAST_CONSTANT_HH
--- a/src/eltlast/formula.hh
+++ b/src/eltlast/formula.hh
@ -0,0 +1,96 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/formula.hh
+/// \brief ELTL formula interface
+#ifndef SPOT_ELTLAST_FORMULA_HH
+# define SPOT_ELTLAST_FORMULA_HH
+
+# include "internal/formula.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+    /// \defgroup eltl ELTL formulae
+    ///
+    /// This module gathers types and definitions related to ELTL formulae.
+
+    /// \addtogroup eltl_essential Essential ELTL types
+    /// \ingroup eltl
+
+    /// \addtogroup eltl_ast ELTL Abstract Syntax Tree
+    /// \ingroup eltl
+
+    /// Forward declarations
+    struct visitor;
+    struct const_visitor;
+
+    /// \brief An ELTL formula.
+    /// \ingroup eltl_essential
+    /// \ingroup eltl_ast
+    ///
+    /// The only way you can work with a formula is to
+    /// build a spot::eltl::visitor or spot::eltl::const_visitor.
+    struct eltl_t
+    {
+      typedef spot::eltl::visitor visitor;
+      typedef spot::eltl::const_visitor const_visitor;
+
+      enum binop { Xor, Implies, Equiv };
+      const char* binop_name(binop op) const
+      {
+	switch (op)
+      	{
+	  case Xor:
+	    return "Xor";
+	  case Implies:
+	    return "Implies";
+	  case Equiv:
+	    return "Equiv";
+      	}
+	// Unreachable code.
+	assert(0);
+	return 0;
+      }
+
+      enum unop { Not };
+      const char* unop_name(unop op) const
+      {
+	switch (op)
+	{
+	  case Not:
+	    return "Not";
+	}
+	// Unreachable code.
+	assert(0);
+	return 0;
+      }
+    };
+
+    typedef spot::internal::formula<eltl_t> formula;
+
+    typedef spot::internal::formula_ptr_less_than<eltl_t> formula_ptr_less_than;
+    typedef spot::internal::formula_ptr_hash<eltl_t> formula_ptr_hash;
+  }
+}
+
+#endif /* !SPOT_ELTLAST_FORMULA_HH_ */
--- a/src/eltlast/multop.hh
+++ b/src/eltlast/multop.hh
@ -0,0 +1,44 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/multop.hh
+/// \brief ELTL multi-operand operators
+#ifndef SPOT_ELTLAST_MULTOP_HH
+# define SPOT_ELTLAST_MULTOP_HH
+
+# include "formula.hh"
+# include "internal/multop.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief Multi-operand operators.
+    /// \ingroup eltl_ast
+    ///
+    /// These operators are considered commutative and associative.
+    typedef spot::internal::multop<eltl_t> multop;
+
+  }
+}
+
+#endif // SPOT_ELTLAST_MULTOP_HH
--- a/src/eltlast/nfa.cc
+++ b/src/eltlast/nfa.cc
@ -0,0 +1,127 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <cassert>
+#include "nfa.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+    nfa::nfa()
+      : ns_(), sn_(), init_(0), arity_(0), finals_()
+    {
+    }
+
+    nfa::~nfa()
+    {
+      ns_map::iterator i;
+      for (i = ns_.begin(); i != ns_.end(); ++i)
+      {
+	state::iterator i2;
+	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	  delete *i2;
+	delete i->second;
+      }
+    }
+
+    nfa::state*
+    nfa::add_state(const std::string& name)
+    {
+      ns_map::iterator i = ns_.find(name);
+      if (i == ns_.end())
+      {
+	state* s = new nfa::state;
+	ns_[name] = s;
+	sn_[s] = name;
+
+	if (!init_)
+	  init_ = s;
+	return s;
+      }
+      return i->second;
+    }
+
+    void
+    nfa::add_transition(const std::string& s, const std::string& d, unsigned c)
+    {
+      state* source = add_state(s);
+      nfa::transition* t = new transition;
+      t->dest = add_state(d);
+      t->cost = c;
+      source->push_back(t);
+      if (c > arity_)
+	arity_ = c;
+    }
+
+    void
+    nfa::set_init_state(const std::string& state)
+    {
+      init_ = add_state(state);
+    }
+
+    void
+    nfa::set_final(const std::string& state)
+    {
+      finals_.insert(state);
+    }
+
+    bool
+    nfa::is_final(const std::string& state)
+    {
+      return finals_.find(state) != finals_.end();
+    }
+
+    unsigned
+    nfa::arity()
+    {
+      return arity_ + 1;
+    }
+
+    const nfa::state*
+    nfa::get_init_state()
+    {
+      if (!init_)
+	add_state("empty");
+      return init_;
+    }
+
+    nfa::iterator
+    nfa::begin(const state* s) const
+    {
+      return nfa::iterator(s->begin());
+    }
+
+    nfa::iterator
+    nfa::end(const state* s) const
+    {
+      return nfa::iterator(s->end());
+    }
+
+    std::string
+    nfa::format_state(const state* s) const
+    {
+      sn_map::const_iterator i = sn_.find(s);
+      assert(i != sn_.end());
+      return i->second;
+    }
+  }
+}
--- a/src/eltlast/nfa.hh
+++ b/src/eltlast/nfa.hh
@ -0,0 +1,147 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/nfa.hh
+/// \brief NFA interface
+#ifndef SPOT_ELTLAST_NFA_HH
+# define SPOT_ELTLAST_NFA_HH
+
+# include "misc/hash.hh"
+# include <boost/shared_ptr.hpp>
+# include <list>
+# include <set>
+
+namespace spot
+{
+  namespace eltl
+  {
+    /// Forward declaration. See below.
+    class succ_iterator;
+
+    /// \brief A Nondeterministic Finite Automaton used in ELTL
+    /// automata operators.
+    /// \ingroup eltl_essential
+    class nfa
+    {
+    public:
+      struct				transition;
+      typedef std::list<transition*>	state;
+      /// Iterator over the successors of a state.
+      typedef succ_iterator		iterator;
+      typedef boost::shared_ptr<nfa>	ptr;
+
+      /// Explicit transitions.
+      struct transition
+      {
+	unsigned cost;
+      	const state* dest;
+      };
+
+      nfa();
+      ~nfa();
+
+      void
+      add_transition(const std::string& s, const std::string& d, unsigned c);
+
+      void
+      set_init_state(const std::string& state);
+      const state*
+      get_init_state();
+
+      void
+      set_final(const std::string& state);
+      bool
+      is_final(const std::string& state);
+
+      /// \brief Get the `arity' i.e. max t.cost, for each transition t.
+      unsigned
+      arity();
+
+      /// \brief Return an iterator on the first succesor (if any) of \a state.
+      ///
+      /// The usual way to do this with a \c for lopp.
+      /// \code
+      ///    for (nfa::iterator i = a.begin(state); i != a.end(state); ++i)
+      ///      ...
+      /// \endcode
+      iterator
+      begin(const state* state) const;
+
+      /// \brief Return an iterator just past the last succesor of \a state.
+      iterator
+      end(const state* state) const;
+
+      std::string
+      format_state(const state* state) const;
+
+    private:
+      state*
+      add_state(const std::string& name);
+
+      typedef Sgi::hash_map<const std::string, state*, string_hash> ns_map;
+      typedef Sgi::hash_map<const state*, std::string, ptr_hash<state> > sn_map;
+
+      ns_map ns_;
+      sn_map sn_;
+      state* init_;
+
+      unsigned arity_;
+      std::set<std::string> finals_;
+
+      /// Explicitly disllow use of implicity generated member functions
+      /// we don't want.
+      nfa(const nfa& other);
+      nfa& operator=(const nfa& other);
+    };
+
+    class succ_iterator
+    {
+    public:
+      succ_iterator(const nfa::state::const_iterator s)
+	: i_(s)
+      {
+      }
+
+      void
+      operator++()
+      {
+	++i_;
+      }
+
+      bool
+      operator!=(const succ_iterator& rhs) const
+      {
+	return i_ != rhs.i_;
+      }
+
+      const nfa::transition* operator*() const
+      {
+	return *i_;
+      }
+
+    private:
+      nfa::state::const_iterator i_;
+    };
+
+  }
+}
+
+#endif // SPOT_ELTLAST_NFA_HH_
--- a/src/eltlast/refformula.hh
+++ b/src/eltlast/refformula.hh
@ -0,0 +1,42 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/refformula.hh
+/// \brief Reference-counted ELTL formulae
+#ifndef SPOT_ELTLAST_REFFORMULA_HH
+# define SPOT_ELTLAST_REFFORMULA_HH
+
+# include "formula.hh"
+# include "internal/refformula.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief A reference-counted ELTL formula.
+    /// \ingroup eltl_ast
+    typedef spot::internal::ref_formula<eltl_t> ref_formula;
+
+  }
+}
+
+#endif // SPOT_ELTLAST_REFFORMULA_HH
--- a/src/eltlast/unop.hh
+++ b/src/eltlast/unop.hh
@ -0,0 +1,42 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/unop.hh
+/// \brief ELTL unary operators
+#ifndef SPOT_ELTLAST_UNOP_HH
+# define SPOT_ELTLAST_UNOP_HH
+
+# include "formula.hh"
+# include "internal/unop.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief Unary operators.
+    /// \ingroup eltl_ast
+    typedef spot::internal::unop<eltl_t> unop;
+
+  }
+}
+
+#endif // SPOT_ELTLAST_UNOP_HH
--- a/src/eltlast/visitor.hh
+++ b/src/eltlast/visitor.hh
@ -0,0 +1,82 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file eltlast/visitor.hh
+/// \brief ELTL visitor interface
+#ifndef SPOT_ELTLAST_VISITOR_HH
+# define SPOT_ELTLAST_VISITOR_HH
+
+# include "binop.hh"
+# include "unop.hh"
+# include "multop.hh"
+# include "atomic_prop.hh"
+# include "constant.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+    // Forward declaration.
+    struct automatop;
+
+    /// \brief Formula visitor that can modify the formula.
+    /// \ingroup eltl_essential
+    ///
+    /// Writing visitors is the prefered way
+    /// to traverse a formula, since it doesn't
+    /// involve any cast.
+    ///
+    /// If you do not need to modify the visited formula, inherit from
+    /// spot::eltl:const_visitor instead.
+    struct visitor
+    {
+      virtual ~visitor() {}
+      virtual void visit(atomic_prop* node) = 0;
+      virtual void visit(constant* node) = 0;
+      virtual void visit(binop* node) = 0;
+      virtual void visit(unop* node) = 0;
+      virtual void visit(multop* node) = 0;
+      virtual void visit(automatop* node) = 0;
+    };
+
+    /// \brief Formula visitor that cannot modify the formula.
+    ///
+    /// Writing visitors is the prefered way
+    /// to traverse a formula, since it doesn't
+    /// involve any cast.
+    ///
+    /// If you want to modify the visited formula, inherit from
+    /// spot::eltl:visitor instead.
+    struct const_visitor
+    {
+      virtual ~const_visitor() {}
+      virtual void visit(const atomic_prop* node) = 0;
+      virtual void visit(const constant* node) = 0;
+      virtual void visit(const binop* node) = 0;
+      virtual void visit(const unop* node) = 0;
+      virtual void visit(const multop* node) = 0;
+      virtual void visit(const automatop* node) = 0;
+    };
+
+  }
+}
+
+#endif // SPOT_ELTLAST_VISITOR_HH
--- a/src/eltlenv/Makefile.am
+++ b/src/eltlenv/Makefile.am
@ -0,0 +1,27 @@
+## 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.
+##
+## 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+eltlenvdir = $(pkgincludedir)/eltlenv
+
+eltlenv_HEADERS = \
+  defaultenv.hh \
+  declenv.hh \
+  environment.hh
--- a/src/eltlenv/declenv.hh
+++ b/src/eltlenv/declenv.hh
@ -0,0 +1,44 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_ELTLENV_DECLENV_HH
+# define SPOT_ELTLENV_DECLENV_HH
+
+# include "environment.hh"
+# include "internal/declenv.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief A declarative environment.
+    /// \ingroup eltl_environment
+    ///
+    /// This environment recognizes all atomic propositions
+    /// that have been previously declared.  It will reject other.
+    typedef spot::internal::declarative_environment<eltl_t>
+    declarative_environment;
+
+  }
+}
+
+#endif // SPOT_ELTLENV_DECLENV_HH
--- a/src/eltlenv/defaultenv.hh
+++ b/src/eltlenv/defaultenv.hh
@ -0,0 +1,45 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_ELTLENV_DEFAULTENV_HH
+# define SPOT_ELTLENV_DEFAULTENV_HH
+
+# include "environment.hh"
+# include "internal/defaultenv.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+
+    /// \brief A laxist environment.
+    /// \ingroup eltl_environment
+    ///
+    /// This environment recognizes all atomic propositions.
+    ///
+    /// This is a singleton.  Use default_environment::instance()
+    /// to obtain the instance.
+    typedef spot::internal::default_environment<eltl_t> default_environment;
+
+  }
+}
+
+#endif // SPOT_ELTLENV_DEFAULTENV_HH
--- a/src/eltlenv/environment.hh
+++ b/src/eltlenv/environment.hh
@ -0,0 +1,39 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_ELTLENV_ENVIRONMENT_HH
+# define SPOT_ELTLENV_ENVIRONMENT_HH
+
+# include "eltlast/formula.hh"
+# include "internal/environment.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+    /// \brief An environment that describes atomic propositions.
+    /// \ingroup eltl_essential
+    typedef spot::internal::environment<eltl_t> environment;
+
+  }
+}
+
+#endif // SPOT_ELTLENV_ENVIRONMENT_HH
--- a/src/eltlparse/Makefile.am
+++ b/src/eltlparse/Makefile.am
@ -0,0 +1,62 @@
+## Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+AM_CPPFLAGS = -I$(srcdir)/..
+AM_CXXFLAGS = #$(WARNING_CXXFLAGS)
+
+eltlparsedir = $(pkgincludedir)/eltlparse
+
+noinst_LTLIBRARIES = libeltlparse.la
+
+ELTLPARSE_YY = eltlparse.yy
+FROM_ELTLPARSE_YY_MAIN = eltlparse.cc
+FROM_ELTLPARSE_YY_OTHERS = \
+  stack.hh \
+  position.hh \
+  location.hh \
+  eltlparse.hh
+FROM_ELTLPARSE_YY = $(FROM_ELTLPARSE_YY_MAIN) $(FROM_ELTLPARSE_YY_OTHERS)
+
+BUILT_SOURCES = $(FROM_ELTLPARSE_YY)
+MAINTAINERCLEANFILES = $(FROM_ELTLPARSE_YY)
+
+$(FROM_ELTLPARSE_YY_MAIN): $(srcdir)/$(ELTLPARSE_YY)
+## We must cd into $(srcdir) first because if we tell bison to read
+## $(srcdir)/$(ELTLPARSE_YY), it will also use the value of $(srcdir)/
+## in the generated include statements.
+	cd $(srcdir) && \
+	  bison --defines --locations --skeleton=lalr1.cc --report=all \
+	  $(ELTLPARSE_YY) -o $(FROM_ELTLPARSE_YY_MAIN)
+$(FROM_ELTLPARSE_YY_OTHERS): $(ELTLPARSE_YY)
+	@test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_ELTLPARSE_YY_MAIN)
+
+EXTRA_DIST = $(ELTLPARSE_YY)
+
+libeltlparse_la_SOURCES = \
+  fmterror.cc \
+  $(FROM_ELTLPARSE_YY) \
+  eltlscan.ll \
+  parsedecl.hh
+
+eltlparse_HEADERS = \
+  public.hh \
+  location.hh \
+  position.hh
--- a/src/eltlparse/eltlparse.yy
+++ b/src/eltlparse/eltlparse.yy
@ -0,0 +1,279 @@
+/* Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+** 02111-1307, USA.
+*/
+%{
+#include <string>
+#include <sstream>
+#include <cerrno>
+#include "public.hh"
+#include "eltlast/allnodes.hh"
+
+// Implementation detail for error handling.
+namespace spot
+{
+  namespace eltl
+  {
+    struct parse_error_list_t
+    {
+      parse_error_list list_;
+      std::string file_;
+    };
+  }
+}
+
+#define PARSE_ERROR(Loc, Msg) \
+  pe.list_.push_back \
+    (parse_error(Loc, spair(pe.file_, Msg)))
+
+%}
+
+%name-prefix="eltlyy"
+%parse-param {spot::eltl::nfamap& nmap}
+%parse-param {spot::eltl::parse_error_list_t &pe}
+%parse-param {spot::eltl::environment &parse_environment}
+%parse-param {spot::eltl::formula* &result}
+%lex-param {spot::eltl::parse_error_list_t &pe}
+%expect 0
+%debug
+%error-verbose
+%pure-parser
+%union
+{
+  int ival;
+  std::string* sval;
+  spot::eltl::nfa* nval;
+  spot::eltl::formula* fval;
+}
+
+%{
+/* ltlparse.hh and parsedecl.hh include each other recursively.
+   We mut ensure that YYSTYPE is declared (by the above %union)
+   before parsedecl.hh uses it. */
+#include "parsedecl.hh"
+using namespace spot::eltl;
+
+%}
+
+/* All tokens.  */
+
+%token <sval> ARG "argument"
+	      ATOMIC_PROP "atomic proposition"
+	      IDENT "identifier"
+	      OP_NOT "not operator"
+	      STATE "state"
+
+%token <ival> OP_OR "or operator"
+	      OP_XOR "xor operator"
+	      OP_AND "and operator"
+	      OP_IMPLIES "implication operator"
+	      OP_EQUIV "equivalent operator"
+
+%token EQ "="
+       LPAREN "("
+       RPAREN ")"
+       COMMA ","
+       END_OF_FILE "end of file"
+       CONST_TRUE "constant true"
+       CONST_FALSE "constant false"
+
+/* Priorities.  */
+
+/* Logical operators.  */
+%left OP_OR
+%left OP_XOR
+%left OP_AND
+%left OP_IMPLIES OP_EQUIV
+
+%nonassoc OP_NOT
+
+%type <nval> nfa_def;
+%type <fval> subformula;
+%type <fval> arg_list;
+
+%destructor { delete $$; } "atomic proposition"
+
+%printer { debug_stream() << *$$; } "atomic proposition"
+
+%%
+
+result: nfa_list subformula
+	{
+	  result = $2;
+	  YYACCEPT;
+	}
+;
+
+/* NFA definitions. */
+
+nfa_list: /* empty. */
+        | nfa_list nfa
+;
+
+nfa: IDENT "=" "(" nfa_def ")"
+	{
+          nmap[*$1] = nfa::ptr($4);
+        }
+;
+
+nfa_def: /* empty. */
+        {
+	  $$ = new nfa();
+        }
+        | nfa_def STATE STATE ARG
+        {
+	  errno = 0;
+	  long i = strtol($4->c_str(), 0, 10);
+	  if (i > INT_MAX || i < INT_MIN || errno == ERANGE)
+	  {
+	    std::string s = "out of range integer `";
+	    s += *$4;
+	    s += "'";
+	    PARSE_ERROR(@1, s);
+	    delete $2;
+	    delete $3;
+	    delete $4;
+	    YYERROR;
+	  }
+	  $1->add_transition(*$2, *$3, i);
+	  $$ = $1;
+        }
+        | nfa_def EQ STATE
+        {
+ 	  $1->set_final(*$3);
+        }
+;
+
+/* Formulae. */
+
+subformula: ATOMIC_PROP
+	 {
+	   $$ = parse_environment.require(*$1);
+	   if (!$$)
+	   {
+	     std::string s = "unknown atomic proposition `";
+	     s += *$1;
+	     s += "' in environment `";
+	     s += parse_environment.name();
+	     s += "'";
+	     PARSE_ERROR(@1, s);
+	     delete $1;
+	     YYERROR;
+	   }
+	   else
+	     delete $1;
+	}
+	  | ATOMIC_PROP "(" arg_list ")"
+	{
+	  nfamap::iterator i = nmap.find(*$1);
+	  if (i == nmap.end())
+	  {
+	    std::string s = "unknown automaton operator `";
+	    s += *$1;
+	    s += "'";
+	    PARSE_ERROR(@1, s);
+	    delete $1;
+	    YYERROR;
+	  }
+
+	  automatop* res = automatop::instance(i->second, $3);
+	  if (res->size() != i->second->arity())
+	  {
+	    std::ostringstream oss1;
+	    oss1 << res->size();
+	    std::ostringstream oss2;
+	    oss2 << i->second->arity();
+
+	    std::string s(*$1);
+	    s += " is used with ";
+	    s += oss1.str();
+	    s += " arguments, but has an arity of ";
+	    s += oss2.str();
+	    PARSE_ERROR(@1, s);
+	    delete $1;
+	    YYERROR;
+	  }
+	  $$ = res;
+	}
+	  | CONST_TRUE
+	{ $$ = constant::true_instance(); }
+	  | CONST_FALSE
+	{ $$ = constant::false_instance(); }
+          | "(" subformula ")"
+	{ $$ = $2; }
+          | subformula OP_AND subformula
+	{ $$ = multop::instance(multop::And, $1, $3); }
+          | subformula OP_OR subformula
+	{ $$ = multop::instance(multop::Or, $1, $3); }
+	  | subformula OP_XOR subformula
+	{ $$ = binop::instance(binop::Xor, $1, $3); }
+	  | subformula OP_IMPLIES subformula
+        { $$ = binop::instance(binop::Implies, $1, $3); }
+	  | subformula OP_EQUIV subformula
+	{ $$ = binop::instance(binop::Equiv, $1, $3); }
+;
+
+arg_list: subformula
+	{ $$ = $1; }
+	| subformula "," arg_list
+	{ $$ = automatop::instance($1, $3); }
+;
+
+%%
+
+void
+eltlyy::parser::error(const location_type& loc, const std::string& s)
+{
+  PARSE_ERROR(loc, s);
+}
+
+namespace spot
+{
+  namespace eltl
+  {
+    formula*
+    parse(const std::string& name,
+	  parse_error_list& error_list,
+	  environment& env,
+	  bool debug)
+    {
+      if (eltlyyopen(name))
+      {
+	error_list.push_back
+	  (parse_error(eltlyy::location(),
+		       spair("-", std::string("Cannot open file ") + name)));
+	return 0;
+      }
+      formula* result = 0;
+      nfamap nmap;
+      parse_error_list_t pe;
+      pe.file_ = name;
+      eltlyy::parser parser(nmap, pe, env, result);
+      parser.set_debug_level(debug);
+      parser.parse();
+      error_list = pe.list_;
+      return result;
+    }
+  }
+}
+
+// Local Variables:
+// mode: c++
+// End:
--- a/src/eltlparse/eltlscan.ll
+++ b/src/eltlparse/eltlscan.ll
@ -0,0 +1,183 @@
+/* Copyright (C) 2008  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+** Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+** 02111-1307, USA.
+*/
+%option noyywrap
+%option prefix="eltlyy"
+%option outfile="lex.yy.c"
+
+%{
+#include <string>
+#include <stack>
+#include "eltlparse/parsedecl.hh"
+
+#define YY_USER_ACTION \
+  yylloc->columns(yyleng);
+
+// Flex uses `0' for end of file.  0 is not a token_type.
+#define yyterminate() return token::END_OF_FILE
+
+// Stack for handling include files.
+typedef std::pair<YY_BUFFER_STATE, std::string> state;
+std::stack<state> include;
+
+#define ERROR(Msg) \
+  pe.list_.push_back \
+    (spot::eltl::parse_error(*yylloc, spot::eltl::spair(pe.file_, Msg)))
+
+typedef eltlyy::parser::token token;
+
+%}
+
+eol      \n|\r|\n\r|\r\n
+%s	formula
+%x	incl
+
+%%
+
+%{
+  yylloc->step();
+%}
+
+  /* Rules for the automaton definitions part. */
+
+<INITIAL>"="		return token::EQ;
+<INITIAL>"("		return token::LPAREN;
+<INITIAL>")"		return token::RPAREN;
+<INITIAL>"%"		BEGIN(formula);
+
+<INITIAL>"include"	BEGIN(incl);
+
+<INITIAL>[a-zA-Z][a-zA-Z0-9_]* {
+			  yylval->sval = new std::string(yytext, yyleng);
+	                  return token::IDENT;
+		        }
+
+<INITIAL>[0-9]+		{
+			  yylval->sval = new std::string(yytext, yyleng);
+	                  return token::STATE;
+			}
+
+<INITIAL>$[0-9]+	{
+			  yylval->sval = new std::string(++yytext, --yyleng);
+	                  return token::ARG;
+			}
+
+<INITIAL><<EOF>>	{
+			  if (include.empty())
+			    yyterminate();
+
+			  state s = include.top();
+			  include.pop();
+			  pe.file_ = s.second;
+			  yy_delete_buffer(YY_CURRENT_BUFFER);
+			  yy_switch_to_buffer(s.first);
+			}
+
+  /* Rules for the include part. */
+
+<incl>[ \t]*
+<incl>[^ \t\n]+		{
+			  FILE* tmp = fopen(yytext, "r");
+			  if (!tmp)
+			    ERROR(std::string("cannot open file ") + yytext);
+			  else
+			  {
+			    include.push(make_pair(YY_CURRENT_BUFFER, pe.file_));
+                            pe.file_ = std::string(yytext);
+			    yy_switch_to_buffer(yy_create_buffer(tmp, YY_BUF_SIZE));
+                          }
+			  BEGIN(INITIAL);
+			}
+
+  /* Rules for the formula part. */
+
+<formula>"("		return token::LPAREN;
+<formula>")"		return token::RPAREN;
+<formula>"!"		return token::OP_NOT;
+<formula>","		return token::COMMA;
+
+
+<formula>"1"|[tT][rR][uU][eE] {
+			  return token::CONST_TRUE;
+			}
+<formula>"0"|[fF][aA][lL][sS][eE] {
+			  return token::CONST_FALSE;
+			}
+
+  /* & and | come from Spin.  && and || from LTL2BA.
+     /\, \/, and xor are from LBTT.
+  */
+<formula>"||"|"|"|"+"|"\\/" {
+			  return token::OP_OR;
+			}
+<formula>"&&"|"&"|"."|"*"|"/\\"	{
+			  return token::OP_AND;
+			}
+<formula>"^"|"xor"	return token::OP_XOR;
+<formula>"=>"|"->"	return token::OP_IMPLIES;
+<formula>"<=>"|"<->"	return token::OP_EQUIV;
+
+<formula>[a-zA-Z][a-zA-Z0-9_]* {
+			  yylval->sval = new std::string(yytext, yyleng);
+			  return token::ATOMIC_PROP;
+			}
+
+  /* Global rules. */
+
+			/* discard whitespace */
+{eol}			yylloc->lines(yyleng); yylloc->step();
+[ \t]+			yylloc->step();
+
+.			return *yytext;
+
+
+%{
+  /* Dummy use of yyunput to shut up a gcc warning.  */
+  (void) &yyunput;
+%}
+
+%%
+
+namespace spot
+{
+  namespace eltl
+  {
+    int
+    eltlyyopen(const std::string &name)
+    {
+      if (name == "-")
+	yyin = stdin;
+      else
+      {
+	yyin = fopen(name.c_str(), "r");
+	if (!yyin)
+	  return 1;
+      }
+      return 0;
+    }
+
+    void
+    eltlyyclose()
+    {
+      fclose(yyin);
+    }
+  }
+}
--- a/src/eltlparse/fmterror.cc
+++ b/src/eltlparse/fmterror.cc
@ -0,0 +1,48 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <ostream>
+#include "public.hh"
+
+namespace spot
+{
+  namespace eltl
+  {
+    bool
+    format_parse_errors(std::ostream& os,
+			parse_error_list& error_list)
+    {
+      bool printed = false;
+      spot::eltl::parse_error_list::iterator it;
+      for (it = error_list.begin(); it != error_list.end(); ++it)
+      {
+        if (it->second.first != "-")
+        {
+          os << it->second.first << ": ";
+	  os << it->first << ": ";
+        }
+	os << it->second.second << std::endl;
+	printed = true;
+      }
+      return printed;
+    }
+  }
+}
--- a/src/eltlparse/parsedecl.hh
+++ b/src/eltlparse/parsedecl.hh
@ -0,0 +1,43 @@
+// Copyright (C) 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_ELTLPARSE_PARSEDECL_HH
+# define SPOT_ELTLPARSE_PARSEDECL_HH
+
+#include "eltlparse.hh"
+#include "location.hh"
+
+# define YY_DECL \
+  int eltlyylex (eltlyy::parser::semantic_type *yylval, \
+		 eltlyy::location *yylloc, \
+		 spot::eltl::parse_error_list_t &pe)
+YY_DECL;
+
+namespace spot
+{
+  namespace eltl
+  {
+    int eltlyyopen(const std::string& name);
+    void eltlyyclose();
+  }
+}
+
+#endif // SPOT_ELTLPARSE_PARSEDECL_HH
--- a/src/eltlparse/public.hh
+++ b/src/eltlparse/public.hh
@ -0,0 +1,84 @@
+// Copyright (C) 2003, 2004, 2005, 2006, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_ELTLPARSE_PUBLIC_HH
+# define SPOT_ELTLPARSE_PUBLIC_HH
+
+# include "eltlast/formula.hh"
+# include "eltlast/visitor.hh"
+// Unfortunately Bison 2.3 uses the same guards in all parsers :(
+# undef BISON_LOCATION_HH
+# undef BISON_POSITION_HH
+# include "eltlparse/location.hh"
+# include "eltlenv/defaultenv.hh"
+# include "eltlast/nfa.hh"
+# include <string>
+# include <list>
+# include <map>
+# include <utility>
+# include <iosfwd>
+
+namespace spot
+{
+  namespace eltl
+  {
+    /// \addtogroup eltl_io
+    /// @{
+
+    typedef std::pair<std::string, std::string> spair;
+    /// \brief A parse diagnostic <location, <file, message>>.
+    typedef std::pair<eltlyy::location, spair> parse_error;
+    /// \brief A list of parser diagnostics, as filled by parse.
+    typedef std::list<parse_error> parse_error_list;
+
+    ///
+    typedef std::map<std::string, nfa::ptr> nfamap;
+
+    /// \brief Build a formula from a text file.
+    /// \param name The name of the file to parse.
+    /// \param error_list A list that will be filled with
+    ///        parse errors that occured during parsing.
+    /// \param env The environment into which parsing should take place.
+    /// \param debug When true, causes the parser to trace its execution.
+    /// \return A pointer to the tgba built from \a filename, or
+    ///        0 if the file could not be opened.
+    ///
+    /// \warning This function is not reentrant.
+    formula* parse(const std::string& name,
+		   parse_error_list& error_list,
+		   environment& env = default_environment::instance(),
+		   bool debug = false);
+
+    /// \brief Format diagnostics produced by spot::eltl::parse.
+    /// \param os Where diagnostics should be output.
+    /// \param eltl_string The string that were parsed.
+    /// \param error_list The error list filled by spot::eltl::parse while
+    ///        parsing \a eltl_string.
+    /// \return \c true iff any diagnostic was output.
+    bool
+    format_parse_errors(std::ostream& os,
+			parse_error_list& error_list);
+
+    /// @}
+  }
+}
+
+#endif // SPOT_ELTLPARSE_PUBLIC_HH
--- a/src/eltltest/Makefile.am
+++ b/src/eltltest/Makefile.am
@ -0,0 +1,44 @@
+## Copyright (C) 2003, 2004, 2005, 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+LDADD = ../libspot.la
+
+check_SCRIPTS = defs
+# Keep this sorted alphabetically.
+check_PROGRAMS = \
+  acc \
+  nfa
+
+acc_SOURCES = acc.cc
+nfa_SOURCES = nfa.cc
+
+EXTRA_DIST = $(TESTS)
+
+# Ordered by strength of the test.  Test basic features first.
+TESTS = \
+  acc.test \
+  nfa.test
+
+CLEANFILES = \
+  input \
+  prelude
--- a/src/eltltest/acc.cc
+++ b/src/eltltest/acc.cc
@ -0,0 +1,42 @@
+// Copyright (C) 2008  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <iostream>
+#include <cassert>
+#include "eltlparse/public.hh"
+
+int
+main(int argc, char** argv)
+{
+  spot::eltl::parse_error_list p;
+  const spot::eltl::formula* f = spot::eltl::parse(
+    argv[1], p, spot::eltl::default_environment::instance(), argc > 2);
+
+  if (spot::eltl::format_parse_errors(std::cerr, p))
+  {
+    if (f != 0)
+      std::cout << f->dump() << std::endl;
+    return 1;
+  }
+
+  assert(f != 0);
+  std::cout << f->dump() << std::endl;
+}
--- a/src/eltltest/acc.test
+++ b/src/eltltest/acc.test
@ -0,0 +1,31 @@
+#!/bin/sh
+
+. ./defs || exit 1
+
+set -e
+cat >prelude <<EOF
+S=(
+    0 1 \$0
+    = 1
+  )
+EOF
+
+cat >input <<EOF
+include prelude
+A=(
+    0 1 \$2
+    1 2 \$0
+    = 0
+  )
+%
+A(1,a,a|b)&S(1)
+EOF
+run 0 ./acc input || exit 1
+
+cat >input <<EOF
+A=(
+  )
+%
+1
+EOF
+run 0 ./acc input || exit 1
--- a/src/eltltest/defs.in
+++ b/src/eltltest/defs.in
@ -0,0 +1,75 @@
+# -*- shell-script -*-
+# 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+# 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', be verbose.
+if test -z "$srcdir"; then
+   test -z "$VERBOSE" && VERBOSE=x
+   # 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
+}
+
+# User can set VERBOSE to see all output.
+test -z "$VERBOSE" && exec >/dev/null 2>&1
+
+echo "== Running test $0"
+
+DOT='@DOT@'
+VALGRIND='@VALGRIND@'
+
+run()
+{
+  expected_exitcode=$1
+  shift
+  exitcode=0
+  if test -n "$VALGRIND"; then
+    exec 6>valgrind.err
+    GLIBCPP_FORCE_NEW=1 \
+    $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
+}
+
+# Turn on shell traces when VERBOSE=x.
+if test "x$VERBOSE" = xx; then
+  set -x
+else
+  :
+fi
--- a/src/eltltest/nfa.cc
+++ b/src/eltltest/nfa.cc
@ -0,0 +1,57 @@
+// Copyright (C) 2008  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <string>
+#include <set>
+#include <iostream>
+#include "eltlast/nfa.hh"
+
+using namespace spot::eltl;
+
+typedef std::set<const nfa::state*> mset;
+
+void
+dfs(nfa& a, const nfa::state* s, mset& m)
+{
+  if (m.find(s) != m.end())
+    return;
+  m.insert(s);
+
+  for (nfa::iterator i = a.begin(s); i != a.end(s); ++i)
+  {
+    std::cout << a.format_state((*i)->dest) << std::endl;
+    dfs(a, (*i)->dest, m);
+  }
+}
+
+int
+main()
+{
+  nfa a;
+
+  a.add_transition("0", "1", 1);
+  a.add_transition("1", "2", 2);
+
+  std::cout << "init: " << a.format_state(a.get_init_state()) << std::endl;
+
+  mset m;
+  dfs(a, a.get_init_state(), m);
+}
--- a/src/eltltest/nfa.test
+++ b/src/eltltest/nfa.test
@ -0,0 +1,6 @@
+#!/bin/sh
+
+. ./defs || exit 1
+
+set -e
+run 0 ./nfa || exit 1
--- a/src/internal/Makefile.am
+++ b/src/internal/Makefile.am
@ -0,0 +1,44 @@
+## Copyright (C) 2003  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+internaldir = $(pkgincludedir)/libinternal
+
+internal_HEADERS = \
+  refformula.hh \
+  refformula.hxx \
+  formula.hh \
+  formula.hxx \
+  atomic_prop.hh \
+  atomic_prop.hxx \
+  binop.hh \
+  binop.hxx \
+  constant.hh \
+  constant.hxx \
+  multop.hh \
+  multop.hxx \
+  predecl.hh \
+  unop.hh \
+  unop.hxx \
+  defaultenv.hh \
+  defaultenv.hxx \
+  declenv.hh \
+  declenv.hxx \
+  environment.hh
--- a/src/internal/atomic_prop.hh
+++ b/src/internal/atomic_prop.hh
@ -0,0 +1,85 @@
+// Copyright (C) 2003, 2004, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/atomic_prop.hh
+/// \brief Generic atomic propositions
+#ifndef SPOT_INTERNAL_ATOMIC_PROP_HH
+# define SPOT_INTERNAL_ATOMIC_PROP_HH
+
+#include <string>
+#include <iosfwd>
+#include <map>
+#include <cassert>
+#include <ostream>
+#include "refformula.hh"
+#include "environment.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief Atomic propositions.
+    /// \ingroup generic_ast
+    template<typename T>
+    class atomic_prop : public ref_formula<T>
+    {
+    public:
+      /// Build an atomic proposition with name \a name in
+      /// environment \a env.
+      static atomic_prop<T>* instance(const std::string& name,
+				      environment<T>& env);
+
+      typedef typename T::visitor visitor;
+      typedef typename T::const_visitor const_visitor;
+
+      virtual void accept(visitor& visitor);
+      virtual void accept(const_visitor& visitor) const;
+
+      /// Get the name of the atomic proposition.
+      const std::string& name() const;
+      /// Get the environment of the atomic proposition.
+      environment<T>& env() const;
+
+      /// Number of instantiated atomic propositions.  For debugging.
+      static unsigned instance_count();
+      /// List all instances of atomic propositions.  For debugging.
+      static std::ostream& dump_instances(std::ostream& os);
+
+    protected:
+      atomic_prop(const std::string& name, environment<T>& env);
+      virtual ~atomic_prop();
+
+      typedef std::pair<std::string, environment<T>*> pair;
+      typedef std::map<pair, atomic_prop<T>*> map;
+      static map instances;
+
+    private:
+      std::string name_;
+      environment<T>* env_;
+    };
+
+  }
+}
+
+# include "atomic_prop.hxx"
+
+#endif // SPOT_INTERNAL_ATOMICPROP_HH
--- a/src/internal/atomic_prop.hxx
+++ b/src/internal/atomic_prop.hxx
@ -0,0 +1,123 @@
+// Copyright (C) 2003, 2004, 2005, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/atomic_prop.hxx
+/// \brief Generic atomic propositions implementation
+#ifndef SPOT_INTERNAL_ATOMIC_PROP_HXX
+# define SPOT_INTERNAL_ATOMIC_PROP_HXX
+
+#include "atomic_prop.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    template<typename T>
+    atomic_prop<T>::atomic_prop(const std::string& name, environment<T>& env)
+      : name_(name), env_(&env)
+    {
+      this->dump_ = "AP(" + name + ")";
+      this->set_key_();
+    }
+
+    template<typename T>
+    atomic_prop<T>::~atomic_prop()
+    {
+      // Get this instance out of the instance map.
+      pair p(name(), &env());
+      typename map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
+    }
+
+    template<typename T>
+    void
+    atomic_prop<T>::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    void
+    atomic_prop<T>::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    const std::string&
+    atomic_prop<T>::name() const
+    {
+      return name_;
+    }
+
+    template<typename T>
+    environment<T>&
+    atomic_prop<T>::env() const
+    {
+      return *env_;
+    }
+
+    template<typename T>
+    typename atomic_prop<T>::map atomic_prop<T>::instances;
+
+    template<typename T>
+    atomic_prop<T>*
+    atomic_prop<T>::instance(const std::string& name, environment<T>& env)
+    {
+      pair p(name, &env);
+      typename map::iterator i = instances.find(p);
+      if (i != instances.end())
+	{
+	  return static_cast<atomic_prop<T>*>(i->second->ref());
+	}
+      atomic_prop<T>* ap = new atomic_prop<T>(name, env);
+      instances[p] = ap;
+      return static_cast<atomic_prop<T>*>(ap->ref());
+    }
+
+    template<typename T>
+    unsigned
+    atomic_prop<T>::instance_count()
+    {
+      return instances.size();
+    }
+
+    template<typename T>
+    std::ostream&
+    atomic_prop<T>::dump_instances(std::ostream& os)
+    {
+
+      for (typename map::iterator i = instances.begin();
+	   i != instances.end(); ++i)
+      {
+	  os << i->second << " = " << i->second->ref_count_()
+	     << " * atomic_prop(" << i->first.first << ", "
+	     << i->first.second->name() << ")" << std::endl;
+	}
+      return os;
+    }
+
+  }
+}
+
+#endif // SPOT_INTERNAL_ATOMICPROP_HXX
--- a/src/internal/binop.hh
+++ b/src/internal/binop.hh
@ -0,0 +1,99 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/binop.hh
+/// \brief Generic binary operators
+///
+/// This does not include \c AND and \c OR operators.  These are
+/// considered to be multi-operand operators (see spot::internal::multop).
+#ifndef SPOT_INTERNAL_BINOP_HH
+# define SPOT_INTERNAL_BINOP_HH
+
+#include <map>
+#include "refformula.hh"
+#include <cassert>
+#include <utility>
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief Generic binary operator.
+    /// \ingroup generic_ast
+    template<typename T>
+    class binop : public ref_formula<T>
+    {
+    public:
+      /// Different kinds of binary opertaors
+      ///
+      /// And and Or are not here.  Because they
+      /// are often nested we represent them as multops.
+      typedef typename T::binop type;
+
+      /// Build an unary operator with operation \a op and
+      /// children \a first and \a second.
+      static binop<T>* instance(type op, formula<T>* first, formula<T>* second);
+
+      typedef typename T::visitor visitor;
+      typedef typename T::const_visitor const_visitor;
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      /// Get the first operand.
+      const formula<T>* first() const;
+      /// Get the first operand.
+      formula<T>* first();
+      /// Get the second operand.
+      const formula<T>* second() const;
+      /// Get the second operand.
+      formula<T>* second();
+
+      /// Get the type of this operator.
+      type op() const;
+      /// Get the type of this operator, as a string.
+      const char* op_name() const;
+
+      /// Number of instantiated binary operators.  For debugging.
+      static unsigned instance_count();
+
+    protected:
+      typedef std::pair<formula<T>*, formula<T>*> pairf;
+      typedef std::pair<type, pairf> pair;
+      typedef std::map<pair, formula<T>*> map;
+      static map instances;
+
+      binop(type op, formula<T>* first, formula<T>* second);
+      virtual ~binop();
+
+    private:
+      type op_;
+      formula<T>* first_;
+      formula<T>* second_;
+    };
+
+  }
+}
+
+# include "binop.hxx"
+
+#endif // SPOT_INTERNAL_BINOP_HH
--- a/src/internal/binop.hxx
+++ b/src/internal/binop.hxx
@ -0,0 +1,156 @@
+// Copyright (C) 2003, 2005  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/binop.hxx
+/// \brief Generic binary operators implementation
+#ifndef SPOT_INTERNAL_BINOP_HXX
+# define SPOT_INTERNAL_BINOP_HXX
+
+#include "binop.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    binop<T>::binop(type op, formula<T>* first, formula<T>* second)
+      : op_(op), first_(first), second_(second)
+    {
+      this->dump_ = "binop(";
+      this->dump_ += op_name();
+      this->dump_ += ", " + first->dump() + ", " + second->dump() + ")";
+      this->set_key_();
+    }
+
+    template<typename T>
+    binop<T>::~binop()
+    {
+      // Get this instance out of the instance map.
+      pairf pf(first(), second());
+      pair p(op(), pf);
+      typename map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
+    }
+
+    template<typename T>
+    void
+    binop<T>::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    void
+    binop<T>::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    const formula<T>*
+    binop<T>::first() const
+    {
+      return first_;
+    }
+
+    template<typename T>
+    formula<T>*
+    binop<T>::first()
+    {
+      return first_;
+    }
+
+    template<typename T>
+    const formula<T>*
+    binop<T>::second() const
+    {
+      return second_;
+    }
+
+    template<typename T>
+    formula<T>*
+    binop<T>::second()
+    {
+      return second_;
+    }
+
+    template<typename T>
+    typename binop<T>::type
+    binop<T>::op() const
+    {
+      return op_;
+    }
+
+    template<typename T>
+    const char*
+    binop<T>::op_name() const
+    {
+      return T::binop_name(op_);
+    }
+
+    template<typename T>
+    typename binop<T>::map binop<T>::instances;
+
+    template<typename T>
+    binop<T>*
+    binop<T>::instance(type op, formula<T>* first, formula<T>* second)
+    {
+      // Sort the operands of associative operators, so that for
+      // example the formula instance for 'a xor b' is the same as
+      // that for 'b xor a'.
+      switch (op)
+      {
+	case T::Xor:
+	case T::Equiv:
+	  if (second < first)
+	    std::swap(first, second);
+	  break;
+	case T::Implies:
+	  // case U:
+	  // case R:
+	  //   // Non associative operators.
+	default:
+	  break;
+      }
+
+      pairf pf(first, second);
+      pair p(op, pf);
+      typename map::iterator i = instances.find(p);
+      if (i != instances.end())
+	{
+	  return static_cast<binop<T>*>(i->second->ref());
+	}
+      binop<T>* ap = new binop<T>(op, first, second);
+      instances[p] = ap;
+      return static_cast<binop<T>*>(ap->ref());
+    }
+
+    template<typename T>
+    unsigned
+    binop<T>::instance_count()
+    {
+      return instances.size();
+    }
+  }
+}
+
+#endif // SPOT_INTERNAL_BINOP_HXX
--- a/src/internal/constant.hh
+++ b/src/internal/constant.hh
@ -0,0 +1,72 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/constant.hh
+/// \brief Generic constants
+#ifndef SPOT_INTERNAL_CONSTANT_HH
+# define SPOT_INTERNAL_CONSTANT_HH
+
+#include <cassert>
+#include "formula.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief A constant (True or False)
+    /// \ingroup generic_ast
+    template<typename T>
+    class constant : public formula<T>
+    {
+    public:
+      enum type { False, True };
+
+      typedef typename T::visitor visitor;
+      typedef typename T::const_visitor const_visitor;
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      /// Return the value of the constant.
+      type val() const;
+      /// Return the value of the constant as a string.
+      const char* val_name() const;
+
+      /// Get the sole instance of spot::internal::constant<T>::constant(1).
+      static constant* true_instance();
+      /// Get the sole instance of spot::internal::constant<T>::constant(0).
+      static constant* false_instance();
+
+    protected:
+      constant(type val);
+      virtual ~constant();
+
+    private:
+      type val_;
+    };
+
+  }
+}
+
+# include "constant.hxx"
+
+#endif // SPOT_INTERNAL_CONSTANT_HH
--- a/src/internal/constant.hxx
+++ b/src/internal/constant.hxx
@ -0,0 +1,112 @@
+// Copyright (C) 2003, 2005, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/constant.hxx
+/// \brief Generic constants implementation
+#ifndef SPOT_INTERNAL_CONSTANT_HXX
+# define SPOT_INTERNAL_CONSTANT_HXX
+
+#include "constant.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    constant<T>::constant(type val)
+      : val_(val)
+    {
+      switch (val)
+	{
+	case True:
+	  this->dump_ = "constant(1)";
+	  this->set_key_();
+	  return;
+	case False:
+	  this->dump_ = "constant(0)";
+	  this->set_key_();
+	  return;
+	}
+      // Unreachable code.
+      assert(0);
+    }
+
+    template<typename T>
+    constant<T>::~constant()
+    {
+    }
+
+    template<typename T>
+    void
+    constant<T>::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    void
+    constant<T>::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    typename constant<T>::type
+    constant<T>::val() const
+    {
+      return val_;
+    }
+
+    template<typename T>
+    const char*
+    constant<T>::val_name() const
+    {
+      switch (val_)
+	{
+	case True:
+	  return "1";
+	case False:
+	  return "0";
+	}
+      // Unreachable code.
+      assert(0);
+      return 0;
+    }
+
+    template<typename T>
+    constant<T>*
+    constant<T>::false_instance()
+    {
+      static constant<T> f(constant<T>::False);
+      return &f;
+    }
+
+    template<typename T>
+    constant<T>*
+    constant<T>::true_instance()
+    {
+      static constant<T> t(constant<T>::True);
+      return &t;
+    }
+  }
+}
+
+#endif // SPOT_INTERNAL_CONSTANT_HXX
--- a/src/internal/declenv.hh
+++ b/src/internal/declenv.hh
@ -0,0 +1,69 @@
+// Copyright (C) 2004  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_INTERNAL_DECLENV_HH
+# define SPOT_INTERNAL_DECLENV_HH
+
+#include <string>
+#include <map>
+#include "atomic_prop.hh"
+#include "environment.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief A declarative environment.
+    /// \ingroup generic_environment
+    ///
+    /// This environment recognizes all atomic propositions
+    /// that have been previously declared.  It will reject other.
+    template<typename T>
+    class declarative_environment : public environment<T>
+    {
+    public:
+      declarative_environment();
+      ~declarative_environment();
+
+      /// Declare an atomic proposition.  Return false iff the
+      /// proposition was already declared.
+      bool declare(const std::string& prop_str);
+
+      virtual formula<T>* require(const std::string& prop_str);
+
+      /// Get the name of the environment.
+      virtual const std::string& name();
+
+      typedef std::map<const std::string, atomic_prop<T>*> prop_map;
+
+      /// Get the map of atomic proposition known to this environment.
+      const prop_map& get_prop_map() const;
+
+    private:
+      prop_map props_;
+    };
+  }
+}
+
+#include "declenv.hxx"
+
+#endif // SPOT_INTERNAL_DECLENV_HH
--- a/src/internal/declenv.hxx
+++ b/src/internal/declenv.hxx
@ -0,0 +1,83 @@
+// Copyright (C) 2004, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_INTERNAL_DECLENV_HXX
+# define SPOT_INTERNAL_DECLENV_HXX
+
+#include "declenv.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    template<typename T>
+    declarative_environment<T>::declarative_environment()
+    {
+    }
+
+    template<typename T>
+    declarative_environment<T>::~declarative_environment()
+    {
+      // FIXME !!
+      // for (prop_map::iterator i = props_.begin(); i != props_.end(); ++i)
+      // 	ltl::destroy(i->second);
+    }
+
+    template<typename T>
+    bool
+    declarative_environment<T>::declare(const std::string& prop_str)
+    {
+      if (props_.find(prop_str) != props_.end())
+	return false;
+      props_[prop_str] = internal::atomic_prop<T>::instance(prop_str, *this);
+      return true;
+    }
+
+    template<typename T>
+    formula<T>*
+    declarative_environment<T>::require(const std::string& prop_str)
+    {
+      typename prop_map::iterator i = props_.find(prop_str);
+      if (i == props_.end())
+	return 0;
+      // It's an atomic_prop, so we do not have to use the clone() visitor.
+      return i->second->ref();
+    }
+
+    template<typename T>
+    const std::string&
+    declarative_environment<T>::name()
+    {
+      static std::string name("declarative environment");
+      return name;
+    }
+
+    template<typename T>
+    const typename declarative_environment<T>::prop_map&
+    declarative_environment<T>::get_prop_map() const
+    {
+      return props_;
+    }
+  }
+}
+
+#endif // SPOT_INTERNAL_DECLENV_HXX
--- a/src/internal/defaultenv.hh
+++ b/src/internal/defaultenv.hh
@ -0,0 +1,59 @@
+// Copyright (C) 2003, 2004, 2005  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_INTERNAL_DEFAULTENV_HH
+# define SPOT_INTERNAL_DEFAULTENV_HH
+
+#include "atomic_prop.hh"
+#include "environment.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief A laxist environment.
+    /// \ingroup generic_environment
+    ///
+    /// This environment recognizes all atomic propositions.
+    ///
+    /// This is a singleton.  Use default_environment<T>::instance()
+    /// to obtain the instance.
+    template<typename T>
+    class default_environment : public environment<T>
+    {
+    public:
+      virtual ~default_environment();
+      virtual formula<T>* require(const std::string& prop_str);
+      virtual const std::string& name();
+
+      /// Get the sole instance of spot::internal::default_environment<T>.
+      static default_environment<T>& instance();
+    protected:
+      default_environment();
+    };
+
+  }
+}
+
+#include "defaultenv.hxx"
+
+#endif // SPOT_INTERNAL_DEFAULTENV_HH
--- a/src/internal/defaultenv.hxx
+++ b/src/internal/defaultenv.hxx
@ -0,0 +1,68 @@
+// Copyright (C) 2003  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_INTERNAL_DEFAULTENV_HXX
+# define SPOT_INTERNAL_DEFAULTENV_HXX
+
+#include "defaultenv.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    template<typename T>
+    default_environment<T>::~default_environment()
+    {
+    }
+
+    template<typename T>
+    formula<T>*
+    default_environment<T>::require(const std::string& s)
+    {
+      return atomic_prop<T>::instance(s, *this);
+    }
+
+    template<typename T>
+    const std::string&
+    default_environment<T>::name()
+    {
+      static std::string name("default environment");
+      return name;
+    }
+
+    template<typename T>
+    default_environment<T>::default_environment()
+    {
+    }
+
+    template<typename T>
+    default_environment<T>&
+    default_environment<T>::instance()
+    {
+      static default_environment<T>* singleton = new default_environment<T>();
+      return *singleton;
+    }
+
+  }
+}
+
+#endif // SPOT_INTERNAL_DEFAULTENV_HXX
--- a/src/internal/environment.hh
+++ b/src/internal/environment.hh
@ -0,0 +1,72 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_INTERNAL_ENVIRONMENT_HH
+# define SPOT_INTERNAL_ENVIRONMENT_HH
+
+# include "formula.hh"
+# include <string>
+
+namespace spot
+{
+  namespace internal
+  {
+    /// \brief An environment that describes atomic propositions.
+    /// \ingroup generic_essential
+    template<typename T>
+    class environment
+    {
+    public:
+      /// \brief Obtain the formula associated to \a prop_str
+      ///
+      /// Usually \a prop_str, is the name of an atomic proposition,
+      /// and spot::internal::require simply returns the associated
+      /// spot::internal::atomic_prop<T>.
+      ///
+      /// Note this is not a \c const method.  Some environments will
+      /// "create" the atomic proposition when requested.
+      ///
+      /// We return a spot::internal::formula<T> instead of an
+      /// spot::internal::atomic_prop<T>, because this
+      /// will allow nifty tricks (e.g., we could name formulae in an
+      /// environment, and let the parser build a larger tree from
+      /// these).
+      ///
+      /// \return 0 iff \a prop_str is not part of the environment,
+      ///   or the associated spot::internal::formula<T> otherwise.
+      virtual formula<T>* require(const std::string& prop_str) = 0;
+
+      /// Get the name of the environment.
+      virtual const std::string& name() = 0;
+
+      virtual
+      ~environment()
+      {
+      }
+
+      // FIXME: More functions will be needed later, but
+      // it's enough for now.
+    };
+
+  }
+}
+
+#endif // SPOT_INTERNAL_ENVIRONMENT_HH
--- a/src/internal/formula.hh
+++ b/src/internal/formula.hh
@ -0,0 +1,162 @@
+// Copyright (C) 2003, 2004, 2005  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/formula.hh
+/// \brief Generic formula interface
+#ifndef SPOT_INTERNAL_FORMULA_HH
+# define SPOT_INTERNAL_FORMULA_HH
+
+# include <string>
+# include <cassert>
+# include "predecl.hh"
+# include "misc/hash.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    /// \brief A Generic formula.
+    /// \ingroup generic_essential
+    /// \ingroup generic_ast
+    ///
+    /// The only way you can work with a formula is to
+    /// build a T::visitor or T::const_visitor.
+    template<typename T>
+    class formula : public T
+    {
+    public:
+      typedef typename T::visitor visitor;
+      typedef typename T::const_visitor const_visitor;
+
+      /// Entry point for T::visitor instances.
+      virtual void accept(visitor& v) = 0;
+      /// Entry point for T::const_visitor instances.
+      virtual void accept(const_visitor& v) const = 0;
+
+      /// \brief clone this node
+      ///
+      /// This increments the reference counter of this node (if one is
+      /// used).  You should almost never use this method directly as
+      /// it doesn't touch the children.  If you want to clone a
+      /// whole formula, use a clone visitor instead.
+      formula<T>* ref();
+      /// \brief release this node
+      ///
+      /// This decrements the reference counter of this node (if one is
+      /// used) and can free the object.  You should almost never use
+      /// this method directly as it doesn't touch the children.  If you
+      /// want to release a whole formula, use a destroy() visitor instead.
+      static void unref(formula<T>* f);
+
+      /// Return a canonic representation of the formula
+      const std::string& dump() const;
+
+      /// Return a hash_key for the formula.
+      const size_t
+      hash() const
+      {
+	return hash_key_;
+      }
+    protected:
+      virtual ~formula();
+
+      /// \brief increment reference counter if any
+      virtual void ref_();
+      /// \brief decrement reference counter if any, return true when
+      /// the instance must be deleted (usually when the counter hits 0).
+      virtual bool unref_();
+
+      /// \brief Compute key_ from dump_.
+      ///
+      /// Should be called once in each object, after dump_ has been set.
+      void set_key_();
+      /// The canonic representation of the formula
+      std::string dump_;
+      /// \brief The hash key of this formula.
+      ///
+      /// Initialized by set_key_().
+      size_t hash_key_;
+    };
+
+    /// \brief Strict Weak Ordering for <code>const formula*</code>.
+    /// \ingroup generic_essentials
+    ///
+    /// This is meant to be used as a comparison functor for
+    /// STL \c map whose key are of type <code>const formula<T>*</code>.
+    ///
+    /// For instance here is how one could declare
+    /// a map of \c const::formula*.
+    /// \code
+    ///   // Remember how many times each formula has been seen.
+    ///   template<typename T>
+    ///   std::map<const spot::internal::formula<T>*, int,
+    ///            spot::internal::formula_ptr_less_than<T> > seen;
+    /// \endcode
+    template<typename T>
+    struct formula_ptr_less_than:
+      public std::binary_function<const formula<T>*, const formula<T>*, bool>
+    {
+      bool
+      operator()(const formula<T>* left, const formula<T>* right) const
+      {
+    	assert(left);
+    	assert(right);
+    	size_t l = left->hash();
+    	size_t r = right->hash();
+    	if (1 != r)
+    	  return l < r;
+    	return left->dump() < right->dump();
+      }
+    };
+
+    /// \brief Hash Function for <code>const formula*</code>.
+    /// \ingroup generic_essentials
+    /// \ingroup hash_funcs
+    ///
+    /// This is meant to be used as a hash functor for
+    /// Sgi's \c hash_map whose key are of type <code>const formula*</code>.
+    ///
+    /// For instance here is how one could declare
+    /// a map of \c const::formula*.
+    /// \code
+    ///   // Remember how many times each formula has been seen.
+    ///   template<typename T>
+    ///   Sgi::hash_map<const spot::internal::formula<T>*, int,
+    ///                 const spot::internal::formula_ptr_hash<T> > seen;
+    /// \endcode
+    template<typename T>
+    struct formula_ptr_hash:
+      public std::unary_function<const formula<T>*, size_t>
+    {
+      size_t
+      operator()(const formula<T>* that) const
+      {
+    	assert(that);
+    	return that->hash();
+      }
+    };
+
+  }
+}
+
+# include "formula.hxx"
+
+#endif // SPOT_INTERNAL_FORMULA_HH
--- a/src/internal/formula.hxx
+++ b/src/internal/formula.hxx
@ -0,0 +1,86 @@
+// Copyright (C) 2003, 2005, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/formula.hxx
+/// \brief Generic formula implementation
+#ifndef SPOT_INTERNAL_FORMULA_HXX
+# define SPOT_INTERNAL_FORMULA_HXX
+
+#include "formula.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    formula<T>*
+    formula<T>::ref()
+    {
+      ref_();
+      return this;
+    }
+
+    template<typename T>
+    formula<T>::~formula()
+    {
+    }
+
+    template<typename T>
+    void
+    formula<T>::unref(formula<T>* f)
+    {
+      if (f->unref_())
+	delete f;
+    }
+
+    template<typename T>
+    void
+    formula<T>::ref_()
+    {
+      // Not reference counted by default.
+    }
+
+    template<typename T>
+    bool
+    formula<T>::unref_()
+    {
+      // Not reference counted by default.
+      return false;
+    }
+
+    template<typename T>
+    const std::string&
+    formula<T>::dump() const
+    {
+      return dump_;
+    }
+
+    template<typename T>
+    void
+    formula<T>::set_key_()
+    {
+      string_hash sh;
+      hash_key_ = sh(dump_);
+    }
+  }
+}
+
+#endif // SPOT_INTERNAL_FORMULA_HXX
--- a/src/internal/multop.hh
+++ b/src/internal/multop.hh
@ -0,0 +1,138 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/multop.hh
+/// \brief Generic multi-operand operators
+#ifndef SPOT_INTERNAL_MULTOP_HH
+# define SPOT_INTERNAL_MULTOP_HH
+
+#include <vector>
+#include <map>
+#include <cassert>
+#include <utility>
+#include <algorithm>
+#include "refformula.hh"
+#include "constant.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief Multi-operand operators.
+    /// \ingroup generic_ast
+    ///
+    /// These operators are considered commutative and associative.
+    template<typename T>
+    class multop : public ref_formula<T>
+    {
+    public:
+      enum type { Or, And };
+
+      /// List of formulae.
+      typedef std::vector<formula<T>*> vec;
+
+      /// \brief Build a spot::internal::multop<T> with two children.
+      ///
+      /// If one of the children itself is a spot::internal::multop<T>
+      /// with the same type, it will be merged.  I.e., children
+      /// if that child will be added, and that child itself will
+      /// be destroyed.  This allows incremental building of
+      /// n-ary internal::multop<T>.
+      ///
+      /// This functions can perform slight optimizations and may not
+      /// return an internal::multop<T> objects.  For instance if \c
+      /// first and \c second are equal, that formula is returned
+      /// as-is.
+      static formula<T>* instance(type op,
+				  formula<T>* first, formula<T>* second);
+
+      /// \brief Build a spot::internal::multop<T> with many children.
+      ///
+      /// Same as the other instance() function, but take a vector of
+      /// formula in argument.  This vector is acquired by the
+      /// spot::internal::multop<T> class, the caller should allocate
+      /// it with \c new, but not use it (especially not destroy it)
+      /// after it has been passed to spot::internal::multop<T>.
+      ///
+      /// This functions can perform slight optimizations and may not
+      /// return an internal::multop<T> objects.  For instance if the
+      /// vector contain only one unique element, this this formula
+      /// will be returned as-is.
+      static formula<T>* instance(type op, vec* v);
+
+      typedef typename T::visitor visitor;
+      typedef typename T::const_visitor const_visitor;
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      /// Get the number of children.
+      unsigned size() const;
+      /// \brief Get the nth children.
+      ///
+      /// Starting with \a n = 0.
+      const formula<T>* nth(unsigned n) const;
+      /// \brief Get the nth children.
+      ///
+      /// Starting with \a n = 0.
+      formula<T>* nth(unsigned n);
+
+      /// Get the type of this operator.
+      type op() const;
+      /// Get the type of this operator, as a string.
+      const char* op_name() const;
+
+      /// Number of instantiated multi-operand operators.  For debugging.
+      static unsigned instance_count();
+
+    protected:
+      typedef std::pair<type, vec*> pair;
+      /// Comparison functor used internally by internal::multop<T>.
+      struct paircmp
+      {
+	bool
+	operator () (const pair& p1, const pair& p2) const
+	{
+	  if (p1.first != p2.first)
+	    return p1.first < p2.first;
+	  return *p1.second < *p2.second;
+	}
+      };
+      typedef std::map<pair, formula<T>*, paircmp> map;
+      static map instances;
+
+      multop(type op, vec* v);
+      virtual ~multop();
+
+    private:
+      type op_;
+      vec* children_;
+
+      static void destroy(formula<T>* c);
+    };
+
+  }
+}
+
+# include "multop.hxx"
+
+#endif // SPOT_INTERNAL_MULTOP_HH
--- a/src/internal/multop.hxx
+++ b/src/internal/multop.hxx
@ -0,0 +1,252 @@
+// Copyright (C) 2003, 2004, 2005, 2008 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/multop.hxx
+/// \brief Generic multi-operand operators implementation
+#ifndef SPOT_INTERNAL_MULTOP_HXX
+# define SPOT_INTERNAL_MULTOP_HXX
+
+#include "multop.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    multop<T>::multop(type op, vec* v)
+      : op_(op), children_(v)
+    {
+      this->dump_ = "multop(";
+      this->dump_ += op_name();
+      unsigned max = v->size();
+      for (unsigned n = 0; n < max; ++n)
+	{
+	  this->dump_ += ", " + (*v)[n]->dump();
+	}
+      this->dump_ += ")";
+      this->set_key_();
+    }
+
+    template<typename T>
+    multop<T>::~multop()
+    {
+      // Get this instance out of the instance map.
+      pair p(op(), children_);
+      typename map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
+
+      delete children_;
+    }
+
+    template<typename T>
+    void
+    multop<T>::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    void
+    multop<T>::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    unsigned
+    multop<T>::size() const
+    {
+      return children_->size();
+    }
+
+    template<typename T>
+    const formula<T>*
+    multop<T>::nth(unsigned n) const
+    {
+      return (*children_)[n];
+    }
+
+    template<typename T>
+    formula<T>*
+    multop<T>::nth(unsigned n)
+    {
+      return (*children_)[n];
+    }
+
+    template<typename T>
+    typename multop<T>::type
+    multop<T>::op() const
+    {
+      return op_;
+    }
+
+    template<typename T>
+    const char*
+    multop<T>::op_name() const
+    {
+      switch (op_)
+	{
+	case And:
+	  return "And";
+	case Or:
+	  return "Or";
+	}
+      // Unreachable code.
+      assert(0);
+      return 0;
+    }
+
+    template<typename T>
+    typename multop<T>::map multop<T>::instances;
+
+    template<typename T>
+    formula<T>*
+    multop<T>::instance(type op, vec* v)
+    {
+      pair p(op, v);
+
+      // Inline children of same kind.
+      {
+	vec inlined;
+	typename vec::iterator i = v->begin();
+	while (i != v->end())
+	  {
+	    multop<T>* p = dynamic_cast<multop<T>*>(*i);
+	    if (p && p->op() == op)
+	      {
+		unsigned ps = p->size();
+		for (unsigned n = 0; n < ps; ++n)
+		  inlined.push_back(p->nth(n));
+		// That sub-formula is now useless, drop it.
+		// Note that we use unref(), not destroy(), because we've
+		// adopted its children and don't want to destroy these.
+		formula<T>::unref(*i);
+		i = v->erase(i);
+	      }
+	    else
+	      {
+		++i;
+	      }
+	  }
+	v->insert(v->end(), inlined.begin(), inlined.end());
+      }
+
+      std::sort(v->begin(), v->end(), formula_ptr_less_than<T>());
+
+      // Remove duplicates.  We can't use std::unique(), because we
+      // must destroy() any formula we drop.
+      {
+	formula<T>* last = 0;
+	typename vec::iterator i = v->begin();
+	while (i != v->end())
+	  {
+	    if (*i == last)
+	      {
+		destroy(*i);
+		i = v->erase(i);
+	      }
+	    else
+	      {
+		last = *i++;
+	      }
+	  }
+	}
+
+      typename vec::size_type s = v->size();
+      if (s == 0)
+	{
+	  delete v;
+	  switch (op)
+	    {
+	    case And:
+	      return constant<T>::true_instance();
+	    case Or:
+	      return constant<T>::false_instance();
+	    }
+	  /* Unreachable code.  */
+	  assert(0);
+	}
+      else if (s == 1)
+	{
+	  formula<T>* res = (*v)[0];
+	  delete v;
+	  return res;
+	}
+
+      typename map::iterator i = instances.find(p);
+      if (i != instances.end())
+	{
+	  delete v;
+	  return static_cast<multop<T>*>(i->second->ref());
+	}
+      multop<T>* ap = new multop<T>(op, v);
+      instances[p] = ap;
+      return static_cast<multop<T>*>(ap->ref());
+
+    }
+
+    template<typename T>
+    formula<T>*
+    multop<T>::instance(type op, formula<T>* first, formula<T>* second)
+    {
+      vec* v = new vec;
+      v->push_back(first);
+      v->push_back(second);
+      return instance(op, v);
+    }
+
+    template<typename T>
+    unsigned
+    multop<T>::instance_count()
+    {
+      return instances.size();
+    }
+
+    template<typename T>
+    void
+    multop<T>::destroy(formula<T>* c)
+    {
+      if (unop<T>* uo = dynamic_cast<unop<T>*>(c))
+      {
+	destroy(uo->child());
+	formula<T>::unref(uo);
+      }
+      else if (binop<T>* bo = dynamic_cast<binop<T>*>(c))
+      {
+	destroy(bo->first());
+	destroy(bo->second());
+	formula<T>::unref(bo);
+      }
+      else if (multop<T>* mo = dynamic_cast<multop<T>*>(c))
+      {
+	unsigned s = mo->size();
+	for (unsigned i = 0; i < s; ++i)
+	  destroy(mo->nth(i));
+	formula<T>::unref(mo);
+      }
+      else // constant<T>* || atomic_prop<T>*
+	formula<T>::unref(c);
+    }
+  }
+}
+
+#endif // SPOT_INTERNAL_MULTOP_HXX
--- a/src/internal/predecl.hh
+++ b/src/internal/predecl.hh
@ -0,0 +1,49 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/predecl.hh
+/// \brief Predeclare all node types.
+///
+/// This file is usually used when \b declaring methods and functions
+/// over nodes.
+#ifndef SPOT_INTERNAL_PREDECL_HH
+# define SPOT_INTERNAL_PREDECL_HH
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    struct atomic_prop;
+    template<typename T>
+    struct unop;
+    template<typename T>
+    struct constant;
+    template<typename T>
+    struct binop;
+    template<typename T>
+    struct formula;
+    template<typename T>
+    struct multop;
+  }
+}
+
+#endif // SPOT_INTERNAL_PREDECL_HH
--- a/src/internal/refformula.hh
+++ b/src/internal/refformula.hh
@ -0,0 +1,57 @@
+// Copyright (C) 2003, 2004, 2005  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/refformula.hh
+/// \brief Reference-counted generic formulae
+#ifndef SPOT_INTERNAL_REFFORMULA_HH
+# define SPOT_INTERNAL_REFFORMULA_HH
+
+#include "formula.hh"
+#include <cassert>
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief A reference-counted generic formula.
+    /// \ingroup generic_ast
+    template<typename T>
+    class ref_formula : public formula<T>
+    {
+    protected:
+      virtual ~ref_formula();
+      ref_formula();
+      void ref_();
+      bool unref_();
+      /// Number of references to this formula.
+      unsigned ref_count_();
+
+    private:
+      unsigned ref_counter_;
+    };
+
+  }
+}
+
+# include "refformula.hxx"
+
+#endif // SPOT_INTERNAL_REFFORMULA_HH
--- a/src/internal/refformula.hxx
+++ b/src/internal/refformula.hxx
@ -0,0 +1,69 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/refformula.hxx
+/// \brief Reference-counted generic formulae implementation
+#ifndef SPOT_INTERNAL_REFFORMULA_HXX
+# define SPOT_INTERNAL_REFFORMULA_HXX
+
+#include "refformula.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    ref_formula<T>::ref_formula()
+      : ref_counter_(0)
+    {
+    }
+
+    template<typename T>
+    ref_formula<T>::~ref_formula()
+    {
+    }
+
+    template<typename T>
+    void
+    ref_formula<T>::ref_()
+    {
+      ++ref_counter_;
+    }
+
+    template<typename T>
+    bool
+    ref_formula<T>::unref_()
+    {
+      assert(ref_counter_ > 0);
+      return !--ref_counter_;
+    }
+
+    template<typename T>
+    unsigned
+    ref_formula<T>::ref_count_()
+    {
+      return ref_counter_;
+    }
+
+  }
+}
+
+#endif // SPOT_INTERNAL_REFFORMULA_HXX
--- a/src/internal/unop.hh
+++ b/src/internal/unop.hh
@ -0,0 +1,85 @@
+// 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.
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/unop.hh
+/// \brief Generic unary operators
+#ifndef SPOT_INTERNAL_UNOP_HH
+# define SPOT_INTERNAL_UNOP_HH
+
+#include <map>
+#include "refformula.hh"
+#include <cassert>
+
+namespace spot
+{
+  namespace internal
+  {
+
+    /// \brief Generic unary operators.
+    /// \ingroup generic_ast
+    template<typename T>
+    class unop : public ref_formula<T>
+    {
+    public:
+      typedef typename T::unop type;
+
+      /// Build an unary operator with operation \a op and
+      /// child \a child.
+      static unop* instance(type op, formula<T>* child);
+
+      typedef typename T::visitor visitor;
+      typedef typename T::const_visitor const_visitor;
+
+      virtual void accept(visitor& v);
+      virtual void accept(const_visitor& v) const;
+
+      /// Get the sole operand of this operator.
+      const formula<T>* child() const;
+      /// Get the sole operand of this operator.
+      formula<T>* child();
+
+      /// Get the type of this operator.
+      type op() const;
+      /// Get the type of this operator, as a string.
+      const char* op_name() const;
+
+      /// Number of instantiated unary operators.  For debugging.
+      static unsigned instance_count();
+
+    protected:
+      typedef std::pair<type, formula<T>*> pair;
+      typedef std::map<pair, formula<T>*> map;
+      static map instances;
+
+      unop(type op, formula<T>* child);
+      virtual ~unop();
+
+    private:
+      type op_;
+      formula<T>* child_;
+    };
+
+  }
+}
+
+# include "unop.hxx"
+
+#endif // SPOT_INTERNAL_UNOP_HH
--- a/src/internal/unop.hxx
+++ b/src/internal/unop.hxx
@ -0,0 +1,122 @@
+// Copyright (C) 2003, 2005  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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+/// \file internal/unop.hxx
+/// \brief Generic unary operators implementation
+#ifndef SPOT_INTERNAL_UNOP_HXX
+# define SPOT_INTERNAL_UNOP_HXX
+
+#include "unop.hh"
+
+namespace spot
+{
+  namespace internal
+  {
+    template<typename T>
+    unop<T>::unop(type op, formula<T>* child)
+      : op_(op), child_(child)
+    {
+      this->dump_ = "unop(";
+      this->dump_ += op_name();
+      this->dump_ += ", " + child->dump() + ")";
+      this->set_key_();
+    }
+
+    template<typename T>
+    unop<T>::~unop()
+    {
+      // Get this instance out of the instance map.
+      pair p(op(), child());
+      typename map::iterator i = instances.find(p);
+      assert (i != instances.end());
+      instances.erase(i);
+    }
+
+    template<typename T>
+    void
+    unop<T>::accept(visitor& v)
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    void
+    unop<T>::accept(const_visitor& v) const
+    {
+      v.visit(this);
+    }
+
+    template<typename T>
+    const formula<T>*
+    unop<T>::child() const
+    {
+      return child_;
+    }
+
+    template<typename T>
+    formula<T>*
+    unop<T>::child()
+    {
+      return child_;
+    }
+
+    template<typename T>
+    typename unop<T>::type
+    unop<T>::op() const
+    {
+      return op_;
+    }
+
+    template<typename T>
+    const char*
+    unop<T>::op_name() const
+    {
+      return T::unop_name(op_);
+    }
+
+    template<typename T>
+    typename unop<T>::map unop<T>::instances;
+
+    template<typename T>
+    unop<T>*
+    unop<T>::instance(type op, formula<T>* child)
+    {
+      pair p(op, child);
+      typename map::iterator i = instances.find(p);
+      if (i != instances.end())
+	{
+	  return static_cast<unop<T>*>(i->second->ref());
+	}
+      unop<T>* ap = new unop<T>(op, child);
+      instances[p] = ap;
+      return static_cast<unop<T>*>(ap->ref());
+    }
+
+    template<typename T>
+    unsigned
+    unop<T>::instance_count()
+    {
+      return instances.size();
+    }
+  }
+}
+
+#endif // SPOT_INTERNAL_UNOP_HXX
--- a/src/ltlast/Makefile.am
+++ b/src/ltlast/Makefile.am
@ -19,9 +19,6 @@
 ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 ## 02111-1307, USA.

-AM_CPPFLAGS = -I$(srcdir)/..
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
-
 ltlastdir = $(pkgincludedir)/ltlast

 ltlast_HEADERS = \
@ -31,17 +28,6 @@ ltlast_HEADERS = \
  constant.hh \
  formula.hh \
  multop.hh \
-  predecl.hh \
  refformula.hh \
  unop.hh \
  visitor.hh
-
-noinst_LTLIBRARIES = libltlast.la
-libltlast_la_SOURCES = \
-  atomic_prop.cc \
-  binop.cc \
-  constant.cc \
-  formula.cc \
-  multop.cc \
-  refformula.cc \
-  unop.cc
--- a/src/ltlast/allnodes.hh
+++ b/src/ltlast/allnodes.hh
@ -23,8 +23,6 @@
 /// \brief Define all LTL node types.
 ///
 /// This file is usually needed when \b defining a visitor.
-/// Prefer ltlast/predecl.hh when only \b declaring methods and functions
-/// over LTL nodes.
 #ifndef SPOT_LTLAST_ALLNODES_HH
 # define SPOT_LTLAST_ALLNODES_HH

--- a/src/ltlast/atomic_prop.hh
+++ b/src/ltlast/atomic_prop.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -24,11 +24,8 @@
 #ifndef SPOT_LTLAST_ATOMIC_PROP_HH
 # define SPOT_LTLAST_ATOMIC_PROP_HH

-#include <string>
-#include <iosfwd>
-#include <map>
-#include "refformula.hh"
-#include "ltlenv/environment.hh"
+# include "formula.hh"
+# include "internal/atomic_prop.hh"

 namespace spot
 {
@ -37,38 +34,7 @@ namespace spot

    /// \brief Atomic propositions.
    /// \ingroup ltl_ast
-    class atomic_prop : public ref_formula
-    {
-    public:
-      /// Build an atomic proposition with name \a name in
-      /// environment \a env.
-      static atomic_prop* instance(const std::string& name, environment& env);
-
-      virtual void accept(visitor& visitor);
-      virtual void accept(const_visitor& visitor) const;
-
-      /// Get the name of the atomic proposition.
-      const std::string& name() const;
-      /// Get the environment of the atomic proposition.
-      environment& env() const;
-
-      /// Number of instantiated atomic propositions.  For debugging.
-      static unsigned instance_count();
-      /// List all instances of atomic propositions.  For debugging.
-      static std::ostream& dump_instances(std::ostream& os);
-
-    protected:
-      atomic_prop(const std::string& name, environment& env);
-      virtual ~atomic_prop();
-
-      typedef std::pair<std::string, environment*> pair;
-      typedef std::map<pair, atomic_prop*> map;
-      static map instances;
-
-    private:
-      std::string name_;
-      environment* env_;
-    };
+    typedef spot::internal::atomic_prop<ltl_t> atomic_prop;

  }
 }
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -27,8 +27,8 @@
 #ifndef SPOT_LTLAST_BINOP_HH
 # define SPOT_LTLAST_BINOP_HH

-#include <map>
-#include "refformula.hh"
+# include "formula.hh"
+# include "internal/binop.hh"

 namespace spot
 {
@ -37,53 +37,7 @@ namespace spot

    /// \brief Binary operator.
    /// \ingroup ltl_ast
-    class binop : public ref_formula
-    {
-    public:
-      /// Different kinds of binary opertaors
-      ///
-      /// And and Or are not here.  Because they
-      /// are often nested we represent them as multops.
-      enum type { Xor, Implies, Equiv, U, R };
-
-      /// Build an unary operator with operation \a op and
-      /// children \a first and \a second.
-      static binop* instance(type op, formula* first, formula* second);
-
-      virtual void accept(visitor& v);
-      virtual void accept(const_visitor& v) const;
-
-      /// Get the first operand.
-      const formula* first() const;
-      /// Get the first operand.
-      formula* first();
-      /// Get the second operand.
-      const formula* second() const;
-      /// Get the second operand.
-      formula* second();
-
-      /// Get the type of this operator.
-      type op() const;
-      /// Get the type of this operator, as a string.
-      const char* op_name() const;
-
-      /// Number of instantiated binary operators.  For debugging.
-      static unsigned instance_count();
-
-    protected:
-      typedef std::pair<formula*, formula*> pairf;
-      typedef std::pair<type, pairf> pair;
-      typedef std::map<pair, formula*> map;
-      static map instances;
-
-      binop(type op, formula* first, formula* second);
-      virtual ~binop();
-
-    private:
-      type op_;
-      formula* first_;
-      formula* second_;
-    };
+    typedef spot::internal::binop<ltl_t> binop;

  }
 }
--- a/src/ltlast/constant.hh
+++ b/src/ltlast/constant.hh
@ -24,7 +24,8 @@
 #ifndef SPOT_LTLAST_CONSTANT_HH
 # define SPOT_LTLAST_CONSTANT_HH

-#include "formula.hh"
+# include "formula.hh"
+# include "internal/constant.hh"

 namespace spot
 {
@ -33,30 +34,7 @@ namespace spot

    /// \brief A constant (True or False)
    /// \ingroup ltl_ast
-    class constant : public formula
-    {
-    public:
-      enum type { False, True };
-      virtual void accept(visitor& v);
-      virtual void accept(const_visitor& v) const;
-
-      /// Return the value of the constant.
-      type val() const;
-      /// Return the value of the constant as a string.
-      const char* val_name() const;
-
-      /// Get the sole instance of spot::ltl::constant::constant(True).
-      static constant* true_instance();
-      /// Get the sole instance of spot::ltl::constant::constant(False).
-      static constant* false_instance();
-
-    protected:
-      constant(type val);
-      virtual ~constant();
-
-    private:
-      type val_;
-    };
+    typedef spot::internal::constant<ltl_t> constant;

  }
 }
--- a/src/ltlast/formula.hh
+++ b/src/ltlast/formula.hh
@ -24,9 +24,7 @@
 #ifndef SPOT_LTLAST_FORMULA_HH
 # define SPOT_LTLAST_FORMULA_HH

-#include <string>
-#include <cassert>
-#include "predecl.hh"
+# include "internal/formula.hh"

 namespace spot
 {
@ -61,6 +59,54 @@ namespace spot
    /// \addtogroup ltl_misc Miscellaneous algorithms for LTL formulae
    /// \ingroup ltl_algorithm

+    struct visitor;
+    struct const_visitor;
+
+    struct ltl_t
+    {
+      typedef spot::ltl::visitor visitor;
+      typedef spot::ltl::const_visitor const_visitor;
+
+      enum binop { Xor, Implies, Equiv, U, R };
+      const char* binop_name(binop op) const
+      {
+	switch (op)
+      	{
+	  case Xor:
+	    return "Xor";
+	  case Implies:
+	    return "Implies";
+	  case Equiv:
+	    return "Equiv";
+	  case U:
+	    return "U";
+	  case R:
+	    return "R";
+      	}
+	// Unreachable code.
+	assert(0);
+	return 0;
+      }
+
+      enum unop { Not, X, F, G };
+      const char* unop_name(unop op) const
+      {
+	switch (op)
+	{
+	  case Not:
+	    return "Not";
+	  case X:
+	    return "X";
+	  case F:
+	    return "F";
+	  case G:
+	    return "G";
+	}
+	// Unreachable code.
+	assert(0);
+	return 0;
+      }
+    };

    /// \brief An LTL formula.
    /// \ingroup ltl_essential
@ -68,114 +114,10 @@ namespace spot
    ///
    /// The only way you can work with a formula is to
    /// build a spot::ltl::visitor or spot::ltl::const_visitor.
-    class formula
-    {
-    public:
-      /// Entry point for vspot::ltl::visitor instances.
-      virtual void accept(visitor& v) = 0;
-      /// Entry point for vspot::ltl::const_visitor instances.
-      virtual void accept(const_visitor& v) const = 0;
-
-      /// \brief clone this node
-      ///
-      /// This increments the reference counter of this node (if one is
-      /// used).  You should almost never use this method directly as
-      /// it doesn't touch the children.  If you want to clone a
-      /// whole formula, use spot::ltl::clone() instead.
-      formula* ref();
-      /// \brief release this node
-      ///
-      /// This decrements the reference counter of this node (if one is
-      /// used) and can free the object.  You should almost never use
-      /// this method directly as it doesn't touch the children.  If you
-      /// want to release a whole formula, use spot::ltl::destroy() instead.
-      static void unref(formula* f);
-
-      /// Return a canonic representation of the formula
-      const std::string& dump() const;
-
-      /// Return a hash_key for the formula.
-      size_t
-      hash() const
-      {
-	return hash_key_;
-      }
-    protected:
-      virtual ~formula();
-
-      /// \brief increment reference counter if any
-      virtual void ref_();
-      /// \brief decrement reference counter if any, return true when
-      /// the instance must be deleted (usually when the counter hits 0).
-      virtual bool unref_();
-
-      /// \brief Compute key_ from dump_.
-      ///
-      /// Should be called once in each object, after dump_ has been set.
-      void set_key_();
-      /// The canonic representation of the formula
-      std::string dump_;
-      /// \brief The hash key of this formula.
-      ///
-      /// Initialized by set_key_().
-      size_t hash_key_;
-    };
-
-    /// \brief Strict Weak Ordering for <code>const formula*</code>.
-    /// \ingroup ltl_essentials
-    ///
-    /// This is meant to be used as a comparison functor for
-    /// STL \c map whose key are of type <code>const formula*</code>.
-    ///
-    /// For instance here is how one could declare
-    /// a map of \c const::formula*.
-    /// \code
-    ///   // Remember how many times each formula has been seen.
-    ///   std::map<const spot::ltl::formula*, int,
-    ///            spot::formula_ptr_less_than> seen;
-    /// \endcode
-    struct formula_ptr_less_than:
-      public std::binary_function<const formula*, const formula*, bool>
-    {
-      bool
-      operator()(const formula* left, const formula* right) const
-      {
-	assert(left);
-	assert(right);
-	size_t l = left->hash();
-	size_t r = right->hash();
-	if (1 != r)
-	  return l < r;
-	return left->dump() < right->dump();
-      }
-    };
-
-    /// \brief Hash Function for <code>const formula*</code>.
-    /// \ingroup ltl_essentials
-    /// \ingroup hash_funcs
-    ///
-    /// This is meant to be used as a hash functor for
-    /// Sgi's \c hash_map whose key are of type <code>const formula*</code>.
-    ///
-    /// For instance here is how one could declare
-    /// a map of \c const::formula*.
-    /// \code
-    ///   // Remember how many times each formula has been seen.
-    ///   Sgi::hash_map<const spot::ltl::formula*, int,
-    ///                 const spot::ltl::formula_ptr_hash> seen;
-    /// \endcode
-    struct formula_ptr_hash:
-      public std::unary_function<const formula*, size_t>
-    {
-      size_t
-      operator()(const formula* that) const
-      {
-	assert(that);
-	return that->hash();
-      }
-    };
-
+    typedef spot::internal::formula<ltl_t> formula;

+    typedef spot::internal::formula_ptr_less_than<ltl_t> formula_ptr_less_than;
+    typedef spot::internal::formula_ptr_hash<ltl_t> formula_ptr_hash;
  }
 }

--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -24,9 +24,8 @@
 #ifndef SPOT_LTLAST_MULTOP_HH
 # define SPOT_LTLAST_MULTOP_HH

-#include <vector>
-#include <map>
-#include "refformula.hh"
+# include "formula.hh"
+# include "internal/multop.hh"

 namespace spot
 {
@ -37,87 +36,7 @@ namespace spot
    /// \ingroup ltl_ast
    ///
    /// These operators are considered commutative and associative.
-    class multop : public ref_formula
-    {
-    public:
-      enum type { Or, And };
-
-      /// List of formulae.
-      typedef std::vector<formula*> vec;
-
-      /// \brief Build a spot::ltl::multop with two children.
-      ///
-      /// If one of the children itself is a spot::ltl::multop
-      /// with the same type, it will be merged.  I.e., children
-      /// if that child will be added, and that child itself will
-      /// be destroyed.  This allows incremental building of
-      /// n-ary ltl::multop.
-      ///
-      /// This functions can perform slight optimizations and
-      /// may not return an ltl::multop objects.  For instance
-      /// if \c first and \c second are equal, that formula is
-      /// returned as-is.
-      static formula* instance(type op, formula* first, formula* second);
-
-      /// \brief Build a spot::ltl::multop with many children.
-      ///
-      /// Same as the other instance() function, but take a vector of
-      /// formula in argument.  This vector is acquired by the
-      /// spot::ltl::multop class, the caller should allocate it with
-      /// \c new, but not use it (especially not destroy it) after it
-      /// has been passed to spot::ltl::multop.
-      ///
-      /// This functions can perform slight optimizations and
-      /// may not return an ltl::multop objects.  For instance
-      /// if the vector contain only one unique element, this
-      /// this formula will be returned as-is.
-      static formula* instance(type op, vec* v);
-
-      virtual void accept(visitor& v);
-      virtual void accept(const_visitor& v) const;
-
-      /// Get the number of children.
-      unsigned size() const;
-      /// \brief Get the nth children.
-      ///
-      /// Starting with \a n = 0.
-      const formula* nth(unsigned n) const;
-      /// \brief Get the nth children.
-      ///
-      /// Starting with \a n = 0.
-      formula* nth(unsigned n);
-
-      /// Get the type of this operator.
-      type op() const;
-      /// Get the type of this operator, as a string.
-      const char* op_name() const;
-
-      /// Number of instantiated multi-operand operators.  For debugging.
-      static unsigned instance_count();
-
-    protected:
-      typedef std::pair<type, vec*> pair;
-      /// Comparison functor used internally by ltl::multop.
-      struct paircmp
-      {
-	bool
-	operator () (const pair& p1, const pair& p2) const
-	{
-	  if (p1.first != p2.first)
-	    return p1.first < p2.first;
-	  return *p1.second < *p2.second;
-	}
-      };
-      typedef std::map<pair, formula*, paircmp> map;
-      static map instances;
-
-      multop(type op, vec* v);
-      virtual ~multop();
-
-    private:
-      type op_;
-      vec* children_;
-    };
+    typedef spot::internal::multop<ltl_t> multop;

  }
 }
--- a/src/ltlast/refformula.hh
+++ b/src/ltlast/refformula.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -24,7 +24,8 @@
 #ifndef SPOT_LTLAST_REFFORMULA_HH
 # define SPOT_LTLAST_REFFORMULA_HH

-#include "formula.hh"
+# include "formula.hh"
+# include "internal/refformula.hh"

 namespace spot
 {
@ -33,18 +34,7 @@ namespace spot

    /// \brief A reference-counted LTL formula.
    /// \ingroup ltl_ast
-    class ref_formula : public formula
-    {
-    protected:
-      virtual ~ref_formula();
-      ref_formula();
-      void ref_();
-      bool unref_();
-      /// Number of references to this formula.
-      unsigned ref_count_();
-    private:
-      unsigned ref_counter_;
-    };
+    typedef spot::internal::ref_formula<ltl_t> ref_formula;

  }
 }
--- a/src/ltlast/unop.hh
+++ b/src/ltlast/unop.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -24,8 +24,8 @@
 #ifndef SPOT_LTLAST_UNOP_HH
 # define SPOT_LTLAST_UNOP_HH

-#include <map>
-#include "refformula.hh"
+# include "formula.hh"
+# include "internal/unop.hh"

 namespace spot
 {
@ -34,43 +34,7 @@ namespace spot

    /// \brief Unary operators.
    /// \ingroup ltl_ast
-    class unop : public ref_formula
-    {
-    public:
-      enum type { Not, X, F, G };
-
-      /// Build an unary operator with operation \a op and
-      /// child \a child.
-      static unop* instance(type op, formula* child);
-
-      virtual void accept(visitor& v);
-      virtual void accept(const_visitor& v) const;
-
-      /// Get the sole operand of this operator.
-      const formula* child() const;
-      /// Get the sole operand of this operator.
-      formula* child();
-
-      /// Get the type of this operator.
-      type op() const;
-      /// Get the type of this operator, as a string.
-      const char* op_name() const;
-
-      /// Number of instantiated unary operators.  For debugging.
-      static unsigned instance_count();
-
-    protected:
-      typedef std::pair<type, formula*> pair;
-      typedef std::map<pair, formula*> map;
-      static map instances;
-
-      unop(type op, formula* child);
-      virtual ~unop();
-
-    private:
-      type op_;
-      formula* child_;
-    };
+    typedef spot::internal::unop<ltl_t> unop;

  }
 }
--- a/src/ltlast/visitor.hh
+++ b/src/ltlast/visitor.hh
@ -1,6 +1,6 @@
-// Copyright (C) 2003, 2004, 2005  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, 2008 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.
 //
@ -24,7 +24,11 @@
 #ifndef SPOT_LTLAST_VISITOR_HH
 # define SPOT_LTLAST_VISITOR_HH

-#include "predecl.hh"
+# include "binop.hh"
+# include "unop.hh"
+# include "multop.hh"
+# include "atomic_prop.hh"
+# include "constant.hh"

 namespace spot
 {
@ -67,7 +71,6 @@ namespace spot
      virtual void visit(const multop* node) = 0;
    };

-
  }
 }

--- a/src/ltlenv/Makefile.am
+++ b/src/ltlenv/Makefile.am
@ -19,17 +19,9 @@
 ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 ## 02111-1307, USA.

-AM_CPPFLAGS = -I$(srcdir)/..
-AM_CXXFLAGS = $(WARNING_CXXFLAGS)
-
 ltlenvdir = $(pkgincludedir)/ltlenv

 ltlenv_HEADERS = \
-  declenv.hh \
  defaultenv.hh \
+  declenv.hh \
  environment.hh
-
-noinst_LTLIBRARIES = libltlenv.la
-libltlenv_la_SOURCES = \
-  declenv.cc \
-  defaultenv.cc
--- a/src/ltlenv/declenv.hh
+++ b/src/ltlenv/declenv.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -23,10 +23,7 @@
 # define SPOT_LTLENV_DECLENV_HH

 # include "environment.hh"
-# include <string>
-# include <map>
-# include "ltlvisit/destroy.hh"
-# include "ltlast/atomic_prop.hh"
+# include "internal/declenv.hh"

 namespace spot
 {
@ -38,29 +35,9 @@ namespace spot
    ///
    /// This environment recognizes all atomic propositions
    /// that have been previously declared.  It will reject other.
-    class declarative_environment : public environment
-    {
-    public:
-      declarative_environment();
-      ~declarative_environment();
+    typedef spot::internal::declarative_environment<ltl_t>
+    declarative_environment;

-      /// Declare an atomic proposition.  Return false iff the
-      /// proposition was already declared.
-      bool declare(const std::string& prop_str);
-
-      virtual ltl::formula* require(const std::string& prop_str);
-
-      /// Get the name of the environment.
-      virtual const std::string& name();
-
-      typedef std::map<const std::string, ltl::atomic_prop*> prop_map;
-
-      /// Get the map of atomic proposition known to this environment.
-      const prop_map& get_prop_map() const;
-
-    private:
-      prop_map props_;
-    };
  }
 }

--- a/src/ltlenv/defaultenv.hh
+++ b/src/ltlenv/defaultenv.hh
@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2008 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@ -23,6 +23,7 @@
 # define SPOT_LTLENV_DEFAULTENV_HH

 # include "environment.hh"
+# include "internal/defaultenv.hh"

 namespace spot
 {
@ -36,18 +37,7 @@ namespace spot
    ///
    /// This is a singleton.  Use default_environment::instance()
    /// to obtain the instance.
-    class default_environment : public environment
-    {
-    public:
-      virtual ~default_environment();
-      virtual formula* require(const std::string& prop_str);
-      virtual const std::string& name();
-
-      /// Get the sole instance of spot::ltl::default_environment.
-      static default_environment& instance();
-    protected:
-      default_environment();
-    };
+    typedef spot::internal::default_environment<ltl_t> default_environment;

  }
 }
--- a/src/ltlenv/environment.hh
+++ b/src/ltlenv/environment.hh
@ -23,7 +23,7 @@
 # define SPOT_LTLENV_ENVIRONMENT_HH

 # include "ltlast/formula.hh"
-# include <string>
+# include "internal/environment.hh"

 namespace spot
 {
@ -31,37 +31,7 @@ namespace spot
  {
    /// \brief An environment that describes atomic propositions.
    /// \ingroup ltl_essential
-    class environment
-    {
-    public:
-      /// \brief Obtain the formula associated to \a prop_str
-      ///
-      /// Usually \a prop_str, is the name of an atomic proposition,
-      /// and spot::ltl::require simply returns the associated
-      /// spot::ltl::atomic_prop.
-      ///
-      /// Note this is not a \c const method.  Some environments will
-      /// "create" the atomic proposition when requested.
-      ///
-      /// We return a spot::ltl::formula instead of an
-      /// spot::ltl::atomic_prop, because this
-      /// will allow nifty tricks (e.g., we could name formulae in an
-      /// environment, and let the parser build a larger tree from
-      /// these).
-      ///
-      /// \return 0 iff \a prop_str is not part of the environment,
-      ///   or the associated spot::ltl::formula otherwise.
-      virtual formula* require(const std::string& prop_str) = 0;
-
-      /// Get the name of the environment.
-      virtual const std::string& name() = 0;
-
-      virtual
-      ~environment()
-      {
-      }
-    };
-
+    typedef spot::internal::environment<ltl_t> environment;
  }
 }

--- a/src/ltlparse/public.hh
+++ b/src/ltlparse/public.hh
@ -23,6 +23,7 @@
 # define SPOT_LTLPARSE_PUBLIC_HH

 # include "ltlast/formula.hh"
+# include "ltlast/visitor.hh"
 // Unfortunately Bison 2.3 uses the same guards in all parsers :(
 # undef BISON_LOCATION_HH
 # undef BISON_POSITION_HH
--- a/src/ltlvisit/randomltl.cc
+++ b/src/ltlvisit/randomltl.cc
@ -23,6 +23,7 @@
 #include <algorithm>
 #include "randomltl.hh"
 #include "ltlast/allnodes.hh"
+#include "ltlast/visitor.hh"
 #include "misc/random.hh"
 #include <iostream>
 #include <cstring>
--- a/src/tgba/tgbatba.cc
+++ b/src/tgba/tgbatba.cc
@ -23,6 +23,7 @@
 #include "tgbatba.hh"
 #include "bddprint.hh"
 #include "ltlast/constant.hh"
+#include "ltlast/visitor.hh"
 #include "misc/hashfunc.hh"

 namespace spot
--- a/src/tgbaalgos/randomgraph.hh
+++ b/src/tgbaalgos/randomgraph.hh
@ -23,6 +23,7 @@
 # define SPOT_TGBAALGOS_RANDOMGRAPH_HH

 #include "ltlvisit/apcollect.hh"
+#include "ltlast/visitor.hh"
 #include "ltlenv/defaultenv.hh"

 namespace spot
--- a/src/tgbaparse/public.hh
+++ b/src/tgbaparse/public.hh
@ -27,6 +27,7 @@
 # undef BISON_LOCATION_HH
 # undef BISON_POSITION_HH
 # include "tgbaparse/location.hh"
+# include "ltlast/visitor.hh"
 # include "ltlenv/defaultenv.hh"
 # include <string>
 # include <list>
--- a/src/tgbatest/explicit.cc
+++ b/src/tgbatest/explicit.cc
@ -25,6 +25,7 @@
 #include "tgba/tgbaexplicit.hh"
 #include "tgbaalgos/dotty.hh"
 #include "ltlast/allnodes.hh"
+#include "ltlast/visitor.hh"

 int
 main()