From fb4873d92e32c9dbaad0bfecc87bb8241f9201e0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 23 Oct 2003 15:49:29 +0000
Subject: [PATCH] * src/tgbaalgos/emptinesscheck.hh
 (connected_component::set_of_state): Rename as ...
 (connected_component::set_type): ... this, and define as a hash_set.
 (connected_component::has_state): New method. *
 src/tgbaalgos/emptinesscheck.cc (connected_component::has_state): New method.
 (emptiness_check::counter_example, emptiness_check::complete_cycle,
 emptiness_check::accepting_path): Simplify using has_state().

---
 ChangeLog                       |  9 +++++++++
 src/tgbaalgos/emptinesscheck.cc | 28 +++++++++++++---------------
 src/tgbaalgos/emptinesscheck.hh | 12 +++++++-----
 3 files changed, 29 insertions(+), 20 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 419899e9e..4df7f168b 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,14 @@
 2003-10-23  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgbaalgos/emptinesscheck.hh (connected_component::set_of_state):
+	Rename as ...
+	(connected_component::set_type): ... this, and define as a hash_set.
+	(connected_component::has_state): New method.
+	* src/tgbaalgos/emptinesscheck.cc (connected_component::has_state):
+	New method.
+	(emptiness_check::counter_example, emptiness_check::complete_cycle,
+	emptiness_check::accepting_path): Simplify using has_state().
+
 	* src/tgbaalgos/emptinesscheck.hh (emptiness_check::seen_state_num):
 	Rename as ...
 	(emptiness_check::h): ... this, and define as a hash_map.
diff --git a/src/tgbaalgos/emptinesscheck.cc b/src/tgbaalgos/emptinesscheck.cc
index 9665d3e56..200b2effd 100644
--- a/src/tgbaalgos/emptinesscheck.cc
+++ b/src/tgbaalgos/emptinesscheck.cc
@@ -16,6 +16,12 @@ namespace spot
     condition = bddfalse;
   }
 
+  bool
+  connected_component::has_state(const state* s) const
+  {
+    return state_set.find(s) != state_set.end();
+  }
+
 
   emptiness_check::emptiness_check(const tgba* a)
     : aut_(a)
@@ -62,7 +68,7 @@ namespace spot
     arc_accepting.push(bddfalse);
     tgba_succ_iterator* iter_ = aut_->succ_iter(init);
     iter_->first();
-    todo.push(pair_state_iter(init, iter_ ));
+    todo.push(pair_state_iter(init, iter_));
     while (!todo.empty())
       {
 	pair_state_iter step = todo.top();
@@ -105,7 +111,7 @@ namespace spot
 		arc_accepting.push(current_accepting);
 		tgba_succ_iterator* iter2 = aut_->succ_iter(current_state);
 		iter2->first();
-		todo.push(pair_state_iter(current_state, iter2 ));
+		todo.push(pair_state_iter(current_state, iter2));
 	      }
 	    else if (h[current_state] != -1)
 	      {
@@ -254,12 +260,10 @@ namespace spot
 		  {
 		    const state* curr_state =
 		      started_from.second->current_state();
-		    connected_component::set_of_state::iterator iter_set =
-		      vec_component[k+1].state_set.find(curr_state);
-		    if (iter_set != vec_component[k+1].state_set.end())
+		    if (vec_component[k+1].has_state(curr_state))
 		      {
 			const state* curr_father = started_from.first;
-			seq.push_front(*iter_set);
+			seq.push_front(curr_state);
 			seq.push_front(curr_father);
 			hash_type::iterator i_2 = h.find(curr_father);
 			assert(i_2 != h.end());
@@ -278,9 +282,7 @@ namespace spot
 		      }
 		    else
 		      {
-			connected_component::set_of_state::iterator i_s =
-			  vec_component[k].state_set.find(curr_state);
-			if (i_s != vec_component[k].state_set.end())
+			if (vec_component[k].has_state(curr_state))
 			  {
 			    path_state::iterator i_path =
 			      path_map.find(curr_state);
@@ -339,9 +341,7 @@ namespace spot
 	    for (iter_s->first(); !iter_s->done(); iter_s->next())
 	      {
 		const state* curr_state = (started_.second)->current_state();
-		connected_component::set_of_state::iterator i_set =
-		  comp_path.state_set.find(curr_state);
-		if (i_set != comp_path.state_set.end())
+		if (comp_path.has_state(curr_state))
 		  {
 		    if (curr_state->compare(to_state) == 0)
 		      {
@@ -402,9 +402,7 @@ namespace spot
 	else
 	  {
 	    state* curr_state = iter_->current_state();
-	    connected_component::set_of_state::iterator it_set =
-	      comp_path.state_set.find(curr_state);
-	    if (it_set != comp_path.state_set.end())
+	    if (comp_path.has_state(curr_state))
 	      {
 		hash_type::iterator i = seen_priority.find(curr_state);
 		if (i == seen_priority.end())
diff --git a/src/tgbaalgos/emptinesscheck.hh b/src/tgbaalgos/emptinesscheck.hh
index a2b9d3d10..083652b5b 100644
--- a/src/tgbaalgos/emptinesscheck.hh
+++ b/src/tgbaalgos/emptinesscheck.hh
@@ -5,7 +5,6 @@
 #include "misc/hash.hh"
 #include <stack>
 #include <list>
-#include <set>
 #include <utility>
 #include <iostream>
 
@@ -23,12 +22,15 @@ namespace spot
     /// The bdd condition is the union of all accepting condition of
     /// transitions which connect the states of the connected component.
     bdd condition;
-    typedef std::set<const spot::state*,
-                     spot::state_ptr_less_than> set_of_state;
 
+    typedef Sgi::hash_set<const state*,
+			  state_ptr_hash, state_ptr_equal> set_type;
     /// for the counter example we need to know all the states of the
     /// component
-    set_of_state state_set;
+    set_type state_set;
+
+    /// Check if the SCC contains states \a s.
+    bool has_state(const state* s) const;
   };
 
   /// \brief Check whether the language of an automate is empty.
@@ -54,7 +56,7 @@ namespace spot
   class emptiness_check
   {
     typedef std::list<const state*> state_sequence;
-    typedef std::pair<const spot::state*, bdd> state_proposition;
+    typedef std::pair<const state*, bdd> state_proposition;
     typedef std::list<state_proposition> cycle_path;
   public:
     emptiness_check(const tgba* a);