From a5e9fb9df4fb1c6a705b8e10b7e8b265576f48b4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 4 Feb 2005 17:47:05 +0000 Subject: [PATCH] * src/tgbatest/randtgba.cc (stat_collector): New class, replacing... (ec_stat, acss_stat, ars_stat, print_ec_stats, print_acss_stats, print_ars_stats): ... these. * tgbaalgos/emptiness_stats.hh (unsigned_statistics): Make the map public. --- ChangeLog | 6 + src/tgbaalgos/emptiness_stats.hh | 40 ++-- src/tgbatest/randtgba.cc | 391 +++++++++---------------------- 3 files changed, 131 insertions(+), 306 deletions(-) diff --git a/ChangeLog b/ChangeLog index 7f215dfe9..feb2c84c2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,11 @@ 2005-02-04 Alexandre Duret-Lutz + * src/tgbatest/randtgba.cc (stat_collector): New class, replacing... + (ec_stat, acss_stat, ars_stat, print_ec_stats, print_acss_stats, + print_ars_stats): ... these. + * tgbaalgos/emptiness_stats.hh (unsigned_statistics): Make the + map public. + * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics::stats_map_): Use char_ptr_less_than. diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh index 5fe9f9b8a..d5464fc9f 100644 --- a/src/tgbaalgos/emptiness_stats.hh +++ b/src/tgbaalgos/emptiness_stats.hh @@ -32,10 +32,8 @@ namespace spot /// \addtogroup emptiness_check_stats /// @{ - class unsigned_statistics + struct unsigned_statistics { - public: - virtual ~unsigned_statistics() { @@ -44,16 +42,14 @@ namespace spot unsigned get(const char* str) const { - stats_map_::const_iterator i = stats_.find(str); - assert(i != stats_.end()); + stats_map::const_iterator i = stats.find(str); + assert(i != stats.end()); return (this->*i->second)(); } - protected: - typedef unsigned (unsigned_statistics::*unsigned_fun_)() const; - typedef std::map stats_map_; - stats_map_ stats_; + typedef unsigned (unsigned_statistics::*unsigned_fun)() const; + typedef std::map stats_map; + stats_map stats; }; /// \brief Emptiness-check statistics @@ -67,13 +63,13 @@ namespace spot ec_statistics() : states_(0), transitions_(0), depth_(0), max_depth_(0) { - stats_["states"] = - static_cast(&ec_statistics::states); - stats_["transitions"] = - static_cast + stats["states"] = + static_cast(&ec_statistics::states); + stats["transitions"] = + static_cast (&ec_statistics::transitions); - stats_["max. depth"] = - static_cast + stats["max. depth"] = + static_cast (&ec_statistics::max_depth); } @@ -152,11 +148,11 @@ namespace spot ars_statistics() : prefix_states_(0), cycle_states_(0) { - stats_["(non unique) states for prefix"] = - static_cast + stats["(non unique) states for prefix"] = + static_cast (&ars_statistics::ars_prefix_states); - stats_["(non unique) states for cycle"] = - static_cast + stats["(non unique) states for cycle"] = + static_cast (&ars_statistics::ars_cycle_states); } @@ -199,8 +195,8 @@ namespace spot public: acss_statistics() { - stats_["search space states"] = - static_cast + stats["search space states"] = + static_cast (&acss_statistics::acss_states); } diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 81ef19e9c..5012c05fc 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -281,52 +281,95 @@ to_float_nonneg(const char* s, const char* arg) return res; } -struct ec_stat +struct stat_collector { - int max_tgba_states; - int tot_tgba_states; - int min_states; - int max_states; - int tot_states; - int min_transitions; - int max_transitions; - int tot_transitions; - int min_max_depth; - int max_max_depth; - int tot_max_depth; - int n; - - ec_stat() - : n(0) + struct one_stat { + unsigned min; + unsigned max; + unsigned tot; + unsigned n; + + one_stat() + : n(0) + { + } + + void + count(unsigned val) + { + if (n++) + { + min = std::min(min, val); + max = std::max(max, val); + tot += val; + } + else + { + max = min = tot = val; + } + } + }; + + typedef std::map alg_1stat_map; + typedef std::map stats_alg_map; + stats_alg_map stats; + + bool + empty() + { + return stats.empty(); } void - count(const spot::unsigned_statistics* ec) + count(const std::string& algorithm, const spot::unsigned_statistics* s) { - int s = ec->get("states"); - int t = ec->get("transitions"); - int m = ec->get("max. depth"); - - if (n++) - { - min_states = std::min(min_states, s); - max_states = std::max(max_states, s); - tot_states += s; - min_transitions = std::min(min_transitions, t); - max_transitions = std::max(max_transitions, t); - tot_transitions += t; - min_max_depth = std::min(min_max_depth, m); - max_max_depth = std::max(max_max_depth, m); - tot_max_depth += m; - } - else - { - min_states = max_states = tot_states = s; - min_transitions = max_transitions = tot_transitions = t; - min_max_depth = max_max_depth = tot_max_depth = m; - } + if (!s) + return; + spot::unsigned_statistics::stats_map::const_iterator i; + for (i = s->stats.begin(); i != s->stats.end(); ++i) + stats[i->first][algorithm].count((s->*i->second)()); } + + std::ostream& + display(std::ostream& os, + const alg_1stat_map& m, const std::string title) const + { + os << std::setw(22) << "" << " | " + << std::setw(30) << std::left << title << std::right << "|" << std::endl + << std::setw(22) << "algorithm" + << " | min < mean < max | total | n" + << std::endl + << std::setw(61) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + for (alg_1stat_map::const_iterator i = m.begin(); i != m.end(); ++i) + os << std::setw(22) << i->first << " |" + << std::setw(6) << i->second.min + << " " + << std::setw(8) + << static_cast(i->second.tot) / i->second.n + << " " + << std::setw(6) << i->second.max + << " |" + << std::setw(6) << i->second.tot + << " |" + << std::setw(4) << i->second.n + << std::endl; + os << std::setw(61) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + return os; + } + + std::ostream& + display(std::ostream& os) const + { + stats_alg_map::const_iterator i; + for (i = stats.begin(); i != stats.end(); ++i) + display(os, i->second, i->first); + return os; + } + + }; struct ec_ratio_stat @@ -379,35 +422,6 @@ struct ec_ratio_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 acss_ratio_stat { float min_states; @@ -438,43 +452,6 @@ struct acss_ratio_stat } }; -struct ars_stat -{ - 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() - : n(0) - { - } - - void - count(const spot::ars_statistics* acss) - { - int p = acss->ars_prefix_states(); - int c = acss->ars_cycle_states(); - if (n++) - { - 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_prefix_states = max_prefix_states = tot_prefix_states = p; - min_cycle_states = max_cycle_states = tot_cycle_states = c; - } - } -}; - struct ars_ratio_stat { float min_prefix_states; @@ -555,23 +532,17 @@ struct ar_stat } }; -typedef std::map ec_stats_type; -ec_stats_type ec_stats; +stat_collector sc_ec; +stat_collector sc_arc; typedef std::map ec_ratio_stat_type; ec_ratio_stat_type glob_ec_ratio_stats; typedef std::map ec_ratio_stats_type; ec_ratio_stats_type ec_ratio_stats; -typedef std::map acss_stats_type; -acss_stats_type acss_stats; - typedef std::map acss_ratio_stats_type; acss_ratio_stats_type acss_ratio_stats; -typedef std::map ars_stats_type; -ars_stats_type ars_stats; - typedef std::map ars_ratio_stats_type; ars_ratio_stats_type ars_ratio_stats; @@ -579,69 +550,6 @@ typedef std::map ar_stats_type; ar_stats_type ar_stats; // Statistics about accepting runs. ar_stats_type mar_stats; // ... about minimized accepting runs. -void -print_ec_stats(const ec_stats_type& ec_stats, bool opt_paper = false) -{ - std::ios::fmtflags old = std::cout.flags(); - if (!opt_paper) - { - std::cout << std::endl; - std::cout << std::right << std::fixed << std::setprecision(1); - - std::cout << "Statistics about emptiness checkers:" << std::endl; - std::cout << std::setw(22) << "" - << " | states | transitions |" - << std::endl << std::setw(22) << "algorithm" - << " | 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) - 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.min_transitions - << " " - << std::setw(8) - << static_cast(i->second.tot_transitions) / i->second.n - << " " - << std::setw(6) << i->second.max_transitions - << " |" - << std::setw(4) << i->second.n - << std::endl; - std::cout << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') - << std::endl - << std::setw(22) << "" - << " | maximal depth |" - << std::endl - << std::setw(22) << "algorithm" - << " | min < mean < max | n" - << std::endl - << std::setw(53) << std::setfill('-') << "" << std::setfill(' ') - << std::endl; - for (ec_stats_type::const_iterator i = ec_stats.begin(); - i != ec_stats.end(); ++i) - std::cout << std::setw(22) << i->first << " |" - << std::setw(6) - << i->second.min_max_depth - << " " - << std::setw(8) - << static_cast(i->second.tot_max_depth) / i->second.n - << " " - << std::setw(6) - << i->second.max_max_depth - << " |" - << std::setw(4) << i->second.n - << std::endl; - } - std::cout << std::setiosflags(old); -} void print_ar_stats(ar_stats_type& ar_stats, const std::string s, @@ -803,42 +711,6 @@ print_ec_ratio_stats(const std::string& s, std::cout << std::setiosflags(old); } -void -print_acss_stats(const acss_stats_type& acss_stats, bool opt_paper = false) -{ - std::ios::fmtflags old = std::cout.flags(); - if (!opt_paper) - { - std::cout << std::endl; - 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); -} - void print_acss_ratio_stats(const acss_ratio_stats_type& acss_ratio_stats, bool opt_paper = false) @@ -888,65 +760,6 @@ print_acss_ratio_stats(const acss_ratio_stats_type& acss_ratio_stats, std::cout << std::setiosflags(old); } -void -print_ars_stats(const ars_stats_type& ars_stats, bool opt_paper = false) -{ - std::ios::fmtflags old = std::cout.flags(); - if (!opt_paper) - { - std::cout << std::endl; - std::cout << std::right << std::fixed << std::setprecision(1); - - std::cout << "Statistics about accepting run computation:" - << std::endl; - std::cout << std::setw(22) << "" - << " |(non unique) states for prefix |" - << 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_prefix_states - << " " - << std::setw(8) - << (static_cast(i->second.tot_prefix_states) - / i->second.n) - << " " - << std::setw(6) << i->second.max_prefix_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; - } - std::cout << std::setiosflags(old); -} - void print_ars_ratio_stats(const ars_ratio_stats_type& ars_ratio_stats, bool opt_paper = false) @@ -1399,7 +1212,7 @@ main(int argc, char** argv) if (!ec) continue; ++n_ec; - std::string algo = ec_algos[i].name; + const char* algo = ec_algos[i].name; if (!opt_paper) { std::cout.width(32); @@ -1419,7 +1232,7 @@ main(int argc, char** argv) const spot::unsigned_statistics* ecs = ec->statistics(); if (opt_z && ecs) { - ec_stats[algo].count(ecs); + sc_ec.count(algo, ecs); if (res) { // Notice that ratios are computed w.r.t. the @@ -1438,7 +1251,7 @@ main(int argc, char** argv) (res->statistics()); if (opt_z && acss) { - acss_stats[algo].count(acss); + sc_arc.count(algo, acss); acss_ratio_stats[algo].count(acss, a); } if (opt_replay) @@ -1457,7 +1270,7 @@ main(int argc, char** argv) { // Count only the first run (the other way // would be to divide the stats by opt_R). - ars_stats[algo].count(ars); + sc_arc.count(algo, ars); ars_ratio_stats[algo].count(ars, a); ars = 0; } @@ -1511,7 +1324,8 @@ main(int argc, char** argv) } else { - std::cout << ", reduced"; + if (!opt_paper) + std::cout << ", reduced"; if (opt_z) mar_stats[algo].count(redrun); } @@ -1586,8 +1400,23 @@ main(int argc, char** argv) } while (opt_F || opt_i); - if (!ec_stats.empty()) - print_ec_stats(ec_stats, opt_paper); + if (!opt_paper) + { + if (!sc_ec.empty()) + { + std::cout << std::endl + << "Statistics about emptiness checks:" + << std::endl; + sc_ec.display(std::cout); + } + if (!sc_arc.empty()) + { + std::cout << std::endl + << "Statistics about accepting run computations:" + << std::endl; + sc_arc.display(std::cout); + } + } if (!glob_ec_ratio_stats.empty()) { @@ -1602,15 +1431,9 @@ main(int argc, char** argv) } } - if (!acss_stats.empty()) - print_acss_stats(acss_stats, opt_paper); - if (!acss_ratio_stats.empty()) print_acss_ratio_stats(acss_ratio_stats, opt_paper); - if (!ars_stats.empty()) - print_ars_stats(ars_stats, opt_paper); - if (!ars_ratio_stats.empty()) print_ars_ratio_stats(ars_ratio_stats, opt_paper);