From 4e22bb8b0999efe826445c3e63ca79a46b4d41b7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 10 Nov 2009 12:16:33 +0100
Subject: [PATCH] Introduce tgba_explicit_labelled<label> so that we can build
 tgba_explicit instances labelled by other objects than strings.

* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Split tgba_explicit in two levels: tgba_explicit with unlabelled
states, and tgba_explicit_labelled templated by the type of
the label.  Define tgba_explicit_string (with the interface
of the former tgba_explicit class) and tgba_explicit_formula
for future use in ltl2tgba.cc.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
use tgba_explicit_string when appropriate.
---
 ChangeLog                    |  19 ++++
 src/tgba/tgbaexplicit.cc     | 165 +++++++---------------------
 src/tgba/tgbaexplicit.hh     | 201 +++++++++++++++++++++++++++++++----
 src/tgba/tgbareduc.cc        |  24 ++---
 src/tgba/tgbareduc.hh        |   4 +-
 src/tgbaalgos/cutscc.cc      |   3 +-
 src/tgbaalgos/dupexp.cc      |   8 +-
 src/tgbaalgos/emptiness.cc   |   4 +-
 src/tgbaalgos/ltl2tgba_fm.cc |   5 +-
 src/tgbaalgos/powerset.cc    |   4 +-
 src/tgbaalgos/randomgraph.cc |   2 +-
 src/tgbaparse/public.hh      |  22 ++--
 src/tgbaparse/tgbaparse.yy   |   6 +-
 src/tgbatest/explicit.cc     |   4 +-
 src/tgbatest/ltl2tgba.cc     |   4 +-
 15 files changed, 284 insertions(+), 191 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 200a6f4c6..19aa80c00 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,22 @@
+2009-11-10  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Introduce tgba_explicit_labelled<label> so that we can build
+	tgba_explicit instances labelled by other objects than strings.
+
+	* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
+	Split tgba_explicit in two levels: tgba_explicit with unlabelled
+	states, and tgba_explicit_labelled templated by the type of
+	the label.  Define tgba_explicit_string (with the interface
+	of the former tgba_explicit class) and tgba_explicit_formula
+	for future use in ltl2tgba.cc.
+	* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
+	src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
+	src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
+	src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
+	src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
+	src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
+	use tgba_explicit_string when appropriate.
+
 2009-11-09  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Do not use the Boost macro from the Autoconf macro archive.
diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc
index 291f4791b..279bca058 100644
--- a/src/tgba/tgbaexplicit.cc
+++ b/src/tgba/tgbaexplicit.cc
@@ -25,6 +25,7 @@
 #include "tgba/formula2bdd.hh"
 #include "misc/bddop.hh"
 #include <cassert>
