diff --git a/ChangeLog b/ChangeLog index 966eaf68a..fcac0ef1b 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,12 @@ 2005-01-03 Alexandre Duret-Lutz + * src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class. + * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh + (couvreur99_check_result): Inherit from acss_statistics. + (couvreur99_check_result::acss_states): Implement it. + * src/tgbatest/randtgba.cc: Display statistics about accepting cycle + search space. + * src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call erase() after splice(), splice() already removes the elements. diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh index b8c3dfa79..dec68dcd0 100644 --- a/src/tgbaalgos/emptiness_stats.hh +++ b/src/tgbaalgos/emptiness_stats.hh @@ -33,42 +33,58 @@ namespace spot public : ec_statistics() : states_(0), transitions_(0), depth_(0), max_depth_(0) - { - } - void set_states(int n) - { - states_ = n; - } - void inc_states() - { - ++states_; - } - void inc_transitions() - { - ++transitions_; - } - void inc_depth() - { - ++depth_; - if (depth_ > max_depth_) - max_depth_ = depth_; - } - void dec_depth() - { - --depth_; - } - int states() const - { - return states_; - } - int transitions() const - { - return transitions_; - } - int max_depth() const - { - return max_depth_; - } + { + } + + void + set_states(int n) + { + states_ = n; + } + + void + inc_states() + { + ++states_; + } + + void + inc_transitions() + { + ++transitions_; + } + + void + inc_depth() + { + ++depth_; + if (depth_ > max_depth_) + max_depth_ = depth_; + } + + void + dec_depth() + { + --depth_; + } + + int + states() const + { + return states_; + } + + int + transitions() const + { + return transitions_; + } + + int + max_depth() const + { + return max_depth_; + } private : unsigned states_; /// number of disctint visited states @@ -77,6 +93,13 @@ namespace spot unsigned max_depth_; /// maximal depth of the stack(s) }; + /// Accepting Cycle Search Space statistics + class acss_statistics + { + public: + virtual int acss_states() const = 0; + }; + /// @} } diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 36749ac46..862e3def2 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -78,6 +78,19 @@ namespace spot { } + int + couvreur99_check_result::acss_states() const + { + int count = 0; + int scc_root = ecs_->root.s.top().index; + + numbered_state_heap_const_iterator* i = ecs_->h->iterator(); + for (i->first(); !i->done(); i->next()) + if (i->get_index() >= scc_root) + ++count; + return count; + } + tgba_run* couvreur99_check_result::accepting_run() { diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index 30e612811..7bd0ca45a 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -24,11 +24,14 @@ #include "status.hh" #include "tgbaalgos/emptiness.hh" +#include "tgbaalgos/emptiness_stats.hh" namespace spot { /// Compute a counter example from a spot::couvreur99_check_status - class couvreur99_check_result: public emptiness_check_result + class couvreur99_check_result: + public emptiness_check_result, + public acss_statistics { public: couvreur99_check_result(const couvreur99_check_status* ecs); @@ -37,6 +40,8 @@ namespace spot void print_stats(std::ostream& os) const; + virtual int acss_states() const; + protected: /// Called by accepting_run() to find a cycle which traverses all /// acceptance conditions in the accepted SCC. diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 8a398d8a4..0a58d747c 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -223,6 +223,35 @@ struct ec_stat } }; +struct acss_stat +{ + int min_states; + int max_states; + int tot_states; + int n; + + acss_stat() + : n(0) + { + } + + void + count(const spot::acss_statistics* acss) + { + int s = acss->acss_states(); + if (n++) + { + min_states = std::min(min_states, s); + max_states = std::max(max_states, s); + tot_states += s; + } + else + { + min_states = max_states = tot_states = s; + } + } +}; + struct ar_stat { int min_prefix; @@ -268,6 +297,9 @@ struct ar_stat typedef std::map ec_stats_type; ec_stats_type ec_stats; +typedef std::map acss_stats_type; +acss_stats_type acss_stats; + typedef std::map ar_stats_type; ar_stats_type ar_stats; // Statistics about accepting runs. ar_stats_type mar_stats; // ... about minimized accepting runs. @@ -282,7 +314,7 @@ print_ar_stats(ar_stats_type& ar_stats) << " | prefix | cycle |" << std::endl << std::setw(22) << "algorithm" - << " | min < mean < max | min < mean < max | n " + << " | min < mean < max | min < mean < max | n" << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl; @@ -311,7 +343,7 @@ print_ar_stats(ar_stats_type& ar_stats) << " | runs | total |" << std::endl << std::setw(22) << "algorithm" - << " | min < mean < max | pre. cyc. runs | n " + << " | min < mean < max | pre. cyc. runs | n" << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl; @@ -540,13 +572,17 @@ main(int argc, char** argv) } tm_ec.stop(algo); const spot::ec_statistics* ecs = - dynamic_cast(ec); + dynamic_cast(ec); if (opt_z && ecs) ec_stats[algo].count(ecs); if (res) { std::cout << "acc. run"; ++n_non_empty; + const spot::acss_statistics* acss = + dynamic_cast(res); + if (opt_z && acss) + acss_stats[algo].count(acss); if (opt_replay) { spot::tgba_run* run; @@ -658,6 +694,7 @@ main(int argc, char** argv) if (!ec_stats.empty()) { + std::cout << std::endl; std::ios::fmtflags old = std::cout.flags(); std::cout << std::right << std::fixed << std::setprecision(1); @@ -665,12 +702,12 @@ main(int argc, char** argv) std::cout << std::setw(22) << "" << " | states | transitions |" << std::endl << std::setw(22) << "algorithm" - << " | min < mean < max | min < mean < max | n " + << " | min < mean < max | min < mean < max | n" << std::endl << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') << std::endl; for (ec_stats_type::const_iterator i = ec_stats.begin(); - i != ec_stats.end(); ++i) + i != ec_stats.end(); ++i) std::cout << std::setw(22) << i->first << " |" << std::setw(6) << i->second.min_states << " " @@ -694,12 +731,12 @@ main(int argc, char** argv) << " | maximal depth |" << std::endl << std::setw(22) << "algorithm" - << " | min < mean < max | n " + << " | min < mean < max | n" << std::endl - << std::setw(59) << std::setfill('-') << "" << std::setfill(' ') + << std::setw(53) << std::setfill('-') << "" << std::setfill(' ') << std::endl; for (ec_stats_type::const_iterator i = ec_stats.begin(); - i != ec_stats.end(); ++i) + i != ec_stats.end(); ++i) std::cout << std::setw(22) << i->first << " |" << std::setw(6) << i->second.min_max_depth @@ -716,6 +753,38 @@ main(int argc, char** argv) std::cout << std::setiosflags(old); } + if (!acss_stats.empty()) + { + std::cout << std::endl; + std::ios::fmtflags old = std::cout.flags(); + std::cout << std::right << std::fixed << std::setprecision(1); + + std::cout << "Statistics about accepting cycle search space:" + << std::endl; + std::cout << std::setw(22) << "" + << " | states |" + << std::endl << std::setw(22) << "algorithm" + << " | min < mean < max | total | n" + << std::endl + << std::setw(61) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + for (acss_stats_type::const_iterator i = acss_stats.begin(); + i != acss_stats.end(); ++i) + std::cout << std::setw(22) << i->first << " |" + << std::setw(6) << i->second.min_states + << " " + << std::setw(8) + << static_cast(i->second.tot_states) / i->second.n + << " " + << std::setw(6) << i->second.max_states + << " |" + << std::setw(6) << i->second.tot_states + << " |" + << std::setw(4) << i->second.n + << std::endl; + std::cout << std::setiosflags(old); + } + if (!ar_stats.empty()) { std::cout << std::endl