From 55c08790fd38d4b13d082d83d8b80af54f8c279c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 3 Jan 2005 15:49:50 +0000 Subject: [PATCH] * src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class. * src/tgbaalgos/ndfs_result.hh (ndfs_result): Inherit from ars_statistics. (ndfs_result::dfs): Call inc_ars_states(). (ndfs_result::test_path, ndfs_result::min_path): Update ars_statistics. * tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit from ars_statistics. * tgbaalgos/gtec/ce.cc (shortest_path, couvreur99_check_result::accepting_cycle::scc_bfs): Update ars_statistics. * src/tgbatest/randtgba.cc: Display statistics about accepting run search. --- ChangeLog | 13 ++ src/tgbaalgos/emptiness_stats.hh | 35 ++++- src/tgbaalgos/gtec/ce.cc | 20 ++- src/tgbaalgos/gtec/ce.hh | 3 +- src/tgbaalgos/ndfs_result.hh | 225 ++++++++++++++++--------------- src/tgbatest/randtgba.cc | 74 ++++++++++ 6 files changed, 249 insertions(+), 121 deletions(-) diff --git a/ChangeLog b/ChangeLog index 0a0e81e35..cdbe6b750 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,18 @@ 2005-01-03 Alexandre Duret-Lutz + * src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class. + * src/tgbaalgos/ndfs_result.hh (ndfs_result): Inherit from + ars_statistics. + (ndfs_result::dfs): Call inc_ars_states(). + (ndfs_result::test_path, ndfs_result::min_path): Update ars_statistics. + * tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit + from ars_statistics. + * tgbaalgos/gtec/ce.cc (shortest_path, + couvreur99_check_result::accepting_cycle::scc_bfs): + Update ars_statistics. + * src/tgbatest/randtgba.cc: Display statistics about accepting run + search. + * src/tgbaalgos/bfssteps.hh (bfs_steps::finalize): Document. * src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class. diff --git a/src/tgbaalgos/emptiness_stats.hh b/src/tgbaalgos/emptiness_stats.hh index dec68dcd0..5b3ec5953 100644 --- a/src/tgbaalgos/emptiness_stats.hh +++ b/src/tgbaalgos/emptiness_stats.hh @@ -28,6 +28,7 @@ namespace spot /// \addtogroup ec_misc /// @{ + /// Emptiness-check statistics class ec_statistics { public : @@ -87,19 +88,45 @@ namespace spot } private : - unsigned states_; /// number of disctint visited states - unsigned transitions_; /// number of visited transitions - unsigned depth_; /// maximal depth of the stack(s) - unsigned max_depth_; /// maximal depth of the stack(s) + unsigned states_; /// number of disctint visited states + unsigned transitions_; /// number of visited transitions + unsigned depth_; /// maximal depth of the stack(s) + unsigned max_depth_; /// maximal depth of the stack(s) }; /// Accepting Cycle Search Space statistics class acss_statistics { public: + /// Number of states in the search space for the accepting cycle. virtual int acss_states() const = 0; }; + /// Accepting Run Search statistics. + class ars_statistics + { + public: + ars_statistics() + : states_(0) + { + } + + void + inc_ars_states() + { + ++states_; + } + + int + ars_states() const + { + return states_; + } + + private: + unsigned states_; /// number of states visited + }; + /// @} } diff --git a/src/tgbaalgos/gtec/ce.cc b/src/tgbaalgos/gtec/ce.cc index 862e3def2..e16b37852 100644 --- a/src/tgbaalgos/gtec/ce.cc +++ b/src/tgbaalgos/gtec/ce.cc @@ -32,8 +32,10 @@ namespace spot class shortest_path: public bfs_steps { public: - shortest_path(const state_set* t, const couvreur99_check_status* ecs) - : bfs_steps(ecs->aut), target(t), ecs(ecs) + shortest_path(const state_set* t, + const couvreur99_check_status* ecs, + couvreur99_check_result* r) + : bfs_steps(ecs->aut), target(t), ecs(ecs), r(r) { } @@ -46,6 +48,7 @@ namespace spot const state* filter(const state* s) { + r->inc_ars_states(); numbered_state_heap::state_index_p sip = ecs->h->find(s); // Ignore unknown states ... if (!sip.first) @@ -69,6 +72,7 @@ namespace spot state_set seen; const state_set* target; const couvreur99_check_status* ecs; + couvreur99_check_result* r; }; } @@ -109,7 +113,7 @@ namespace spot for (tgba_run::steps::const_iterator i = run_->cycle.begin(); i != run_->cycle.end(); ++i) ss.insert(i->s); - shortest_path shpath(&ss, ecs_); + shortest_path shpath(&ss, ecs_, this); const state* prefix_start = ecs_->aut->get_init_state(); // There are two cases: either the initial state is already on @@ -161,11 +165,14 @@ namespace spot struct scc_bfs: bfs_steps { const couvreur99_check_status* ecs; + couvreur99_check_result* r; bdd& acc_to_traverse; int scc_root; + scc_bfs(const couvreur99_check_status* ecs, - bdd& acc_to_traverse) - : bfs_steps(ecs->aut), ecs(ecs), acc_to_traverse(acc_to_traverse), + couvreur99_check_result* r, bdd& acc_to_traverse) + : bfs_steps(ecs->aut), ecs(ecs), r(r), + acc_to_traverse(acc_to_traverse), scc_root(ecs->root.s.top().index) { } @@ -173,6 +180,7 @@ namespace spot virtual const state* filter(const state* s) { + r->inc_ars_states(); numbered_state_heap::state_index_p sip = ecs->h->find(s); // Ignore unknown states. if (!sip.first) @@ -200,7 +208,7 @@ namespace spot return false; } - } b(ecs_, acc_to_traverse); + } b(ecs_, this, acc_to_traverse); substart = b.search(substart, run_->cycle); } diff --git a/src/tgbaalgos/gtec/ce.hh b/src/tgbaalgos/gtec/ce.hh index 7bd0ca45a..c27971d0d 100644 --- a/src/tgbaalgos/gtec/ce.hh +++ b/src/tgbaalgos/gtec/ce.hh @@ -31,7 +31,8 @@ namespace spot /// Compute a counter example from a spot::couvreur99_check_status class couvreur99_check_result: public emptiness_check_result, - public acss_statistics + public acss_statistics, + public ars_statistics { public: couvreur99_check_result(const couvreur99_check_status* ecs); diff --git a/src/tgbaalgos/ndfs_result.hh b/src/tgbaalgos/ndfs_result.hh index 7de92a234..e8519df4b 100644 --- a/src/tgbaalgos/ndfs_result.hh +++ b/src/tgbaalgos/ndfs_result.hh @@ -62,129 +62,127 @@ namespace spot typedef std::list stack_type; template - class ndfs_result : public emptiness_check_result + class ndfs_result: + public emptiness_check_result, + public ars_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()) + { + } virtual ~ndfs_result() - { - } + { + } virtual tgba_run* accepting_run() - { - const stack_type& stb = ms_.get_st_blue(); - const stack_type& str = ms_.get_st_red(); + { + const stack_type& stb = ms_.get_st_blue(); + const stack_type& str = ms_.get_st_red(); - assert(!stb.empty()); + assert(!stb.empty()); - bdd covered_acc = bddfalse; - accepting_transitions_list acc_trans; + bdd covered_acc = bddfalse; + accepting_transitions_list acc_trans; - const state* start; + const state* start; - if (str.empty()) - start = stb.front().s->clone(); - else - { - start = str.front().s->clone(); - if (a_->number_of_acceptance_conditions() == 0) - { - // take arbitrarily the last transition on the red stack - stack_type::const_iterator i, j; - i = j = str.begin(); ++i; - if (i == str.end()) - i = stb.begin(); - transition t = { i->s->clone(), j->label, j->acc, - j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); - acc_trans.push_back(t); - } - else - { - // ignore the prefix - stack_type::const_reverse_iterator i, j; + start = stb.front().s->clone(); + if (!str.empty()) + { + if (a_->number_of_acceptance_conditions() == 0) + { + // take arbitrarily the last transition on the red stack + stack_type::const_iterator i, j; + i = j = str.begin(); ++i; + if (i == str.end()) + i = stb.begin(); + transition t = { i->s->clone(), j->label, j->acc, + j->s->clone() }; + assert(h_.has_been_visited(t.source)); + assert(h_.has_been_visited(t.dest)); + acc_trans.push_back(t); + } + else + { + // ignore the prefix + stack_type::const_reverse_iterator i, j; - i = j = stb.rbegin(); ++j; - for (; i->s->compare(start) != 0; ++i, ++j) - { - } + i = j = stb.rbegin(); ++j; + while (i->s->compare(start) != 0) + ++i, ++j; + stack_type::const_reverse_iterator end = stb.rend(); + for (; j != end; ++i, ++j) + { + if ((covered_acc & j->acc) != j->acc) + { + transition t = { i->s->clone(), j->label, j->acc, + j->s->clone() }; + assert(h_.has_been_visited(t.source)); + assert(h_.has_been_visited(t.dest)); + acc_trans.push_back(t); + covered_acc |= j->acc; + } + } - stack_type::const_reverse_iterator end = stb.rend(); - for (; j != end; ++i, ++j) - { - if ((covered_acc & j->acc) != j->acc) - { - transition t = { i->s->clone(), j->label, j->acc, - j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); - acc_trans.push_back(t); - covered_acc |= j->acc; - } - } + j = str.rbegin(); + if ((covered_acc & j->acc) != j->acc) + { + transition t = { i->s->clone(), j->label, j->acc, + j->s->clone() }; + assert(h_.has_been_visited(t.source)); + assert(h_.has_been_visited(t.dest)); + acc_trans.push_back(t); + covered_acc |= j->acc; + } - j = str.rbegin(); - if ((covered_acc & j->acc) != j->acc) - { - transition t = { i->s->clone(), j->label, j->acc, - j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); - acc_trans.push_back(t); - covered_acc |= j->acc; - } + i = j; ++j; + end = str.rend(); + for (; j != end; ++i, ++j) + { + if ((covered_acc & j->acc) != j->acc) + { + transition t = { i->s->clone(), j->label, j->acc, + j->s->clone() }; + assert(h_.has_been_visited(t.source)); + assert(h_.has_been_visited(t.dest)); + acc_trans.push_back(t); + covered_acc |= j->acc; + } + } + } + } - i = j; ++j; - end = str.rend(); - for (; j != end; ++i, ++j) - { - if ((covered_acc & j->acc) != j->acc) - { - transition t = { i->s->clone(), j->label, j->acc, - j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); - acc_trans.push_back(t); - covered_acc |= j->acc; - } - } - } - } + if (a_->all_acceptance_conditions() != covered_acc) + { + bool b = dfs(start, acc_trans, covered_acc); + assert(b); + (void) b; + } - if (a_->all_acceptance_conditions() != covered_acc) - { - bool b = dfs(start, acc_trans, covered_acc); - assert(b); - (void) b; - } + delete start; - delete start; + assert(!acc_trans.empty()); - assert(!acc_trans.empty()); + tgba_run* run = new tgba_run; + // construct run->cycle from acc_trans. + construct_cycle(run, acc_trans); + // construct run->prefix (a minimal path from the initial state to any + // state of run->cycle) and adjust the cycle to the state reached by the + // prefix. + construct_prefix(run); - tgba_run* run = new tgba_run; - // construct run->cycle from acc_trans. - construct_cycle(run, acc_trans); - // construct run->prefix (a minimal path from the initial state to any - // state of run->cycle) and adjust the cycle to the state reached by the - // prefix. - construct_prefix(run); + for (typename accepting_transitions_list::const_iterator i = + acc_trans.begin(); i != acc_trans.end(); ++i) + { + delete i->source; + delete i->dest; + } - for (typename accepting_transitions_list::const_iterator i = - acc_trans.begin(); i != acc_trans.end(); ++i) - { - delete i->source; - delete i->dest; - } - - return run; - } + return run; + } private: const ndfs_search& ms_; @@ -244,6 +242,7 @@ namespace spot if (!f.it->done()) { const state *s_prime = f.it->current_state(); + inc_ars_states(); ndfsr_trace << " Visit the successor: " << a_->format_state(s_prime) << std::endl; bdd label = f.it->current_condition(); @@ -340,9 +339,10 @@ namespace spot class test_path: public bfs_steps { public: - test_path(const tgba* a, const state* t, + test_path(ars_statistics* ars, + const tgba* a, const state* t, const state_set& d, const heap& h) - : bfs_steps(a), target(t), dead(d), h(h) + : bfs_steps(a), ars(ars), target(t), dead(d), h(h) { } @@ -368,6 +368,7 @@ namespace spot const state* filter(const state* s) { + ars->inc_ars_states(); if (!h.has_been_visited(s) || seen.find(s) != seen.end() || dead.find(s) != dead.end()) @@ -396,6 +397,7 @@ namespace spot } private: + ars_statistics* ars; state_set seen; const state* target; const state_set& dead; @@ -408,7 +410,7 @@ namespace spot if (start->compare(target) == 0) return true; - test_path s(a_, target, dead, h_); + test_path s(this, a_, target, dead, h_); const state* res = s.search(start->clone(), path); if (res) { @@ -430,8 +432,9 @@ namespace spot class min_path: public bfs_steps { public: - min_path(const tgba* a, const m_source_trans& target, const heap& h) - : bfs_steps(a), target(target), h(h) + min_path(ars_statistics* ars, + const tgba* a, const m_source_trans& target, const heap& h) + : bfs_steps(a), ars(ars), target(target), h(h) { } @@ -457,6 +460,7 @@ namespace spot const state* filter(const state* s) { + ars->inc_ars_states(); ndfsr_trace << "filter: " << a_->format_state(s); if (!h.has_been_visited(s) || seen.find(s) != seen.end()) { @@ -480,6 +484,7 @@ namespace spot } private: + ars_statistics* ars; state_set seen; const m_source_trans& target; const heap& h; @@ -533,7 +538,7 @@ namespace spot typename m_source_trans::iterator i = target.find(current.dest); if (i == target.end()) { - min_path s(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); @@ -563,7 +568,7 @@ namespace spot << a_->format_state(begin) << std::endl; transition tmp; target.insert(std::make_pair(begin, tmp)); - min_path s(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); @@ -598,7 +603,7 @@ namespace spot else { // This initial state is outside the cycle. Compute the prefix. - min_path s(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 0a58d747c..89c779350 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -252,6 +252,36 @@ struct acss_stat } }; +struct ars_stat +{ + int min_states; + int max_states; + int tot_states; + int n; + + ars_stat() + : n(0) + { + } + + void + count(const spot::ars_statistics* acss) + { + int s = acss->ars_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; @@ -299,6 +329,8 @@ ec_stats_type ec_stats; typedef std::map acss_stats_type; acss_stats_type acss_stats; +typedef std::map ars_stats_type; +ars_stats_type ars_stats; typedef std::map ar_stats_type; ar_stats_type ar_stats; // Statistics about accepting runs. @@ -586,10 +618,21 @@ main(int argc, char** argv) if (opt_replay) { spot::tgba_run* run; + + const spot::ars_statistics* ars = + dynamic_cast(res); + tm_ar.start(algo); for (int count = opt_R;;) { run = res->accepting_run(); + if (opt_z && ars) + { + // Count only the first run (the other way + // would be to divide the stats by opt_R). + ars_stats[algo].count(ars); + ars = 0; + } if (count-- <= 0 || !run) break; delete run; @@ -784,6 +827,37 @@ main(int argc, char** argv) << std::endl; std::cout << std::setiosflags(old); } + if (!ars_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 run computation:" + << std::endl; + std::cout << std::setw(22) << "" + << " | (non unique) states |" + << 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_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()) {