+#include "ltlvisit/tostring.hh"
 
 namespace spot
 {
@@ -121,45 +122,9 @@ namespace spot
 
   tgba_explicit::~tgba_explicit()
   {
-    ns_map::iterator i;
-    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      {
-	tgba_explicit::state::iterator i2;
-	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
-	  delete *i2;
-	delete i->second;
-      }
     dict_->unregister_all_my_variables(this);
   }
 
-  tgba_explicit::state*
-  tgba_explicit::add_state(const std::string& name)
-  {
-    ns_map::iterator i = name_state_map_.find(name);
-    if (i == name_state_map_.end())
-      {
-	tgba_explicit::state* s = new tgba_explicit::state;
-	name_state_map_[name] = s;
-	state_name_map_[s] = name;
-
-	// The first state we add is the inititial state.
-	// It can also be overridden with set_init_state().
-	if (!init_)
-	  init_ = s;
-
-	return s;
-      }
-    return i->second;
-  }
-
-  tgba_explicit::state*
-  tgba_explicit::set_init_state(const std::string& state)
-  {
-    tgba_explicit::state* s = add_state(state);
-    init_ = s;
-    return s;
-  }
-
   tgba_explicit::transition*
   tgba_explicit::create_transition(state* source, const state* dest)
   {
@@ -170,18 +135,6 @@ namespace spot
     source->push_back(t);
     return t;
   }
-
-  tgba_explicit::transition*
-  tgba_explicit::create_transition(const std::string& source,
-				   const std::string& dest)
-  {
-    // It's important that the source be created before the
-    // destination, so the first encountered source becomes the
-    // default initial state.
-    state* s = add_state(source);
-    return create_transition(s, add_state(dest));
-  }
-
   void
   tgba_explicit::add_condition(transition* t, const ltl::formula* f)
   {
@@ -196,26 +149,6 @@ namespace spot
     t->condition &= f;
   }
 
-  void
-  tgba_explicit::declare_acceptance_condition(const ltl::formula* f)
-  {
-    int v = dict_->register_acceptance_variable(f, this);
-    f->destroy();
-    bdd neg = bdd_nithvar(v);
-    neg_acceptance_conditions_ &= neg;
-
-    // Append neg to all acceptance conditions.
-    ns_map::iterator i;
-    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      {
-	tgba_explicit::state::iterator i2;
-	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
-	  (*i2)->acceptance_conditions &= neg;
-      }
-
-    all_acceptance_conditions_computed_ = false;
-  }
-
   void
   tgba_explicit::copy_acceptance_conditions_of(const tgba *a)
   {
@@ -226,52 +159,6 @@ namespace spot
     neg_acceptance_conditions_ = f;
   }
 
-  void
-  tgba_explicit::complement_all_acceptance_conditions()
-  {
-    bdd all = all_acceptance_conditions();
-    ns_map::iterator i;
-    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      {
-	tgba_explicit::state::iterator i2;
-	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
-	  {
-	    (*i2)->acceptance_conditions = all - (*i2)->acceptance_conditions;
-	  }
-      }
-  }
-
-  void
-  tgba_explicit::merge_transitions()
-  {
-    ns_map::iterator i;
-    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
-      {
-	state::iterator t1;
-	for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
-	  {
-	    bdd acc = (*t1)->acceptance_conditions;
-	    const state* dest = (*t1)->dest;
-
-	    // Find another transition with the same destination and
-	    // acceptance conditions.
-	    state::iterator t2 = t1;
-	    ++t2;
-	    while (t2 != i->second->end())
-	      {
-		state::iterator t2copy = t2++;
-		if ((*t2copy)->acceptance_conditions == acc
-		    && (*t2copy)->dest == dest)
-		  {
-		    (*t1)->condition |= (*t2copy)->condition;
-		    delete *t2copy;
-		    i->second->erase(t2copy);
-		  }
-	      }
-	  }
-      }
-  }
-
   bool
   tgba_explicit::has_acceptance_condition(const ltl::formula* f) const
   {
@@ -317,7 +204,7 @@ namespace spot
   {
     // Fix empty automata by adding a lone initial state.
     if (!init_)
-      const_cast<tgba_explicit*>(this)->add_state("empty");
+      const_cast<tgba_explicit*>(this)->add_default_init();
     return new state_explicit(init_);
   }
 
@@ -368,16 +255,6 @@ namespace spot
     return dict_;
   }
 
-  std::string
-  tgba_explicit::format_state(const spot::state* s) const
-  {
-    const state_explicit* se = dynamic_cast<const state_explicit*>(s);
-    assert(se);
-    sn_map::const_iterator i = state_name_map_.find(se->get_state());
-    assert(i != state_name_map_.end());
-    return i->second;
-  }
-
   bdd
   tgba_explicit::all_acceptance_conditions() const
   {
@@ -396,4 +273,42 @@ namespace spot
     return neg_acceptance_conditions_;
   }
 
+  tgba_explicit::state*
+  tgba_explicit_string::add_default_init()
+  {
+    return add_state("empty");
+  }
+
+  std::string
+  tgba_explicit_string::format_state(const spot::state* s) const
+  {
+    const state_explicit* se = dynamic_cast<const state_explicit*>(s);
+    assert(se);
+    sn_map::const_iterator i = state_name_map_.find(se->get_state());
+    assert(i != state_name_map_.end());
+    return i->second;
+  }
+
+  tgba_explicit_formula::~tgba_explicit_formula()
+  {
+    ns_map::iterator i;
+    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+      i->first->destroy();
+  }
+
+  tgba_explicit::state* tgba_explicit_formula::add_default_init()
+  {
+    return add_state(ltl::constant::true_instance());
+  }
+
+  std::string
+  tgba_explicit_formula::format_state(const spot::state* s) const
+  {
+    const state_explicit* se = dynamic_cast<const state_explicit*>(s);
+    assert(se);
+    sn_map::const_iterator i = state_name_map_.find(se->get_state());
+    assert(i != state_name_map_.end());
+    return ltl::to_string(i->second);
+  }
+
 }
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index 78026ad7c..2eb03278c 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -1,6 +1,6 @@
-// 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.
+// Copyright (C) 2003, 2004, 2006, 2009 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.
 //
