* 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

@@ -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.

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)
@@ -254,12 +260,10 @@ namespace spot
 		  {
 		    const state* curr_state =
 		      started_from.second->current_state();
-		    connected_component::set_of_state::iterator iter_set =
+		    if (vec_component[k+1].has_state(curr_state))
-		      vec_component[k+1].state_set.find(curr_state);
-		    if (iter_set != vec_component[k+1].state_set.end())
 		      {
 			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 =
+			if (vec_component[k].has_state(curr_state))
-			  vec_component[k].state_set.find(curr_state);
-			if (i_s != vec_component[k].state_set.end())
 			  {
 			    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 =
+		if (comp_path.has_state(curr_state))
-		  comp_path.state_set.find(curr_state);
-		if (i_set != comp_path.state_set.end())
 		  {
 		    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 =
+	    if (comp_path.has_state(curr_state))
-	      comp_path.state_set.find(curr_state);
-	    if (it_set != comp_path.state_set.end())
 	      {
 		hash_type::iterator i = seen_priority.find(curr_state);
 		if (i == seen_priority.end())

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);