From f0de38680a18863d727a3b21b4d37ff5e1f7873c Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 29 Aug 2003 15:54:31 +0000
Subject: [PATCH] * src/tgba/state.hh (state::hash): New method.
 (state_ptr_equal, state_ptr_hash): New functors. * src/tgba/statebdd.hh,
 src/tgba/statebdd.cc (state_bdd::hash): New method. *
 src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (state_explicit::hash):
 New method. (ns_map, sn_map): Use Sgi::hash_map instead of std::map. *
 src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (state_product::hash): New
 method. * src/tgba/tgbatba.cc (state_tba_proxy::hash): New method. *
 src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine using
 Sgi::hash_map or Sgi::hash_set. (lbtt_reachable): Don't erase a key that is
 pointed to by an iterator. * src/tgbaalgos/reachiter.cc
 (tgba_reachable_iterator::~tgba_reachable_iterator): Likewise. *
 src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise. *
 src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map. *
 src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map. *
 iface/gspn/gspn.cc (state_gspn::hash): New method. * src/misc/hash.hh
 (string_hash): New functor.

---
 ChangeLog                  | 22 +++++++++++++
 iface/gspn/gspn.cc         |  6 ++++
 src/misc/hash.hh           | 25 ++++++++++++---
 src/tgba/state.hh          | 66 ++++++++++++++++++++++++++++++++++++++
 src/tgba/statebdd.cc       |  6 ++++
 src/tgba/statebdd.hh       |  1 +
 src/tgba/tgbaexplicit.cc   |  7 ++++
 src/tgba/tgbaexplicit.hh   | 10 +++---
 src/tgba/tgbaproduct.cc    |  7 ++++
 src/tgba/tgbaproduct.hh    |  1 +
 src/tgba/tgbatba.cc        |  8 +++++
 src/tgbaalgos/lbtt.cc      | 40 ++++++++++++++++-------
 src/tgbaalgos/magic.cc     | 10 ++++--
 src/tgbaalgos/magic.hh     |  5 +--
 src/tgbaalgos/reachiter.cc | 10 ++++--
 src/tgbaalgos/reachiter.hh |  3 +-
 16 files changed, 201 insertions(+), 26 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 56759cb3d..48503c62e 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,27 @@
 2003-08-29  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/state.hh (state::hash): New method.
+	(state_ptr_equal, state_ptr_hash): New functors.
+	* src/tgba/statebdd.hh, src/tgba/statebdd.cc (state_bdd::hash):
+	New method.
+	* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
+	(state_explicit::hash): New method.
+	(ns_map, sn_map): Use Sgi::hash_map instead of std::map.
+	* src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc
+	(state_product::hash): New method.
+	* src/tgba/tgbatba.cc (state_tba_proxy::hash): New method.
+	* src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine
+	using Sgi::hash_map or Sgi::hash_set.
+	(lbtt_reachable): Don't erase a key that is pointed to by an
+	iterator.
+	* src/tgbaalgos/reachiter.cc
+	(tgba_reachable_iterator::~tgba_reachable_iterator): Likewise.
+	* src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise.
+	* src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map.
+	* src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map.
+	* iface/gspn/gspn.cc (state_gspn::hash): New method.
+	* src/misc/hash.hh (string_hash): New functor.
+
 	* src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions)
 	Compute all_accepting_conditions_ from neg_accepting_conditions_,
 	not by browsing the dictionary.  The dictionary also contains
diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc
index f20cec1bc..1278db654 100644
--- a/iface/gspn/gspn.cc
+++ b/iface/gspn/gspn.cc
@@ -48,6 +48,12 @@ namespace spot
 	- reinterpret_cast<char*>(get_state());
     }
 
+    virtual size_t
+    hash() const
+    {
+      return reinterpret_cast<char*>(get_state()) - static_cast<char*>(0);
+    }
+
     virtual state_gspn* clone() const
     {
       return new state_gspn(get_state());
diff --git a/src/misc/hash.hh b/src/misc/hash.hh
index 62782834e..379707b21 100644
--- a/src/misc/hash.hh
+++ b/src/misc/hash.hh
@@ -1,13 +1,19 @@
 #ifndef SPOT_MISC_HASH_HH
 #  define SPOT_MISC_HASH_HH
 
-// See the G++ FAQ for details about this.
+#  include <string>
 
+// See the G++ FAQ for details about the following.
 #  ifdef __GNUC__
 #  if __GNUC__ < 3
 #    include <hash_map.h>
 #    include <hash_set.h>
-    namespace Sgi { using ::hash_map; }; // inherit globals
+    namespace Sgi
+    { // inherit globals
+      using ::hash_map;
+      using ::hash_set;
+      using ::hash;
+    };
 #  else
 #    include <ext/hash_map>
 #    include <ext/hash_set>
@@ -30,9 +36,20 @@ namespace spot
   template <class T>
   struct ptr_hash
   {
-    size_t operator()(const T* f) const
+    size_t operator()(const T* p) const
     {
-      return reinterpret_cast<const char*>(f) - static_cast<const char*>(0);
+      return reinterpret_cast<const char*>(p) - static_cast<const char*>(0);
+    }
+  };
+
+  /// A hash function for strings.
+  struct string_hash : Sgi::hash<const char*>
+  {
+    size_t operator()(const std::string& s) const
+    {
+      // We are living dangerously.  Be sure to call operator()
+      // from the super-class, not this one.
+      return Sgi::hash<const char*>::operator()(s.c_str());
     }
   };
 }