@@ -26,12 +26,14 @@
 #include <list>
 #include "tgba.hh"
 #include "ltlast/formula.hh"
+#include <cassert>
 
 namespace spot
 {
   // Forward declarations.  See below.
   class state_explicit;
   class tgba_explicit_succ_iterator;
+  class tgba_explicit;
 
   /// Explicit representation of a spot::tgba.
   /// \ingroup tgba_representation
@@ -51,17 +53,15 @@ namespace spot
       const state* dest;
     };
 
-    state* set_init_state(const std::string& state);
+    /// Add a default initial state.
+    virtual state* add_default_init() = 0;
 
-    transition*
-    create_transition(const std::string& source, const std::string& dest);
     transition*
     create_transition(state* source, const state* dest);
 
     void add_condition(transition* t, const ltl::formula* f);
     /// This assumes that all variables in \a f are known from dict.
     void add_conditions(transition* t, bdd f);
-    void declare_acceptance_condition(const ltl::formula* f);
 
     /// \brief Copy the acceptance conditions of a tgba.
     ///
@@ -73,12 +73,6 @@ namespace spot
     void add_acceptance_condition(transition* t, const ltl::formula* f);
     /// This assumes that all acceptance conditions in \a f are known from dict.
     void add_acceptance_conditions(transition* t, bdd f);
-    void complement_all_acceptance_conditions();
-    void merge_transitions();
-
-    /// Return the tgba_explicit::state for \a name, creating the state if
-    /// it does not exist.
-    state* add_state(const std::string& name);
 
     // tgba interface
     virtual ~tgba_explicit();
@@ -88,23 +82,18 @@ namespace spot
 	      const spot::state* global_state = 0,
 	      const tgba* global_automaton = 0) const;
     virtual bdd_dict* get_dict() const;
-    virtual std::string format_state(const spot::state* state) const;
 
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
 
+    virtual std::string format_state(const spot::state* s) const = 0;
+
   protected:
     virtual bdd compute_support_conditions(const spot::state* state) const;
     virtual bdd compute_support_variables(const spot::state* state) const;
 
     bdd get_acceptance_condition(const ltl::formula* f);
 
-    typedef Sgi::hash_map<const std::string, tgba_explicit::state*,
-			  string_hash> ns_map;
-    typedef Sgi::hash_map<const tgba_explicit::state*, std::string,
-			  ptr_hash<tgba_explicit::state> > sn_map;
-    ns_map name_state_map_;
-    sn_map state_name_map_;
     bdd_dict* dict_;
     tgba_explicit::state* init_;
     mutable bdd all_acceptance_conditions_;
@@ -118,6 +107,7 @@ namespace spot
   };
 
 
+
   /// States used by spot::tgba_explicit.
   /// \ingroup tgba_representation
   class state_explicit : public spot::state
@@ -168,6 +158,177 @@ namespace spot
     bdd all_acceptance_conditions_;
   };
 
