From 8f0135ebb02a2066e37cabbd66b4fec4248bae0b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 24 Jan 2005 15:21:41 +0000 Subject: [PATCH] * src/tgbaalgos/emptiness_stats.hh (ars_statistics): Distinguish states visited to compute the prefix and those for the cycle. * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/gtec/ce.cc: Adjust. * src/tgbatest/randtgba.cc: Print both statistics. --- ChangeLog | 8 +++++ src/tgbaalgos/emptiness_stats.hh | 25 ++++++++++---- src/tgbaalgos/gtec/ce.cc | 4 +-- src/tgbaalgos/gv04.cc | 2 +- src/tgbaalgos/ndfs_result.hxx | 17 ++++++---- src/tgbatest/randtgba.cc | 58 ++++++++++++++++++++++++-------- 6 files changed, 85 insertions(+), 29 deletions(-) diff --git a/ChangeLog b/ChangeLog index 3b1d9e6e6..137618740 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2005-01-24 Alexandre Duret-Lutz + + * src/tgbaalgos/emptiness_stats.hh (ars_statistics): Distinguish + states visited to compute the prefix and those for the cycle. + * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, + src/tgbaalgos/gtec/ce.cc: Adjust. + * src/tgbatest/randtgba.cc: Print both statistics. + 2005-01-24 Denis Poitrenaud * src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add options diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh index f555191fb..23b85e1e3 100644 --- a/src/tgbaalgos/emptiness_stats.hh +++ b/src/tgbaalgos/emptiness_stats.hh @@ -125,24 +125,37 @@ namespace spot { public: ars_statistics() - : states_(0) + : prefix_states_(0), cycle_states_(0) { } void - inc_ars_states() + inc_ars_prefix_states() { - ++states_; + ++prefix_states_; } int - ars_states() const + ars_prefix_states() const { - return states_; + return prefix_states_; + } + + void + inc_ars_cycle_states() + { + ++cycle_states_; + } + + int + ars_cycle_states() const + { + return cycle_states_; } private: - unsigned states_; /// number of states visited + unsigned prefix_states_; /// states visited to construct the prefix + unsigned cycle_states_; /// states visited to construct the cycle }; /// @} diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index e16b37852..f293318f3 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -48,7 +48,7 @@ namespace spot const state* filter(const state* s) { - r->inc_ars_states(); + r->inc_ars_prefix_states(); numbered_state_heap::state_index_p sip = ecs->h->find(s); // Ignore unknown states ... if (!sip.first) @@ -180,7 +180,7 @@ namespace spot virtual const state* filter(const state* s) { - r->inc_ars_states(); + r->inc_ars_cycle_states(); numbered_state_heap::state_index_p sip = ecs->h->find(s); // Ignore unknown states. if (!sip.first) diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index b3fcc0f75..cdcad1dbe 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -339,7 +339,7 @@ namespace spot virtual const state* filter(const state* s) { - r->inc_ars_states(); + r->inc_ars_cycle_states(); // Do not escape the SCC hash_type::const_iterator j = data.h.find(s); if (// This state was never visited so far. diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 6cfd74a70..0a0b814dd 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -272,7 +272,7 @@ namespace spot if (!f.it->done()) { const state *s_prime = f.it->current_state(); - inc_ars_states(); + inc_ars_cycle_states(); ndfsr_trace << " Visit the successor: " << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); @@ -398,7 +398,7 @@ namespace spot const state* filter(const state* s) { - ars->inc_ars_states(); + ars->inc_ars_cycle_states(); if (!h.has_been_visited(s) || seen.find(s) != seen.end() || dead.find(s) != dead.end()) @@ -459,6 +459,7 @@ namespace spot typedef Sgi::hash_multimap m_source_trans; + template class min_path: public bfs_steps { public: @@ -490,7 +491,11 @@ namespace spot const state* filter(const state* s) { - ars->inc_ars_states(); + if (cycle) + ars->inc_ars_cycle_states(); + else + ars->inc_ars_prefix_states(); + ndfsr_trace << "filter: " << a_->format_state(s); if (!h.has_been_visited(s) || seen.find(s) != seen.end()) { @@ -568,7 +573,7 @@ namespace spot typename m_source_trans::iterator i = target.find(current.dest); if (i == target.end()) { - min_path s(this, a_, target, h_); + min_path s(this, a_, target, h_); const state* res = s.search(current.dest->clone(), run->cycle); // init current to the corresponding transition. assert(res); @@ -598,7 +603,7 @@ namespace spot << a_->format_state(begin) << std::endl; transition tmp; target.insert(std::make_pair(begin, tmp)); - min_path s(this, a_, target, h_); + min_path s(this, a_, target, h_); const state* res = s.search(current.dest->clone(), run->cycle); assert(res); assert(res->compare(begin) == 0); @@ -633,7 +638,7 @@ namespace spot else { // This initial state is outside the cycle. Compute the prefix. - min_path s(this, a_, target, h_); + min_path s(this, a_, target, h_); cycle_entry_point = s.search(prefix_start, run->prefix); assert(cycle_entry_point); cycle_entry_point = cycle_entry_point->clone(); diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 807eff267..f97a18fcd 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -336,9 +336,12 @@ struct acss_stat struct ars_stat { - int min_states; - int max_states; - int tot_states; + int min_prefix_states; + int max_prefix_states; + int tot_prefix_states; + int min_cycle_states; + int max_cycle_states; + int tot_cycle_states; int n; ars_stat() @@ -349,21 +352,25 @@ struct ars_stat void count(const spot::ars_statistics* acss) { - int s = acss->ars_states(); + int p = acss->ars_prefix_states(); + int c = acss->ars_cycle_states(); if (n++) { - min_states = std::min(min_states, s); - max_states = std::max(max_states, s); - tot_states += s; + min_prefix_states = std::min(min_prefix_states, p); + max_prefix_states = std::max(max_prefix_states, p); + tot_prefix_states += p; + min_cycle_states = std::min(min_cycle_states, c); + max_cycle_states = std::max(max_cycle_states, c); + tot_cycle_states += c; } else { - min_states = max_states = tot_states = s; + min_prefix_states = max_prefix_states = tot_prefix_states = p; + min_cycle_states = max_cycle_states = tot_cycle_states = c; } } }; - struct ar_stat { int min_prefix; @@ -1259,7 +1266,7 @@ main(int argc, char** argv) std::cout << "Statistics about accepting run computation:" << std::endl; std::cout << std::setw(22) << "" - << " | (non unique) states |" + << " |(non unique) states for prefix |" << std::endl << std::setw(22) << "algorithm" << " | min < mean < max | total | n" << std::endl @@ -1268,14 +1275,37 @@ main(int argc, char** argv) for (ars_stats_type::const_iterator i = ars_stats.begin(); i != ars_stats.end(); ++i) std::cout << std::setw(22) << i->first << " |" - << std::setw(6) << i->second.min_states + << std::setw(6) << i->second.min_prefix_states << " " << std::setw(8) - << static_cast(i->second.tot_states) / i->second.n + << (static_cast(i->second.tot_prefix_states) + / i->second.n) << " " - << std::setw(6) << i->second.max_states + << std::setw(6) << i->second.max_prefix_states << " |" - << std::setw(6) << i->second.tot_states + << std::setw(6) << i->second.tot_prefix_states + << " |" + << std::setw(4) << i->second.n + << std::endl; + std::cout << std::setw(22) << "" + << " | (non unique) states for cycle |" + << std::endl << std::setw(22) << "algorithm" + << " | min < mean < max | total | n" + << std::endl + << std::setw(61) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + for (ars_stats_type::const_iterator i = ars_stats.begin(); + i != ars_stats.end(); ++i) + std::cout << std::setw(22) << i->first << " |" + << std::setw(6) << i->second.min_cycle_states + << " " + << std::setw(8) + << (static_cast(i->second.tot_cycle_states) + / i->second.n) + << " " + << std::setw(6) << i->second.max_cycle_states + << " |" + << std::setw(6) << i->second.tot_cycle_states << " |" << std::setw(4) << i->second.n << std::endl;