diff --git a/src/tgba/state.hh b/src/tgba/state.hh
index 9584f94de..9e4e8325d 100644
--- a/src/tgba/state.hh
+++ b/src/tgba/state.hh
@@ -1,6 +1,7 @@
 #ifndef SPOT_TGBA_STATE_HH
 # define SPOT_TGBA_STATE_HH
 
+#include <cstddef>
 #include <bdd.h>
 
 namespace spot
@@ -22,6 +23,27 @@ namespace spot
     /// \sa spot::state_ptr_less_than
     virtual int compare(const state* other) const = 0;
 
+    /// \brief Hash a state.
+    ///
+    /// This method returns an integer that can be used as a
+    /// hash value for this state.
+    ///
+    /// Note that the hash value is guaranteed to be unique for all
+    /// equal states (in compare()'s sense) for only has long has one
+    /// of these states exists.  So it's OK to use a spot::state as a
+    /// key in a \c hash_map because the mere use of the state as a
+    /// key in the hash will ensure the state continues to exist.
+    ///
+    /// However if you create the state, get its hash key, delete the
+    /// state, recreate the same state, and get its hash key, you may
+    /// obtain two different hash keys if the same state were not
+    /// already used elsewhere.  In practice this weird situation can
+    /// occur only when the state is BDD-encoded, because BDD numbers
+    /// (used to build the hash value) can be reused for other
+    /// formulas.  That probably doesn't matter, since the hash value
+    /// is meant to be used in a \c hash_map, but it had to be noted.
+    virtual size_t hash() const = 0;
+
     /// Duplicate a state.
     virtual state* clone() const = 0;
 
@@ -51,6 +73,50 @@ namespace spot
     }
   };
 
+  /// \brief An Equivalence Relation for \c state*.
+  ///
+  /// This is meant to be used as a comparison functor for
+  /// Sgi \c hash_map whose key are of type \c state*.
+  ///
+  /// For instance here is how one could declare
+  /// a map of \c state*.
+  /// \code
+  ///   // Remember how many times each state has been visited.
+  ///   Sgi::hash_map<spot::state*, int, spot::state_ptr_less_than,
+  ///                                    spot::state_ptr_equal> seen;
+  /// \endcode
+  struct state_ptr_equal
+  {
+    bool
+    operator()(const state* left, const state* right) const
+    {
+      assert(left);
+      return 0 == left->compare(right);
+    }
+  };
+
+  /// \brief Hash Function for \c state*.
+  ///
+  /// This is meant to be used as a hash functor for
+  /// Sgi's \c hash_map whose key are of type \c state*.
+  ///
+  /// For instance here is how one could declare
+  /// a map of \c state*.
+  /// \code
+  ///   // Remember how many times each state has been visited.
+  ///   Sgi::hash_map<spot::state*, int, spot::state_ptr_less_than,
+  ///                                    spot::state_ptr_equal> seen;
+  /// \endcode
+  struct state_ptr_hash
+  {
+    size_t
+    operator()(const state* that) const
+    {
+      assert(that);
+      return that->hash();
+    }
+  };
+
 }
 
 #endif // SPOT_TGBA_STATE_HH
diff --git a/src/tgba/statebdd.cc b/src/tgba/statebdd.cc
index 852cd43a9..d5e12f84e 100644
--- a/src/tgba/statebdd.cc
+++ b/src/tgba/statebdd.cc
@@ -16,6 +16,12 @@ namespace spot
     return o->as_bdd().id() - state_.id();
   }
 
+  size_t
+  state_bdd::hash() const
+  {
+    return state_.id();
+  }
+
   /// Duplicate a state.
   state_bdd*
   state_bdd::clone() const
diff --git a/src/tgba/statebdd.hh b/src/tgba/statebdd.hh
index 6466f8d9a..60123fb03 100644
--- a/src/tgba/statebdd.hh
+++ b/src/tgba/statebdd.hh
@@ -23,6 +23,7 @@ namespace spot
     }
 
     virtual int compare(const state* other) const;