+  /// A tgba_explicit instance with states labeled by a given type.
+  template<typename label, typename label_hash>
+  class tgba_explicit_labelled: public tgba_explicit
+  {
+  protected:
+    typedef label label_t;
+    typedef Sgi::hash_map<label, tgba_explicit::state*,
+			  label_hash> ns_map;
+    typedef Sgi::hash_map<const tgba_explicit::state*, label,
+			  ptr_hash<tgba_explicit::state> > sn_map;
+    ns_map name_state_map_;
+    sn_map state_name_map_;
+  public:
+    tgba_explicit_labelled(bdd_dict* dict) : tgba_explicit(dict) {};
+
+    bool has_state(const label& name)
+    {
+      return name_state_map_.find(name) != name_state_map_.end();
+    }
+
+    /// Return the tgba_explicit::state for \a name, creating the state if
+    /// it does not exist.
+    state* add_state(const label& name)
+    {
+      typename ns_map::iterator i = name_state_map_.find(name);
+      if (i == name_state_map_.end())
+	{
+	  tgba_explicit::state* s = new tgba_explicit::state;
+	  name_state_map_[name] = s;
+	  state_name_map_[s] = name;
+
+	  // The first state we add is the inititial state.
+	  // It can also be overridden with set_init_state().
+	  if (!init_)
+	    init_ = s;
+
+	  return s;
+	}
+      return i->second;
+    }
+
+    state*
+    set_init_state(const label& state)
+    {
+      tgba_explicit::state* s = add_state(state);
+      init_ = s;
+      return s;
+    }
+
+
+    transition*
+    create_transition(state* source, const state* dest)
+    {
+      return tgba_explicit::create_transition(source, dest);
+    }
+
+    transition*
+    create_transition(const label& source, const label& dest)
+    {
+      // It's important that the source be created before the
+      // destination, so the first source encountered becomes the
+      // default initial state.
+      state* s = add_state(source);
+      return tgba_explicit::create_transition(s, add_state(dest));
+    }
+
+    void
+    complement_all_acceptance_conditions()
+    {
+      bdd all = all_acceptance_conditions();
+      typename ns_map::iterator i;
+      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+	{
+	  tgba_explicit::state::iterator i2;
+	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	    {
+	      (*i2)->acceptance_conditions = all - (*i2)->acceptance_conditions;
+	    }
+	}
+    }
+
+    void
+    declare_acceptance_condition(const ltl::formula* f)
+    {
+      int v = dict_->register_acceptance_variable(f, this);
+      f->destroy();
+      bdd neg = bdd_nithvar(v);
+      neg_acceptance_conditions_ &= neg;
+
+      // Append neg to all acceptance conditions.
+      typename ns_map::iterator i;
+      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+	{
+	  tgba_explicit::state::iterator i2;
+	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	    (*i2)->acceptance_conditions &= neg;
+	}
+
+      all_acceptance_conditions_computed_ = false;
+    }
+
+
+    void
+    merge_transitions()
+    {
+      typename ns_map::iterator i;
+      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+	{
+	  state::iterator t1;
+	  for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
+	    {
+	      bdd acc = (*t1)->acceptance_conditions;
+	      const state* dest = (*t1)->dest;
+
+	      // Find another transition with the same destination and
+	      // acceptance conditions.
+	      state::iterator t2 = t1;
+	      ++t2;
+	      while (t2 != i->second->end())
+		{
+		  state::iterator t2copy = t2++;
+		  if ((*t2copy)->acceptance_conditions == acc
+		      && (*t2copy)->dest == dest)
+		    {
+		      (*t1)->condition |= (*t2copy)->condition;
+		      delete *t2copy;
+		      i->second->erase(t2copy);
+		    }
+		}
+	    }
+	}
+    }
+
+
+    virtual
+    ~tgba_explicit_labelled()
+    {
+      typename ns_map::iterator i;
+      for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
+	{
+	  tgba_explicit::state::iterator i2;
+	  for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
+	    delete *i2;
+	  delete i->second;
+	}
+    }
+
+  };
+
+  class tgba_explicit_string:
+    public tgba_explicit_labelled<std::string, string_hash>
+  {
+  public:
+    tgba_explicit_string(bdd_dict* dict):
+      tgba_explicit_labelled<std::string, string_hash>(dict)
+    {};
+    virtual state* add_default_init();
+    virtual std::string format_state(const spot::state* s) const;
+  };
+
+  class tgba_explicit_formula:
+    public tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>
+  {
+  public:
+    tgba_explicit_formula(bdd_dict* dict):
+      tgba_explicit_labelled<const ltl::formula*, ltl::formula_ptr_hash>(dict)
+    {};
+    virtual ~tgba_explicit_formula();
+    virtual state* add_default_init();
+    virtual std::string format_state(const spot::state* s) const;
+  };
 }
 
 #endif // SPOT_TGBA_TGBAEXPLICIT_HH
