* src/ltltest/randltl.cc: Include cassert.

* src/tgbaalgos/ndfs_result.hxx: Implement the spot::acss_statistics
interface.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc: Add to each heap class a method returning its
size.

ChangeLog

@@ -1,3 +1,13 @@
+2005-01-06  Denis Poitrenaud  <Denis.Poitrenaud@lip6.fr>
+
+	* src/ltltest/randltl.cc: Include cassert.
+
+	* src/tgbaalgos/ndfs_result.hxx: Implement the spot::acss_statistics
+	interface.
+	* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
+	src/tgbaalgos/tau03opt.cc: Add to each heap class a method returning its
+	size.
+
 2005-01-06  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltltest/randltl.cc: Add options -r and -u.

src/ltltest/randltl.cc

@@ -19,6 +19,7 @@
 // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 // 02111-1307, USA.
 
+#include <cassert>
 #include <iostream>
 #include <set>
 #include <string>

src/tgbaalgos/magic.cc

@@ -387,6 +387,11 @@ namespace spot
           return (it != h.end());
         }
 
+      int size() const
+        {
+          return h.size();
+        }
+
     private:
 
       typedef Sgi::hash_map<const state*, color,
@@ -422,9 +427,9 @@ namespace spot
 
       bsh_magic_search_heap(size_t s)
         {
-          size = s;
-          h = new unsigned char[size];
-          memset(h, WHITE, size);
+          size_ = s;
+          h = new unsigned char[size_];
+          memset(h, WHITE, size_);
         }
 
       ~bsh_magic_search_heap()
@@ -435,7 +440,7 @@ namespace spot
       color_ref get_color_ref(const state*& s)
         {
           size_t ha = s->hash();
-          return color_ref(&(h[ha%size]), ha%4);
+          return color_ref(&(h[ha%size_]), ha%4);
         }
 
       void add_new_state(const state* s, color c)
@@ -453,11 +458,18 @@ namespace spot
       bool has_been_visited(const state* s) const
         {
           size_t ha = s->hash();
-          return color((h[ha%size] >> ((ha%4)*2)) & 3U) != WHITE;
+          return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
+        }
+
+      int size() const
+        {
+          // this method must return the number of state stored in the heap. Due
+          // to potential conflicts this size cannot be computed.
+          return 0;
         }
 
     private:
-      size_t size;
+      size_t size_;
       unsigned char* h;
     };
 

src/tgbaalgos/ndfs_result.hxx

@@ -64,14 +64,22 @@ namespace spot
   template <typename ndfs_search, typename heap>
   class ndfs_result:
     public emptiness_check_result,
-    public ars_statistics
+    public ars_statistics,
+    public acss_statistics
   {
   public:
     ndfs_result(const ndfs_search& ms)
-      : emptiness_check_result(ms.automaton()), ms_(ms), h_(ms_.get_heap())
+      : emptiness_check_result(ms.automaton()), ms_(ms),
+        h_(ms_.get_heap())
     {
     }
 
+    int acss_states() const
+    {
+      // all visited states are in the state space search
+      return h_.size();
+    }
+
     virtual ~ndfs_result()
     {
     }

src/tgbaalgos/se05.cc

@@ -445,6 +445,11 @@ namespace spot
           return true;
         }
 
+      int size() const
+        {
+          return h.size() + hc.size();
+        }
+
     private:
 
       hash_type h; // associate to each blue and red state its color
@@ -497,10 +502,10 @@ namespace spot
         unsigned char o;
       };
 
-      bsh_se05_search_heap(size_t s) : size(s)
+      bsh_se05_search_heap(size_t s) : size_(s)
         {
-          h = new unsigned char[size];
-          memset(h, WHITE, size);
+          h = new unsigned char[size_];
+          memset(h, WHITE, size_);
         }
 
       ~bsh_se05_search_heap()
@@ -513,8 +518,8 @@ namespace spot
           size_t ha = s->hash();
           hcyan_type::iterator ic = hc.find(s);
           if (ic!=hc.end())
-            return color_ref(&hc, *ic, &h[ha%size], ha%4);
-          return color_ref(&h[ha%size], ha%4);
+            return color_ref(&hc, *ic, &h[ha%size_], ha%4);
+          return color_ref(&h[ha%size_], ha%4);
         }
 
       void add_new_state(const state* s, color c)
@@ -540,11 +545,18 @@ namespace spot
           if (ic != hc.end())
             return true;
           size_t ha = s->hash();
-          return color((h[ha%size] >> ((ha%4)*2)) & 3U) != WHITE;
+          return color((h[ha%size_] >> ((ha%4)*2)) & 3U) != WHITE;
+        }
+
+      int size() const
+        {
+          // this method must return the number of state stored in the heap. Due
+          // to potential conflicts this size cannot be computed.
+          return 0;
         }
 
     private:
-      size_t size;
+      size_t size_;
       unsigned char* h;
       hcyan_type hc;
     };

src/tgbaalgos/tau03.cc

@@ -360,6 +360,11 @@ namespace spot
           hash_type::const_iterator it = h.find(s);
           return (it != h.end());
         }
+
+      int size() const
+        {
+          return h.size();
+        }
     private:
 
       typedef Sgi::hash_map<const state*, std::pair<color, bdd>,

src/tgbaalgos/tau03opt.cc

@@ -481,6 +481,11 @@ namespace spot
           return true;
         }
 
+      int size() const
+        {
+          return h.size() + hc.size();
+        }
+
     private:
 
       // associate to each blue and red state its color and its acceptance set