+    virtual size_t hash() const;
     virtual state_bdd* clone() const;
 
   protected:
diff --git a/src/tgba/tgbaexplicit.cc b/src/tgba/tgbaexplicit.cc
index a81d42931..02edc2b4d 100644
--- a/src/tgba/tgbaexplicit.cc
+++ b/src/tgba/tgbaexplicit.cc
@@ -70,6 +70,13 @@ namespace spot
     return o->get_state() - get_state();
   }
 
+  size_t
+  state_explicit::hash() const
+  {
+    return
+      reinterpret_cast<const char*>(get_state()) - static_cast<const char*>(0);
+  }
+
   state_explicit*
   state_explicit::clone() const
   {
diff --git a/src/tgba/tgbaexplicit.hh b/src/tgba/tgbaexplicit.hh
index 3138a6762..68295feca 100644
--- a/src/tgba/tgbaexplicit.hh
+++ b/src/tgba/tgbaexplicit.hh
@@ -1,8 +1,8 @@
 #ifndef SPOT_TGBA_TGBAEXPLICIT_HH
 # define SPOT_TGBA_TGBAEXPLICIT_HH
 
+#include "misc/hash.hh"
 #include <list>
-#include <map>
 #include "tgba.hh"
 #include "ltlast/formula.hh"
 
@@ -62,8 +62,10 @@ namespace spot
     bdd get_condition(ltl::formula* f);
     bdd get_accepting_condition(ltl::formula* f);
 
-    typedef std::map<const std::string, tgba_explicit::state*> ns_map;
-    typedef std::map<const tgba_explicit::state*, std::string> sn_map;
+    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_;
@@ -89,7 +91,7 @@ namespace spot
     }
 
     virtual int compare(const spot::state* other) const;
-
+    virtual size_t hash() const;
     virtual state_explicit* clone() const;
 
     virtual ~state_explicit()
diff --git a/src/tgba/tgbaproduct.cc b/src/tgba/tgbaproduct.cc
index a5a959d49..d5feb5697 100644
--- a/src/tgba/tgbaproduct.cc
+++ b/src/tgba/tgbaproduct.cc
@@ -32,6 +32,13 @@ namespace spot
     return right_->compare(o->right());
   }
 
+  size_t
+  state_product::hash() const
+  {
+    // We assume that size_t has at least 32bits.
+    return (left_->hash() << 16) + (right_->hash() & 0xFFFF);
+  }
+
   state_product*
   state_product::clone() const
   {
diff --git a/src/tgba/tgbaproduct.hh b/src/tgba/tgbaproduct.hh
index 6b7a19e90..eef1023a2 100644
--- a/src/tgba/tgbaproduct.hh
+++ b/src/tgba/tgbaproduct.hh
@@ -43,6 +43,7 @@ namespace spot
     }
 
     virtual int compare(const state* other) const;
+    virtual size_t hash() const;
     virtual state_product* clone() const;
 
   private:
diff --git a/src/tgba/tgbatba.cc b/src/tgba/tgbatba.cc
index 9c7160af3..f6f6be852 100644
--- a/src/tgba/tgbatba.cc
+++ b/src/tgba/tgbatba.cc
@@ -56,6 +56,14 @@ namespace spot
       return acc_.id() - o->accepting_cond().id();
     }
 
