From 603b49e21654e54c76c4c740f5796cc153e4b8c3 Mon Sep 17 00:00:00 2001 From: Denis Poitrenaud Date: Thu, 6 Jan 2005 15:54:48 +0000 Subject: [PATCH] * 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 | 10 ++++++++++ src/ltltest/randltl.cc | 1 + src/tgbaalgos/magic.cc | 24 ++++++++++++++++++------ src/tgbaalgos/ndfs_result.hxx | 12 ++++++++++-- src/tgbaalgos/se05.cc | 26 +++++++++++++++++++------- src/tgbaalgos/tau03.cc | 5 +++++ src/tgbaalgos/tau03opt.cc | 5 +++++ 7 files changed, 68 insertions(+), 15 deletions(-) diff --git a/ChangeLog b/ChangeLog index cbec05642..215a2c5a4 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,13 @@ +2005-01-06 Denis Poitrenaud + + * 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 * src/ltltest/randltl.cc: Add options -r and -u. diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc index ea9d7aee9..a8e285eb1 100644 --- a/src/ltltest/randltl.cc +++ b/src/ltltest/randltl.cc @@ -19,6 +19,7 @@ // Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA // 02111-1307, USA. +#include #include #include #include diff --git a/src/tgbaalgos/magic.cc b/src/tgbaalgos/magic.cc index 539ef9a76..6f86b0ed8 100644 --- a/src/tgbaalgos/magic.cc +++ b/src/tgbaalgos/magic.cc @@ -387,6 +387,11 @@ namespace spot return (it != h.end()); } + int size() const + { + return h.size(); + } + private: typedef Sgi::hash_maphash(); - 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; }; diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index dbbe2a992..f8c543761 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -64,14 +64,22 @@ namespace spot template 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() { } diff --git a/src/tgbaalgos/se05.cc b/src/tgbaalgos/se05.cc index e4b76f7ba..e11371444 100644 --- a/src/tgbaalgos/se05.cc +++ b/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; }; diff --git a/src/tgbaalgos/tau03.cc b/src/tgbaalgos/tau03.cc index 1897c7822..49d9e5302 100644 --- a/src/tgbaalgos/tau03.cc +++ b/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, diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 5e3542123..8f5ccce2a 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/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