From 9c2c3926c7b948b127c9d54dfc85bf95711c44da Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 3 Feb 2005 17:37:11 +0000 Subject: [PATCH] * tgbaalgos/emptiness_stats.hh (unsigned_statistics): New base class for ec_statistics and ars_statistics. (acss_statistics): Inherit from ars_statistics. * tgbaalgos/emptiness.cc, tgbaalgos/emptiness.hh: (emptiness_check::statistics, emptiness_check_result::statistics): New methods. * tgbatest/randtgba.cc: Adjust to use the above. * tgbaalgos/gv04.cc, tgbaalgos/ndfs_result.hxx, tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/ce.hh: Do not inherit from ars_statistics if acss_statistics is used. --- ChangeLog | 11 ++++ src/tgbaalgos/emptiness.cc | 14 ++++- src/tgbaalgos/emptiness.hh | 8 +++ src/tgbaalgos/emptiness_stats.hh | 92 +++++++++++++++++++++++++------- src/tgbaalgos/gtec/ce.cc | 4 +- src/tgbaalgos/gtec/ce.hh | 5 +- src/tgbaalgos/gv04.cc | 5 +- src/tgbaalgos/ndfs_result.hxx | 18 +++---- src/tgbatest/randtgba.cc | 28 +++++----- 9 files changed, 135 insertions(+), 50 deletions(-) diff --git a/ChangeLog b/ChangeLog index bf5b7092f..1a175b010 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,16 @@ 2005-02-03 Alexandre Duret-Lutz + * tgbaalgos/emptiness_stats.hh (unsigned_statistics): New base + class for ec_statistics and ars_statistics. + (acss_statistics): Inherit from ars_statistics. + * tgbaalgos/emptiness.cc, tgbaalgos/emptiness.hh: + (emptiness_check::statistics, emptiness_check_result::statistics): + New methods. + * tgbatest/randtgba.cc: Adjust to use the above. + * tgbaalgos/gv04.cc, tgbaalgos/ndfs_result.hxx, tgbaalgos/gtec/ce.cc, + tgbaalgos/gtec/ce.hh: Do not inherit from ars_statistics if + acss_statistics is used. + * src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Add pseudo code. 2005-02-02 Alexandre Duret-Lutz diff --git a/src/tgbaalgos/emptiness.cc b/src/tgbaalgos/emptiness.cc index 70f9a38c7..71f68a095 100644 --- a/src/tgbaalgos/emptiness.cc +++ b/src/tgbaalgos/emptiness.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. // @@ -100,10 +100,22 @@ namespace spot return 0; } + const unsigned_statistics* + emptiness_check_result::statistics() const + { + return dynamic_cast(this); + } + emptiness_check::~emptiness_check() { } + const unsigned_statistics* + emptiness_check::statistics() const + { + return dynamic_cast(this); + } + std::ostream& emptiness_check::print_stats(std::ostream& os) const { diff --git a/src/tgbaalgos/emptiness.hh b/src/tgbaalgos/emptiness.hh index 5dc4019ed..6d7ca0487 100644 --- a/src/tgbaalgos/emptiness.hh +++ b/src/tgbaalgos/emptiness.hh @@ -26,6 +26,7 @@ #include #include #include "tgba/state.hh" +#include "emptiness_stats.hh" namespace spot { @@ -98,6 +99,10 @@ namespace spot { return a_; } + + /// Return statistics, if available. + virtual const unsigned_statistics* statistics() const; + protected: const tgba* a_; ///< The automaton. }; @@ -131,6 +136,9 @@ namespace spot /// several time, but generally you should not assume that. virtual emptiness_check_result* check() = 0; + /// Return statistics, if available. + virtual const unsigned_statistics* statistics() const; + /// Print statistics, if any. virtual std::ostream& print_stats(std::ostream& os) const; diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh index 185f8c860..78e1468fd 100644 --- a/src/tgbaalgos/emptiness_stats.hh +++ b/src/tgbaalgos/emptiness_stats.hh @@ -23,6 +23,8 @@ # define SPOT_TGBAALGOS_EMPTINESS_STATS_HH #include +#include +#include namespace spot { @@ -30,17 +32,48 @@ namespace spot /// \addtogroup emptiness_check_stats /// @{ + class unsigned_statistics + { + public: + + virtual + ~unsigned_statistics() + { + } + + unsigned + get(const char* str) const + { + 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_; + }; + /// \brief Emptiness-check statistics /// /// Implementations of spot::emptiness_check may also implement /// this interface. Try to dynamic_cast the spot::emptiness_check /// pointer to know whether these statistics are available. - class ec_statistics + class ec_statistics: public unsigned_statistics { public : ec_statistics() : states_(0), transitions_(0), depth_(0), max_depth_(0) { + stats_["states"] = + static_cast(&ec_statistics::states); + stats_["transitions"] = + static_cast + (&ec_statistics::transitions); + stats_["max. depth"] = + static_cast + (&ec_statistics::max_depth); } void @@ -76,25 +109,25 @@ namespace spot depth_ -= n; } - int + unsigned states() const { return states_; } - int + unsigned transitions() const { return transitions_; } - int + unsigned max_depth() const { return max_depth_; } - int + unsigned depth() const { return depth_; @@ -107,29 +140,23 @@ namespace spot unsigned max_depth_; /// maximal depth of the stack(s) }; - /// \brief Accepting Cycle Search Space statistics - /// - /// Implementations of spot::emptiness_check_result may also implement - /// this interface. Try to dynamic_cast the spot::emptiness_check_result - /// pointer to know whether these statistics are available. - class acss_statistics - { - public: - /// Number of states in the search space for the accepting cycle. - virtual int acss_states() const = 0; - }; - /// \brief Accepting Run Search statistics. /// /// Implementations of spot::emptiness_check_result may also implement /// this interface. Try to dynamic_cast the spot::emptiness_check_result /// pointer to know whether these statistics are available. - class ars_statistics + class ars_statistics: public unsigned_statistics { public: ars_statistics() : prefix_states_(0), cycle_states_(0) { + stats_["(non unique) states for prefix"] = + static_cast + (&ars_statistics::ars_prefix_states); + stats_["(non unique) states for cycle"] = + static_cast + (&ars_statistics::ars_cycle_states); } void @@ -138,7 +165,7 @@ namespace spot ++prefix_states_; } - int + unsigned ars_prefix_states() const { return prefix_states_; @@ -150,7 +177,7 @@ namespace spot ++cycle_states_; } - int + unsigned ars_cycle_states() const { return cycle_states_; @@ -161,6 +188,31 @@ namespace spot unsigned cycle_states_; /// states visited to construct the cycle }; + /// \brief Accepting Cycle Search Space statistics + /// + /// Implementations of spot::emptiness_check_result may also implement + /// this interface. Try to dynamic_cast the spot::emptiness_check_result + /// pointer to know whether these statistics are available. + class acss_statistics: public ars_statistics + { + public: + acss_statistics() + { + stats_["search space states"] = + static_cast + (&acss_statistics::acss_states); + } + + virtual + ~acss_statistics() + { + } + + /// Number of states in the search space for the accepting cycle. + virtual unsigned acss_states() const = 0; + }; + + /// @} } diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index c75e3c41d..3bd34ff20 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -82,10 +82,10 @@ namespace spot { } - int + unsigned couvreur99_check_result::acss_states() const { - int count = 0; + unsigned count = 0; int scc_root = ecs_->root.top().index; numbered_state_heap_const_iterator* i = ecs_->h->iterator(); diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index c27971d0d..76102c2c0 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -31,8 +31,7 @@ namespace spot /// Compute a counter example from a spot::couvreur99_check_status class couvreur99_check_result: public emptiness_check_result, - public acss_statistics, - public ars_statistics + public acss_statistics { public: couvreur99_check_result(const couvreur99_check_status* ecs); @@ -41,7 +40,7 @@ namespace spot void print_stats(std::ostream& os) const; - virtual int acss_states() const; + virtual unsigned acss_states() const; protected: /// Called by accepting_run() to find a cycle which traverses all diff --git a/src/tgbaalgos/gv04.cc b/src/tgbaalgos/gv04.cc index 2f0e5e4bb..25f868479 100644 --- a/src/tgbaalgos/gv04.cc +++ b/src/tgbaalgos/gv04.cc @@ -238,8 +238,7 @@ namespace spot struct result: public emptiness_check_result, - public acss_statistics, - public ars_statistics + public acss_statistics { gv04& data; @@ -265,7 +264,7 @@ namespace spot } } - virtual int + virtual unsigned acss_states() const { // Gross! diff --git a/src/tgbaalgos/ndfs_result.hxx b/src/tgbaalgos/ndfs_result.hxx index 9fa0e09a3..86a43f2c6 100644 --- a/src/tgbaalgos/ndfs_result.hxx +++ b/src/tgbaalgos/ndfs_result.hxx @@ -67,15 +67,16 @@ namespace spot // size() method (which we indicate using n==1). template - struct acss_interface + struct stats_interface + : public ars_statistics { }; template - struct acss_interface + struct stats_interface : public acss_statistics { - int + unsigned acss_states() const { // all visited states are in the state space search @@ -89,9 +90,8 @@ namespace spot template class ndfs_result: public emptiness_check_result, - public ars_statistics, - // Conditionally inherit from acss_statistics. - public acss_interface, heap::Has_Size> + // Conditionally inherit from acss_statistics or ars_statistics. + public stats_interface, heap::Has_Size> { public: ndfs_result(const ndfs_search& ms) @@ -216,7 +216,7 @@ namespace spot const ndfs_search& ms_; const heap& h_; template - friend struct acss_interface; + friend struct stats_interface; struct transition { const state* source; @@ -286,7 +286,7 @@ namespace spot } else if (seen.find(s_prime) == seen.end()) { - inc_ars_cycle_states(); + this->inc_ars_cycle_states(); ndfsr_trace << " it is not seen, go down" << std::endl; seen.insert(s_prime); tgba_succ_iterator* i = a_->succ_iter(s_prime); @@ -295,7 +295,7 @@ namespace spot } else if ((acc & covered_acc) != acc) { - inc_ars_cycle_states(); + this->inc_ars_cycle_states(); ndfsr_trace << " a propagation is needed, " << "start a search" << std::endl; if (search(s_prime, target, dead)) diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 4d1118158..81ef19e9c 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -302,11 +302,11 @@ struct ec_stat } void - count(const spot::ec_statistics* ec) + count(const spot::unsigned_statistics* ec) { - int s = ec->states(); - int t = ec->transitions(); - int m = ec->max_depth(); + int s = ec->get("states"); + int t = ec->get("transitions"); + int m = ec->get("max. depth"); if (n++) { @@ -348,12 +348,15 @@ struct ec_ratio_stat } void - count(const spot::ec_statistics* ec, const spot::tgba* a) + count(const spot::unsigned_statistics* ec, const spot::tgba* a) { spot::tgba_statistics a_size = spot::stats_reachable(a); - float ms = ec->states() / static_cast(a_size.states); - float mt = ec->transitions() / static_cast(a_size.transitions); - float mm = ec->max_depth() / static_cast(a_size.states); + int s = ec->get("states"); + int t = ec->get("transitions"); + int m = ec->get("max. depth"); + float ms = s / static_cast(a_size.states); + float mt = t / static_cast(a_size.transitions); + float mm = m / static_cast(a_size.states); if (n++) { @@ -1413,8 +1416,7 @@ main(int argc, char** argv) ec = cons_emptiness_check(i, a, degen, real_n_acc); } tm_ec.stop(algo); - const spot::ec_statistics* ecs = - dynamic_cast(ec); + const spot::unsigned_statistics* ecs = ec->statistics(); if (opt_z && ecs) { ec_stats[algo].count(ecs); @@ -1432,7 +1434,8 @@ main(int argc, char** argv) std::cout << "acc. run"; ++n_non_empty; const spot::acss_statistics* acss = - dynamic_cast(res); + dynamic_cast + (res->statistics()); if (opt_z && acss) { acss_stats[algo].count(acss); @@ -1443,7 +1446,8 @@ main(int argc, char** argv) spot::tgba_run* run; const spot::ars_statistics* ars = - dynamic_cast(res); + dynamic_cast + (res->statistics()); tm_ar.start(algo); for (int count = opt_R;;)