+    virtual size_t
+    hash() const
+    {
+      // We expect to have many more state than accepting conditions.
+      // Hence we keep only 8 bits for accepting conditions.
+      return (s_->hash() << 8) + (acc_.id() & 0xFF);
+    }
+
     virtual
     state_tba_proxy* clone() const
     {
diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc
index 73151095d..b060d5d73 100644
--- a/src/tgbaalgos/lbtt.cc
+++ b/src/tgbaalgos/lbtt.cc
@@ -1,3 +1,4 @@
+#include "misc/hash.hh"
 #include <map>
 #include <set>
 #include <string>
@@ -86,30 +87,41 @@ namespace spot
 
   typedef std::pair<state*, bdd> state_acc_pair;
 
-  struct state_acc_pair_less_than
+  struct state_acc_pair_equal
   {
     bool
     operator()(const state_acc_pair& left, const state_acc_pair& right) const
     {
-      int cmp = left.first->compare(right.first);
-      if (cmp < 0)
-	return true;
-      if (cmp > 0)
+      if (left.first->compare(right.first))
 	return false;
-      return left.second.id() < right.second.id();
+      return left.second.id() == right.second.id();
+    }
+  };
+
+  struct state_acc_pair_hash
+  {
+    bool
+    operator()(const state_acc_pair& that) const
+    {
+      // We assume there will be far more states than accepting conditions.
+      // Hence we keep only 8 bits for the latter.
+      return (that.first->hash() << 8) + (that.second.id() & 0xFF);
     }
   };
 
   // Each state of the produced automata is numbered.  Map of state seen.
-  typedef std::map<state_acc_pair, unsigned, state_acc_pair_less_than> acp_seen_map;
+  typedef Sgi::hash_map<state_acc_pair, unsigned, state_acc_pair_hash,
+			state_acc_pair_equal> acp_seen_map;
 
   // Set of states yet to produce.
-  typedef std::set<state_acc_pair, state_acc_pair_less_than> todo_set;
+  typedef Sgi::hash_set<state_acc_pair, state_acc_pair_hash,
+			state_acc_pair_equal> todo_set;
 
   // Each *source* state corresponds to several states in the produced
   // automata.  A minmax_pair specifies the range of such associated states.
   typedef std::pair<unsigned, unsigned> minmax_pair;
-  typedef std::map<state*, minmax_pair, state_ptr_less_than> seen_map;
+  typedef Sgi::hash_map<state*, minmax_pair,
+			state_ptr_hash, state_ptr_equal> seen_map;
 
   // Take a STATE from the source automaton, and fill TODO with
   // the list of associated states to output.  Return the correponding
@@ -230,8 +242,14 @@ namespace spot
     os << state_number << " " << acs.count() << std::endl;
     os << body.str();
     // Finally delete all states used as keys in m.
-    for (seen_map::iterator i = seen.begin(); i != seen.end(); ++i)
-      delete i->first;
+    seen_map::const_iterator s = seen.begin();
+    while (s != seen.end())
+      {
+	// Advance the iterator before deleting the "key" pointer.
+	const state* ptr = s->first;
+	++s;
+	delete ptr;
+      }
     return os;
   }
 }
diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc
index 0ba49f16a..f6bb1ddf2 100644
--- a/src/tgbaalgos/magic.cc
+++ b/src/tgbaalgos/magic.cc
@@ -12,8 +12,14 @@ namespace spot
 
   magic_search::~magic_search()
   {
-    for (hash_type::iterator i = h.begin(); i != h.end(); ++i)
-      delete i->first;
+    hash_type::const_iterator s = h.begin();
+    while (s != h.end())
+      {
+	// Advance the iterator before deleting the "key" pointer.
+	const state* ptr = s->first;
+	++s;
+	delete ptr;
+      }
     if (x)
       delete x;
   }
diff --git a/src/tgbaalgos/magic.hh b/src/tgbaalgos/magic.hh
index da2388adc..8c54810fa 100644
--- a/src/tgbaalgos/magic.hh
+++ b/src/tgbaalgos/magic.hh
@@ -1,6 +1,7 @@
 #ifndef SPOT_TGBAALGOS_MAGIC_HH
 # define SPOT_TGBAALGOS_MAGIC_HH
 
+#include "misc/hash.hh"
 #include <list>
 #include <utility>
 #include <ostream>
@@ -82,8 +83,8 @@ namespace spot
     /// This is an addition to the data from the paper.
     tstack_type tstack;
 
-    // FIXME: use a hash_map.
-    typedef std::map<const state*, magic, state_ptr_less_than> hash_type;
+    typedef Sgi::hash_map<const state*, magic,
+			  state_ptr_hash, state_ptr_equal> hash_type;
     hash_type h;		///< Map of visited states.
 
     /// Append a new state to the current path.
diff --git a/src/tgbaalgos/reachiter.cc b/src/tgbaalgos/reachiter.cc
index 4a68faf53..93eddb9c5 100644
--- a/src/tgbaalgos/reachiter.cc
+++ b/src/tgbaalgos/reachiter.cc
@@ -13,8 +13,14 @@ namespace spot
 
   tgba_reachable_iterator::~tgba_reachable_iterator()
   {
-    for (seen_map::const_iterator s = seen.begin(); s != seen.end(); ++s)
-      delete s->first;
+    seen_map::const_iterator s = seen.begin();
+    while (s != seen.end())
+      {
+	// Advance the iterator before deleting the "key" pointer.
+	const state* ptr = s->first;
+	++s;
+	delete ptr;
+      }
   }
 
   void
diff --git a/src/tgbaalgos/reachiter.hh b/src/tgbaalgos/reachiter.hh
index ea84df366..af8a4fdc7 100644
--- a/src/tgbaalgos/reachiter.hh
+++ b/src/tgbaalgos/reachiter.hh
@@ -56,7 +56,8 @@ namespace spot
   protected:
     const tgba* automata_;	///< The spot::tgba to explore.
 
-    typedef std::map<const state*, int, state_ptr_less_than> seen_map;
+    typedef Sgi::hash_map<const state*, int,
+			  state_ptr_hash, state_ptr_equal> seen_map;
     seen_map seen;		///< States already seen.
   };