diff --git a/src/tgba/tgbareduc.cc b/src/tgba/tgbareduc.cc
index 89571697a..54f9ca167 100644
--- a/src/tgba/tgbareduc.cc
+++ b/src/tgba/tgbareduc.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2004, 2005, 2008 Laboratoire d'Informatique de Paris
+// Copyright (C) 2004, 2005, 2008, 2009 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
 //
@@ -31,7 +31,7 @@ namespace spot
 
   tgba_reduc::tgba_reduc(const tgba* a,
 			 const numbered_state_heap_factory* nshf)
-    : tgba_explicit(a->get_dict()),
+    : tgba_explicit_string(a->get_dict()),
       tgba_reachable_iterator_breadth_first(a),
       h_(nshf->build())
   {
@@ -203,10 +203,8 @@ namespace spot
     const std::string ss = automata_->format_state(source);
     const std::string sd = automata_->format_state(dest);
 
-    tgba_explicit::state* s
-      = tgba_explicit::add_state(ss);
-    tgba_explicit::state* d
-      = tgba_explicit::add_state(sd);
+    tgba_explicit::state* s = tgba_explicit_string::add_state(ss);
+    tgba_explicit::state* d = tgba_explicit_string::add_state(sd);
 
     transition* t = new transition();
     t->dest = d;
@@ -241,9 +239,9 @@ namespace spot
     bdd acc_simul;
     std::list<state*> ltmp;
     const tgba_explicit::state* s1 =
-      name_state_map_[tgba_explicit::format_state(s)];
+      name_state_map_[tgba_explicit_string::format_state(s)];
     const tgba_explicit::state* s2 =
-      name_state_map_[tgba_explicit::format_state(simul)];
+      name_state_map_[tgba_explicit_string::format_state(simul)];
 
     sp_map::iterator i = state_predecessor_map_.find(s1);
     if (i == state_predecessor_map_.end()) // 0 predecessor
@@ -323,12 +321,12 @@ namespace spot
     // predecessor in state_predecessor_map_.
 
     ns_map::iterator k =
-      name_state_map_.find(tgba_explicit::format_state(s));
+      name_state_map_.find(tgba_explicit_string::format_state(s));
     if (k == name_state_map_.end()) // 0 predecessor
 	return;
 
     tgba_explicit::state* st =
-      name_state_map_[tgba_explicit::format_state(s)];
+      name_state_map_[tgba_explicit_string::format_state(s)];
 
     // for all successor q of s, we remove s of the predecessor of q.
     // Note that the initial node can't be removed.
@@ -370,9 +368,9 @@ namespace spot
   tgba_reduc::merge_state(const spot::state* sim1, const spot::state* sim2)
   {
     const tgba_explicit::state* s1 =
-      name_state_map_[tgba_explicit::format_state(sim1)];
+      name_state_map_[tgba_explicit_string::format_state(sim1)];
     const tgba_explicit::state* s2 =
-      name_state_map_[tgba_explicit::format_state(sim2)];
+      name_state_map_[tgba_explicit_string::format_state(sim2)];
     const tgba_explicit::state* stmp = s1;
     const spot::state* simtmp = sim1;
 
@@ -612,7 +610,7 @@ namespace spot
 
 	if (sm->second == n)
 	  {
-	    s1 = name_state_map_[tgba_explicit::format_state(s)];
+	    s1 = name_state_map_[tgba_explicit_string::format_state(s)];
 	    s1 = const_cast<tgba_explicit::state*>(s1);
 	    for (state::iterator i = s1->begin();
 		 i != s1->end(); ++i)
diff --git a/src/tgba/tgbareduc.hh b/src/tgba/tgbareduc.hh
index 0ab5cd218..486c364aa 100644
--- a/src/tgba/tgbareduc.hh
+++ b/src/tgba/tgbareduc.hh
@@ -1,4 +1,4 @@
-// Copyright (C) 2004, 2005, 2006, 2008 Laboratoire d'Informatique de
+// Copyright (C) 2004, 2005, 2006, 2008, 2009 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
 //
@@ -51,7 +51,7 @@ namespace spot
   /// Explicit automata used in reductions.
   /// \ingroup tgba_representation
   class tgba_reduc:
-    public tgba_explicit, public tgba_reachable_iterator_breadth_first
+    public tgba_explicit_string, public tgba_reachable_iterator_breadth_first
   {
   public:
     tgba_reduc(const tgba* a,
diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc
index 3cd2dcaf0..101f5246f 100644
--- a/src/tgbaalgos/cutscc.cc
+++ b/src/tgbaalgos/cutscc.cc
@@ -39,7 +39,7 @@ namespace spot
   tgba* cut_scc(const tgba* a, const scc_map& m,
 		const std::set<unsigned>* s)
   {
-    tgba_explicit* sub_a = new tgba_explicit(a->get_dict());
+    tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict());
     state* cur = a->get_init_state();
     std::queue<state*> tovisit;
     typedef Sgi::hash_set<const state*,
@@ -418,4 +418,3 @@ namespace spot
     return iter_count;
   }
 }
-
diff --git a/src/tgbaalgos/dupexp.cc b/src/tgbaalgos/dupexp.cc
index 850198c90..f9fe192ce 100644
--- a/src/tgbaalgos/dupexp.cc
+++ b/src/tgbaalgos/dupexp.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -34,12 +34,12 @@ namespace spot
     {
     public:
       dupexp_iter(const tgba* a)
-	: T(a), out_(new tgba_explicit(a->get_dict()))
+	: T(a), out_(new tgba_explicit_string(a->get_dict()))
       {
 	out_->copy_acceptance_conditions_of(a);
       }
 
-      tgba_explicit*
+      tgba_explicit_string*
       result()
       {
 	return out_;
@@ -62,7 +62,7 @@ namespace spot
       }
 
     private:
-      tgba_explicit* out_;
+      tgba_explicit_string* out_;
     };
 
   } // anonymous
diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc
index 26c01b2dd..cbbb77acf 100644
--- a/src/tgbaalgos/emptiness.cc
+++ b/src/tgbaalgos/emptiness.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2005, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -292,7 +292,7 @@ namespace spot
   tgba*
   tgba_run_to_tgba(const tgba* a, const tgba_run* run)
   {
-    tgba_explicit* res = new tgba_explicit(a->get_dict());
+    tgba_explicit_string* res = new tgba_explicit_string(a->get_dict());
     res->copy_acceptance_conditions_of(a);
 
     const state* s = a->get_init_state();
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index 26a06caca..ae1e656b3 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -195,7 +195,8 @@ namespace spot
       }
 
       void
-      conj_bdd_to_acc(tgba_explicit* a, bdd b, tgba_explicit::transition* t)
+      conj_bdd_to_acc(tgba_explicit_string* a, bdd b,
+		      tgba_explicit::transition* t)
       {
 	assert(b != bddfalse);
 	while (b != bddtrue)
@@ -775,7 +776,7 @@ namespace spot
     formulae_seen.insert(f2);
     formulae_to_translate.insert(f2);
 
-    tgba_explicit* a = new tgba_explicit(dict);
+    tgba_explicit_string* a = new tgba_explicit_string(dict);
 
     a->set_init_state(to_string(f2));
 
diff --git a/src/tgbaalgos/powerset.cc b/src/tgbaalgos/powerset.cc
index e3dcb14f2..6f54a5d6a 100644
--- a/src/tgbaalgos/powerset.cc
+++ b/src/tgbaalgos/powerset.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -40,7 +40,7 @@ namespace spot
 
     power_set seen;
     todo_list todo;
-    tgba_explicit* res = new tgba_explicit(aut->get_dict());
+    tgba_explicit_string* res = new tgba_explicit_string(aut->get_dict());
 
     state_set states;
 
diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc
index eeee47223..07fad17b7 100644
--- a/src/tgbaalgos/randomgraph.cc
+++ b/src/tgbaalgos/randomgraph.cc
@@ -95,7 +95,7 @@ namespace spot
 	       ltl::environment* env)
   {
     assert(n > 0);
-    tgba_explicit* res = new tgba_explicit(dict);
+    tgba_explicit_string* res = new tgba_explicit_string(dict);
 
     int props_n = ap->size();
     int* props = new int[props_n];
diff --git a/src/tgbaparse/public.hh b/src/tgbaparse/public.hh
index 652ae6a28..80c061c2e 100644
--- a/src/tgbaparse/public.hh
+++ b/src/tgbaparse/public.hh
@@ -1,6 +1,6 @@
-// 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.
+// Copyright (C) 2003, 2004, 2005, 2006, 2009 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.
 //
@@ -62,14 +62,14 @@ namespace spot
   /// was parsed succesfully, check \a error_list for emptiness.
   ///
   /// \warning This function is not reentrant.
-  tgba_explicit* tgba_parse(const std::string& filename,
-			    tgba_parse_error_list& error_list,
-			    bdd_dict* dict,
-			    ltl::environment& env
-			    = ltl::default_environment::instance(),
-			    ltl::environment& envacc
-			    = ltl::default_environment::instance(),
-			    bool debug = false);
+  tgba_explicit_string* tgba_parse(const std::string& filename,
+				   tgba_parse_error_list& error_list,
+				   bdd_dict* dict,
+				   ltl::environment& env
+				   = ltl::default_environment::instance(),
+				   ltl::environment& envacc
+				   = ltl::default_environment::instance(),
+				   bool debug = false);
 
   /// \brief Format diagnostics produced by spot::tgba_parse.
   /// \param os Where diagnostics should be output.
diff --git a/src/tgbaparse/tgbaparse.yy b/src/tgbaparse/tgbaparse.yy
index b2fdd6155..67c7606e4 100644
--- a/src/tgbaparse/tgbaparse.yy
+++ b/src/tgbaparse/tgbaparse.yy
@@ -41,7 +41,7 @@ typedef std::map<std::string, bdd> formula_cache;
 %parse-param {spot::tgba_parse_error_list& error_list}
 %parse-param {spot::ltl::environment& parse_environment}
 %parse-param {spot::ltl::environment& parse_envacc}
-%parse-param {spot::tgba_explicit*& result}
+%parse-param {spot::tgba_explicit_string*& result}
 %parse-param {formula_cache& fcache}
 %union
 {
@@ -233,7 +233,7 @@ tgbayy::parser::error(const location_type& location,
 
 namespace spot
 {
-  tgba_explicit*
+  tgba_explicit_string*
   tgba_parse(const std::string& name,
 	     tgba_parse_error_list& error_list,
 	     bdd_dict* dict,
@@ -249,7 +249,7 @@ namespace spot
 	return 0;
       }
     formula_cache fcache;
-    tgba_explicit* result = new tgba_explicit(dict);
+    tgba_explicit_string* result = new tgba_explicit_string(dict);
     tgbayy::parser parser(error_list, env, envacc, result, fcache);
     parser.set_debug_level(debug);
     parser.parse();
diff --git a/src/tgbatest/explicit.cc b/src/tgbatest/explicit.cc
index e917d5b6d..4862a2b96 100644
--- a/src/tgbatest/explicit.cc
+++ b/src/tgbatest/explicit.cc
@@ -1,4 +1,4 @@
-// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+// Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
 //
@@ -33,7 +33,7 @@ main()
 
   spot::ltl::default_environment& e =
     spot::ltl::default_environment::instance();
-  spot::tgba_explicit* a = new spot::tgba_explicit(dict);
+  spot::tgba_explicit_string* a = new spot::tgba_explicit_string(dict);
 
   typedef spot::tgba_explicit::transition trans;
 
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 6f11d935c..1db9521a2 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -202,7 +202,7 @@ main(int argc, char** argv)
   bool show_fc = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
-  spot::tgba_explicit* system = 0;
+  spot::tgba_explicit_string* system = 0;
   spot::tgba* product = 0;
   spot::tgba* product_to_free = 0;
   spot::bdd_dict* dict = new spot::bdd_dict();
@@ -574,7 +574,7 @@ main(int argc, char** argv)
       if (from_file)
 	{
 	  spot::tgba_parse_error_list pel;
-	  spot::tgba_explicit* e;
+	  spot::tgba_explicit_string* e;
 	  tm.start("parsing automaton");
 	  to_free = a = e = spot::tgba_parse(input, pel, dict,
 					     env, env, debug_opt);