From 3f22bc17ffa756043acc10a1dba908f1cffd596b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 22 Sep 2005 15:28:10 +0000 Subject: [PATCH] * src/tgbaalgos/tau03opt.cc: Include . (tau03_opt_search): Add option "ordering" (off by default). If enabled, initialize an explicit ordering for acceptance conditions into the new member "cond" (a vector of bdds). (project_acc): New helper function for projecting a set of acceptance conditions to a subset that maximizes the number of initial consecutive conditions covered by the set in the condition ordering. (dfs_blue): Implement the ordering heuristic. (dfs_red): Use a sentinel in condition_stack to avoid explicit checks for the stack's emptiness. Consider also the conditions in acc when checking for the completion of an accepting cycle. Fix the implementation of condition heuristic. Implement the ordering heuristic. Simplify the removal of elements from condition_stack (due to the way in which elements are pushed on the stack, there can be at most one element with a given depth in the stack at any one time). --- ChangeLog | 22 ++++++++++++ src/tgbaalgos/tau03opt.cc | 72 +++++++++++++++++++++++++++++---------- 2 files changed, 76 insertions(+), 18 deletions(-) diff --git a/ChangeLog b/ChangeLog index e3964f706..80c2c11bd 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,25 @@ +2005-09-20 Heikki Tauriainen + + * src/tgbaalgos/tau03opt.cc: Include . + (tau03_opt_search): Add option "ordering" (off by default). + If enabled, initialize an explicit ordering for acceptance + conditions into the new member "cond" (a vector of bdds). + (project_acc): New helper function for projecting a set of + acceptance conditions to a subset that maximizes the number + of initial consecutive conditions covered by the set in the + condition ordering. + (dfs_blue): Implement the ordering heuristic. + (dfs_red): Use a sentinel in condition_stack to avoid explicit + checks for the stack's emptiness. + Consider also the conditions in acc when checking for the + completion of an accepting cycle. + Fix the implementation of condition heuristic. + Implement the ordering heuristic. + Simplify the removal of elements from condition_stack (due to + the way in which elements are pushed on the stack, there can + be at most one element with a given depth in the stack at any + one time). + 2005-09-05 Heikki Tauriainen * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_prefix): diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc index 4f1c5630d..87c9f6805 100644 --- a/src/tgbaalgos/tau03opt.cc +++ b/src/tgbaalgos/tau03opt.cc @@ -41,6 +41,7 @@ #endif #include +#include #include #include "misc/hash.hh" #include "tgba/tgba.hh" @@ -56,8 +57,8 @@ namespace spot { enum color {WHITE, CYAN, BLUE}; - /// \brief Emptiness checker on spot::tgba automata having at most one - /// acceptance condition (i.e. a TBA). + /// \brief Emptiness checker on spot::tgba automata having a finite number + /// of acceptance conditions (i.e. a TGBA). template class tau03_opt_search : public emptiness_check, public ec_statistics { @@ -69,9 +70,20 @@ namespace spot h(size), all_acc(a->all_acceptance_conditions()), use_condition_stack(o.get("condstack")), + use_ordering(use_condition_stack && o.get("ordering")), use_weights(o.get("weights", 1)), use_red_weights(use_weights && o.get("redweights", 1)) { + if (use_ordering) + { + bdd all_conds = all_acc; + while (all_conds != bddfalse) + { + bdd acc = bdd_satone(all_conds); + cond.push_back(acc); + all_conds -= acc; + } + } } virtual ~tau03_opt_search() @@ -149,6 +161,16 @@ namespace spot st.pop_front(); } + bdd project_acc(bdd acc) const + { + bdd result = bddfalse; + for (std::vector::const_iterator i = cond.begin(); + i != cond.end() && (acc & *i) != bddfalse; + ++i) + result |= *i; + return result; + } + /// \brief weight of the state on top of the blue stack. weight current_weight; @@ -167,11 +189,17 @@ namespace spot /// Whether to use the "condition stack". bool use_condition_stack; + /// Whether to use an ordering between the acceptance conditions. + /// Effective only if using the condition stack. + bool use_ordering; /// Whether to use weights to abort earlier. bool use_weights; /// Whether to use weights in the red dfs. bool use_red_weights; + /// Ordering of the acceptance conditions. + std::vector cond; + bool dfs_blue() { while (!st_blue.empty()) @@ -210,7 +238,7 @@ namespace spot { trace << " It is cyan and acceptance condition " << "is reached, report cycle" << std::endl; - c_prime.cumulate_acc(c.get_acc() | acc); + c_prime.cumulate_acc(all_acc); push(st_red, s_prime, label, acc); return true; } @@ -218,11 +246,12 @@ namespace spot { trace << " It is cyan or blue and"; bdd acu = acc | c.get_acc(); - if ((c_prime.get_acc() & acu) != acu) + bdd acp = (use_ordering ? project_acc(acu) : acu); + if ((c_prime.get_acc() & acp) != acp) { trace << " a propagation is needed, " << "start a red dfs" << std::endl; - c_prime.cumulate_acc(acu); + c_prime.cumulate_acc(acp); push(st_red, s_prime, label, acc); if (dfs_red(acu)) return true; @@ -254,13 +283,14 @@ namespace spot h.get_color_ref(st_blue.front().s); assert(!c.is_white()); bdd acu = f_dest.acc | c.get_acc(); - if ((c_prime.get_acc() & acu) != acu) + bdd acp = (use_ordering ? project_acc(acu) : acu); + if ((c_prime.get_acc() & acp) != acp) { trace << " The arc from " << a_->format_state(st_blue.front().s) << " to the current state implies to " << " start a red dfs" << std::endl; - c_prime.cumulate_acc(acu); + c_prime.cumulate_acc(acp); push(st_red, f_dest.s, f_dest.label, f_dest.acc); if (dfs_red(acu)) return true; @@ -290,6 +320,7 @@ namespace spot typedef std::pair cond_level; std::stack condition_stack; unsigned depth = 1; + condition_stack.push(cond_level(bddfalse, 0)); while (!st_red.empty()) { @@ -310,31 +341,40 @@ namespace spot { trace << " It is white, pop it" << std::endl; delete s_prime; + continue; } else if (c_prime.get_color() == CYAN && (all_acc == ((use_red_weights ? (current_weight - c_prime.get_weight()) : bddfalse) | c_prime.get_acc() + | acc | acu))) { trace << " It is cyan and acceptance condition " << "is reached, report cycle" << std::endl; - c_prime.cumulate_acc(acu); + c_prime.cumulate_acc(all_acc); push(st_red, s_prime, label, acc); return true; } - else if ((c_prime.get_acc() & acu) != acu) + bdd acp; + if (use_ordering) + acp = project_acc(c_prime.get_acc() | acu | acc); + else if (use_condition_stack) + acp = acu | acc; + else + acp = acu; + if ((c_prime.get_acc() & acp) != acp) { trace << " It is cyan or blue and propagation " << "is needed, go down" << std::endl; - c_prime.cumulate_acc(acu); + c_prime.cumulate_acc(acp); push(st_red, s_prime, label, acc); if (use_condition_stack) { bdd old = acu; - acu = c_prime.get_acc(); + acu |= acc; condition_stack.push(cond_level(acu - old, depth)); } ++depth; @@ -353,14 +393,10 @@ namespace spot h.pop_notify(f.s); pop(st_red); --depth; - if (use_condition_stack) + if (condition_stack.top().second == depth) { - while (!condition_stack.empty() - && condition_stack.top().second == depth) - { - acu -= condition_stack.top().first; - condition_stack.pop(); - } + acu -= condition_stack.top().first; + condition_stack.pop(); } } }