diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc index 9a2005286..0287166b1 100644 --- a/src/tgbaalgos/degen.cc +++ b/src/tgbaalgos/degen.cc @@ -24,6 +24,10 @@ #include "ltlast/constant.hh" #include #include +#include "tgbaalgos/scc.hh" +#include "tgba/bddprint.hh" + +//#define DEGEN_DEBUG namespace spot { @@ -39,7 +43,7 @@ namespace spot size_t operator()(const degen_state& s) const { - return s.first->hash() & wang32_hash(s.second); + return s.first->hash() & wang32_hash(s.second); } }; @@ -47,17 +51,17 @@ namespace spot { bool operator()(const degen_state& left, - const degen_state& right) const + const degen_state& right) const { - if (left.second != right.second) - return false; - return left.first->compare(right.first) == 0; + if (left.second != right.second) + return false; + return left.first->compare(right.first) == 0; } }; // Associate the degeneralized state to its number. typedef Sgi::hash_map ds2num_map; + degen_state_hash, degen_state_equal> ds2num_map; // Queue of state to be processed. typedef std::deque queue_t; @@ -66,22 +70,22 @@ namespace spot class unicity_table { typedef Sgi::hash_set uniq_set; + state_ptr_hash, state_ptr_equal> uniq_set; uniq_set m; public: const state* operator()(const state* s) { - uniq_set::const_iterator i = m.find(s); - if (i == m.end()) - { - m.insert(s); - return s; - } - else - { - s->destroy(); - return *i; - } + uniq_set::const_iterator i = m.find(s); + if (i == m.end()) + { + m.insert(s); + return s; + } + else + { + s->destroy(); + return *i; + } } ~unicity_table() @@ -94,6 +98,12 @@ namespace spot (*old)->destroy(); } } + + size_t + size() + { + return m.size(); + } }; // Acceptance set common to all outgoing transitions of some state. @@ -102,7 +112,7 @@ namespace spot const tgba* a_; typedef std::pair cache_entry; typedef Sgi::hash_map cache_t; + state_ptr_hash, state_ptr_equal> cache_t; cache_t cache_; public: @@ -112,42 +122,122 @@ namespace spot cache_t::const_iterator fill_cache(const state* s) { - bdd common = a_->all_acceptance_conditions(); - bdd union_ = bddfalse; - tgba_succ_iterator* it = a_->succ_iter(s); - for (it->first(); !it->done(); it->next()) - { - bdd set = it->current_acceptance_conditions(); - common &= set; - union_ |= set; - } - delete it; - cache_entry e(common, union_); - return cache_.insert(std::make_pair(s, e)).first; + bdd common = a_->all_acceptance_conditions(); + bdd union_ = bddfalse; + tgba_succ_iterator* it = a_->succ_iter(s); + for (it->first(); !it->done(); it->next()) + { + bdd set = it->current_acceptance_conditions(); + common &= set; + union_ |= set; + } + delete it; + cache_entry e(common, union_); + return cache_.insert(std::make_pair(s, e)).first; } // Intersection of all outgoing acceptance sets bdd common_acc(const state* s) { - cache_t::const_iterator i = cache_.find(s); - if (i == cache_.end()) - i = fill_cache(s); - return i->second.first; + cache_t::const_iterator i = cache_.find(s); + if (i == cache_.end()) + i = fill_cache(s); + return i->second.first; } // Union of all outgoing acceptance sets bdd union_acc(const state* s) { - cache_t::const_iterator i = cache_.find(s); - if (i == cache_.end()) - i = fill_cache(s); - return i->second.second; + cache_t::const_iterator i = cache_.find(s); + if (i == cache_.end()) + i = fill_cache(s); + return i->second.second; + } + }; + + // Order of accepting sets (for one SCC) + class acc_order + { + std::vector order_; + bdd found_; + + public: + unsigned + next_level(bdd all, int slevel, bdd acc) + { + bdd temp = acc; + if (all != found_) + { + // Check for new conditions in acc + if ((acc & found_) != acc) + { + bdd acc_t = acc; + while (acc_t != bddfalse) + { + bdd next = bdd_satone(acc_t); + acc_t -= next; + // Add new condition + if ((next & found_) != next) + { + order_.push_back(next); + found_ |= next; + } + } + } + } + + acc = temp; + unsigned next = slevel; + while (next < order_.size() + && (acc & order_[next]) == order_[next]) + ++next; + return next; + } + + void + print(int scc, const bdd_dict* dict) + { + std::vector::iterator i; + std::cout << "Order_" << scc << ":\t"; + for (i=order_.begin(); i!=order_.end(); i++) + { + bdd_print_acc(std::cout, dict, *i); + std::cout << ", "; + } + std::cout << std::endl; + } + }; + + // Accepting order for each SCC + class scc_orders + { + bdd all_; + std::map orders_; + + public: + scc_orders(bdd all): all_(all) + { + } + + unsigned + next_level(int scc, int slevel, bdd acc) + { + return orders_[scc].next_level(all_, slevel, acc); + } + + void + print(const bdd_dict* dict) + { + std::map::iterator i; + for (i = orders_.begin(); i != orders_.end(); i++) + i->second.print(i->first, dict); } }; } sba* - degeneralize(const tgba* a) + degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders, + bool use_lvl_cache) { bdd_dict* dict = a->get_dict(); @@ -177,13 +267,16 @@ namespace spot // during the translation.) bdd all = a->all_acceptance_conditions(); while (all != bddfalse) - { - bdd next = bdd_satone(all); - all -= next; - order.push_back(next); - } + { + bdd next = bdd_satone(all); + all -= next; + order.push_back(next); + } } + // Initialize scc_orders + scc_orders orders(a->all_acceptance_conditions()); + outgoing_acc outgoing(a); // Make sure we always use the same pointer for identical states @@ -202,6 +295,17 @@ namespace spot typedef std::map tr_cache_t; tr_cache_t tr_cache; + + // State level cash + typedef std::map lvl_cache_t; + lvl_cache_t lvl_cache; + + // Compute SCCs in order to use custom acc order for each SCC + // or lvl_cache + scc_map m(a); + if (use_cust_acc_orders || use_lvl_cache) + m.build_map(); + queue_t todo; const state* s0 = uniq(a->get_init_state()); @@ -213,84 +317,116 @@ namespace spot bdd all = a->all_acceptance_conditions(); tgba_succ_iterator* it = a->succ_iter(s0); for (it->first(); !it->done(); it->next()) - { - // Look only for transitions that are accepting. - if (all != it->current_acceptance_conditions()) - continue; - // Look only for self-loops. - const state* dest = uniq(it->current_state()); - if (dest == s0) - { - // The initial state has an accepting self-loop. - s.second = order.size(); - break; - } - } + { + // Look only for transitions that are accepting. + if (all != it->current_acceptance_conditions()) + continue; + // Look only for self-loops. + const state* dest = uniq(it->current_state()); + if (dest == s0) + { + // The initial state has an accepting self-loop. + s.second = order.size(); + break; + } + } delete it; } +#ifdef DEGEN_DEBUG + std::mapnames; + names[s.first] = 1; + + ds2num[s] = 10000*names[s.first] + 100*s.second + m.scc_of_state(s.first); +#else ds2num[s] = 0; +#endif + todo.push_back(s); + // If use_lvl_cache is on insert initial state to level cash + // Level cash stores first encountered level for each state. + // When entering an SCC first the lvl_cache is checked. + // If such state exists level from chache is used. + // If not, a new level (starting with 0) is computed. + if (use_lvl_cache) + lvl_cache[s.first] = s.second; + while (!todo.empty()) { - s = todo.front(); - todo.pop_front(); - int src = ds2num[s]; - unsigned slevel = s.second; + s = todo.front(); + todo.pop_front(); + int src = ds2num[s]; + unsigned slevel = s.second; - // If we have a state on the last level, it should be accepting. - bool is_acc = slevel == order.size(); - // On the accepting level, start again from level 0. - if (is_acc) - slevel = 0; + // If we have a state on the last level, it should be accepting. + bool is_acc = slevel == order.size(); + // On the accepting level, start again from level 0. + if (is_acc) + slevel = 0; - tgba_succ_iterator* i = a->succ_iter(s.first); - for (i->first(); !i->done(); i->next()) - { - degen_state d(uniq(i->current_state()), 0); + // Check SCC for state s + int s_scc = -1; + if (use_lvl_cache || use_cust_acc_orders) + s_scc = m.scc_of_state(s.first); - // The old level is slevel. What should be the new one? - bdd acc = i->current_acceptance_conditions(); - bdd otheracc = outgoing.common_acc(d.first); + tgba_succ_iterator* i = a->succ_iter(s.first); + for (i->first(); !i->done(); i->next()) + { + degen_state d(uniq(i->current_state()), 0); - if (is_acc) - { - // Ignore the last expected acceptance set (the value of - // *prev below) if it is common to all other outgoing - // transitions (of the current state) AND if it is not - // used by any outgoing transition of the destination - // state. - // - // 1) It's correct to do that, because this acceptance - // set is common to other outgoing transitions. - // Therefore if we make a cycle to this state we - // will eventually see that acceptance set thanks - // to the "pulling" of the common acceptance sets - // of the destination state (d.first). - // - // 2) It's also desirable because it makes the - // degeneralization idempotent (up to a renaming of - // states). Consider the following automaton where - // 1 is initial and => marks accepting transitions: - // 1=>1, 1=>2, 2->2, 2->1 This is already an SBA, - // with 1 as accepting state. However if you try - // degeralize it without ignoring *prev, you'll get - // two copies of states 2, depending on whether we - // reach it using 1=>2 or from 2->2. If this - // example was not clear, uncomment this following - // "if" block, and play with the "degenid.test" - // test case. - // - // 3) Ignoring all common acceptance sets would also - // be correct, but it would make the - // degeneralization produce larger automata in some - // cases. The current condition to ignore only one - // acceptance set if is this not used by the next - // state is a heuristic that is compatible with - // point 2) above while not causing more states to - // be generated in our benchmark of 188 formulae - // from the literature. +#ifdef DEGEN_DEBUG + if (names.find(d.first) == names.end()) + names[d.first] = uniq.size(); +#endif + + // Check whether the target's SCC is accepting + bool is_scc_acc = false; + int scc = m.scc_of_state(i->current_state()); + if (m.accepting(scc)) + is_scc_acc = true; + + // The old level is slevel. What should be the new one? + bdd acc = i->current_acceptance_conditions(); + bdd otheracc = outgoing.common_acc(d.first); + + if (is_acc) + { + // Ignore the last expected acceptance set (the value of + // *prev below) if it is common to all other outgoing + // transitions (of the current state) AND if it is not + // used by any outgoing transition of the destination + // state. + // + // 1) It's correct to do that, because this acceptance + // set is common to other outgoing transitions. + // Therefore if we make a cycle to this state we + // will eventually see that acceptance set thanks + // to the "pulling" of the common acceptance sets + // of the destination state (d.first). + // + // 2) It's also desirable because it makes the + // degeneralization idempotent (up to a renaming of + // states). Consider the following automaton where + // 1 is initial and => marks accepting transitions: + // 1=>1, 1=>2, 2->2, 2->1 This is already an SBA, + // with 1 as accepting state. However if you try + // degeralize it without ignoring *prev, you'll get + // two copies of states 2, depending on whether we + // reach it using 1=>2 or from 2->2. If this + // example was not clear, uncomment this following + // "if" block, and play with the "degenid.test" + // test case. + // + // 3) Ignoring all common acceptance sets would also + // be correct, but it would make the + // degeneralization produce larger automata in some + // cases. The current condition to ignore only one + // acceptance set if is this not used by the next + // state is a heuristic that is compatible with + // point 2) above while not causing more states to + // be generated in our benchmark of 188 formulae + // from the literature. if (!order.empty()) { unsigned prev = order.size() - 1; @@ -302,70 +438,112 @@ namespace spot acc -= order[prev]; } } - } - // A transition in the SLEVEL acceptance set should - // be directed to the next acceptance set. If the - // current transition is also in the next acceptance - // set, then go to the one after, etc. - // - // See Denis Oddoux's PhD thesis for a nice - // explanation (in French). - // @PhDThesis{ oddoux.03.phd, - // author = {Denis Oddoux}, - // title = {Utilisation des automates alternants pour un - // model-checking efficace des logiques - // temporelles lin{\'e}aires.}, - // school = {Universit{\'e}e Paris 7}, - // year = {2003}, - // address= {Paris, France}, - // month = {December} - // } - unsigned next = slevel; - // Consider both the current acceptance sets, and the - // acceptance sets common to the outgoing transitions of - // the destination state. - acc |= otheracc; - while (next < order.size() && bdd_implies(order[next], acc)) - ++next; + } + // A transition in the SLEVEL acceptance set should + // be directed to the next acceptance set. If the + // current transition is also in the next acceptance + // set, then go to the one after, etc. + // + // See Denis Oddoux's PhD thesis for a nice + // explanation (in French). + // @PhDThesis{ oddoux.03.phd, + // author = {Denis Oddoux}, + // title = {Utilisation des automates alternants pour un + // model-checking efficace des logiques + // temporelles lin{\'e}aires.}, + // school = {Universit{\'e}e Paris 7}, + // year = {2003}, + // address= {Paris, France}, + // month = {December} + // } + if (is_scc_acc) + { + acc |= otheracc; + // If use_z_lvl is on, start with level zero 0 when swhitching SCCs + unsigned next = (!use_z_lvl || s_scc == scc)?slevel:0; - d.second = next; + // If lvl_cache is used and switching SCCs, use level from cahce + if (use_lvl_cache && s_scc != scc && lvl_cache.find(d.first) != lvl_cache.end()) + { + d.second = lvl_cache[d.first]; + } + else + { + // If using custom acc orders, get next level for this scc + if (use_cust_acc_orders) + d.second = orders.next_level(scc, next, acc); + // Else compute level according the global acc order + else + { + // Consider both the current acceptance sets, and the + // acceptance sets common to the outgoing transitions of + // the destination state. + while (next < order.size() + && (acc & order[next]) == order[next]) + ++next; - // Have we already seen this destination? - int dest; - ds2num_map::const_iterator di = ds2num.find(d); - if (di != ds2num.end()) - { - dest = di->second; - } - else - { - dest = ds2num.size(); - ds2num[d] = dest; - todo.push_back(d); - } + d.second = next; + } + } + } - state_explicit_number::transition*& t = - tr_cache[dest * 2 + is_acc]; + // Have we already seen this destination? + int dest; + ds2num_map::const_iterator di = ds2num.find(d); + if (di != ds2num.end()) + { + dest = di->second; + } + else + { +#ifdef DEGEN_DEBUG + dest = 10000*names[d.first] + 100*d.second + scc; +#else + dest = ds2num.size(); +#endif + ds2num[d] = dest; + todo.push_back(d); + // Insert new state to cash + if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end()) + lvl_cache[d.first] = d.second; + } - if (t == 0) - { - // Actually create the transition. - t = res->create_transition(src, dest); - t->condition = i->current_condition(); - // If the source state is accepting, we have to put - // degen_acc on all outgoing transitions. (We are still - // building a TGBA; we only assure that it can be used as - // an SBA.) - t->acceptance_conditions = is_acc ? degen_acc : bddfalse; - } - else - { - t->condition |= i->current_condition(); - } - } - delete i; - tr_cache.clear(); + state_explicit_number::transition*& t = + tr_cache[dest * 2 + is_acc]; + + if (t == 0) + { + // Actually create the transition. + t = res->create_transition(src, dest); + t->condition = i->current_condition(); + // If the source state is accepting, we have to put + // degen_acc on all outgoing transitions. (We are still + // building a TGBA; we only assure that it can be used as + // an SBA.) + t->acceptance_conditions = is_acc ? degen_acc : bddfalse; + } + else + { + t->condition |= i->current_condition(); + } + } + delete i; + tr_cache.clear(); } + +#ifdef DEGEN_DEBUG + std::vector::iterator i; + std::cout << "Orig. order: \t"; + for (i=order.begin(); i!=order.end(); i++) + { + bdd_print_acc(std::cout, dict, *i); + std::cout << ", "; + } + std::cout << std::endl; + orders.print(dict); +#endif + + res->merge_transitions(); return res; } } diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh index 3757ad8ab..10d2652ec 100644 --- a/src/tgbaalgos/degen.hh +++ b/src/tgbaalgos/degen.hh @@ -35,7 +35,8 @@ namespace spot /// /// \see tgba_sba_proxy, tgba_tba_proxy /// \ingroup tgba_misc - sba* degeneralize(const tgba* a); + sba* degeneralize(const tgba* a, bool use_z_lvl = true, bool use_cust_acc_orders = true, + bool use_lvl_cache = true); }