From 191fa370e25aa04d5ab30f2f8bec8b5812c742f4 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 13 May 2012 14:25:59 +0200 Subject: [PATCH] Overhaul bdddict to speedup bdd->formula lookups. * src/tgba/bdddict.hh, src/tgba/bdddict.cc: Store variable types and associated formula in a vector indexed by BDD variable numbers, instead of using several maps. * src/evtgbaalgos/tgba2evtgba.cc, src/tgba/bddprint.cc, src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/save.cc: Adjust usage. --- src/evtgbaalgos/tgba2evtgba.cc | 11 +- src/tgba/bdddict.cc | 293 ++++++++++++++++++--------------- src/tgba/bdddict.hh | 35 ++-- src/tgba/bddprint.cc | 61 +++---- src/tgba/formula2bdd.cc | 6 +- src/tgbaalgos/ltl2tgba_fm.cc | 13 +- src/tgbaalgos/save.cc | 10 +- 7 files changed, 218 insertions(+), 211 deletions(-) diff --git a/src/evtgbaalgos/tgba2evtgba.cc b/src/evtgbaalgos/tgba2evtgba.cc index d5d26d932..ca7030ab7 100644 --- a/src/evtgbaalgos/tgba2evtgba.cc +++ b/src/evtgbaalgos/tgba2evtgba.cc @@ -1,7 +1,8 @@ -// Copyright (C) 2009, 2011 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -90,7 +91,7 @@ namespace spot if (low == bddfalse) { const ltl::formula* v = - aut_->get_dict()->var_formula_map[bdd_var(one)]; + aut_->get_dict()->bdd_map[bdd_var(one)].f; res->add_transition(name_[in], to_string(v), ss, @@ -125,7 +126,7 @@ namespace spot if (low == bddfalse) { const ltl::formula* v = - aut_->get_dict()->acc_formula_map[bdd_var(one)]; + aut_->get_dict()->bdd_map[bdd_var(one)].f; ss.insert(rsymbol(to_string(v))); break; } diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index bbd1a1c46..8130e8d9b 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -35,6 +35,7 @@ namespace spot { bdd_dict::bdd_dict() : bdd_allocator(), + bdd_map(bdd_varnum()), next_to_now(bdd_newpair()), now_to_next(bdd_newpair()) { @@ -63,9 +64,11 @@ namespace spot f = f->clone(); num = allocate_variables(1); var_map[f] = num; - var_formula_map[num] = f; + bdd_map.resize(bdd_varnum()); + bdd_map[num].type = var; + bdd_map[num].f = f; } - var_refs[num].insert(for_me); + bdd_map[num].refs.insert(for_me); return num; } @@ -75,9 +78,11 @@ namespace spot if (f == bddtrue || f == bddfalse) return; - vf_map::iterator i = var_formula_map.find(bdd_var(f)); - assert(i != var_formula_map.end()); - var_refs[i->first].insert(for_me); + int v = bdd_var(f); + assert(unsigned(v) < bdd_map.size()); + bdd_info& i = bdd_map[v]; + assert(i.type == var); + i.refs.insert(for_me); register_propositions(bdd_high(f), for_me); register_propositions(bdd_low(f), for_me); @@ -98,13 +103,17 @@ namespace spot f = f->clone(); num = allocate_variables(2); now_map[f] = num; - now_formula_map[num] = f; + bdd_map.resize(bdd_varnum()); + bdd_map[num].type = now; + bdd_map[num].f = f; + bdd_map[num + 1].type = next; + bdd_map[num + 1].f = f; // Record that num+1 should be renamed as num when // the next state becomes current. bdd_setpair(next_to_now, num + 1, num); bdd_setpair(now_to_next, num, num + 1); } - var_refs[num].insert(for_me); + bdd_map[num].refs.insert(for_me); // Keep only references for now. return num; } @@ -124,9 +133,13 @@ namespace spot f = f->clone(); num = allocate_variables(1); acc_map[f] = num; - acc_formula_map[num] = f; + bdd_map.resize(bdd_varnum()); + bdd_info& i = bdd_map[num]; + i.type = acc; + i.f = f; + i.clone_counts = 0; } - var_refs[num].insert(for_me); + bdd_map[num].refs.insert(for_me); return num; } @@ -136,9 +149,11 @@ namespace spot if (f == bddtrue || f == bddfalse) return; - vf_map::iterator i = acc_formula_map.find(bdd_var(f)); - assert(i != acc_formula_map.end()); - var_refs[i->first].insert(for_me); + int v = bdd_var(f); + assert(unsigned(v) < bdd_map.size()); + bdd_info& i = bdd_map[v]; + assert(i.type == acc); + i.refs.insert(for_me); register_acceptance_variables(bdd_high(f), for_me); register_acceptance_variables(bdd_low(f), for_me); @@ -146,14 +161,15 @@ namespace spot int - bdd_dict::register_clone_acc(int var, const void* for_me) + bdd_dict::register_clone_acc(int v, const void* for_me) { - vf_map::iterator i = acc_formula_map.find(var); - assert(i != acc_formula_map.end()); + assert(unsigned(v) < bdd_map.size()); + bdd_info& i = bdd_map[v]; + assert(i.type == acc); + std::ostringstream s; // FIXME: We could be smarter and reuse unused "$n" numbers. - s << ltl::to_string(i->second) << "$" - << ++clone_counts[var]; + s << ltl::to_string(i.f) << "$" << ++i.clone_counts; const ltl::formula* f = ltl::atomic_prop::instance(s.str(), ltl::default_environment::instance()); @@ -177,8 +193,13 @@ namespace spot } int res = i->second.register_n(n); + bdd_map.resize(bdd_varnum()); + while (n--) - var_refs[res + n].insert(for_me); + { + bdd_map[res + n].type = anon; + bdd_map[res + n].refs.insert(for_me); + } return res; } @@ -188,10 +209,10 @@ namespace spot bdd_dict::register_all_variables_of(const void* from_other, const void* for_me) { - vr_map::iterator i; - for (i = var_refs.begin(); i != var_refs.end(); ++i) + bdd_info_map::iterator i; + for (i = bdd_map.begin(); i != bdd_map.end(); ++i) { - ref_set& s = i->second; + ref_set& s = i->refs; if (s.find(from_other) != s.end()) s.insert(for_me); } @@ -203,30 +224,21 @@ namespace spot } void - bdd_dict::unregister_variable(int var, const void* me) + bdd_dict::unregister_variable(int v, const void* me) { - vr_map::iterator i = var_refs.find(var); - assert(i != var_refs.end()); - unregister_variable(i, me); - } + assert(unsigned(v) < bdd_map.size()); - void - bdd_dict::unregister_variable(vr_map::iterator& cur, const void* me) - { - ref_set& s = cur->second; + ref_set& s = bdd_map[v].refs; ref_set::iterator si = s.find(me); if (si == s.end()) return; s.erase(si); - int var = cur->first; // If var is anonymous, we should reinsert it into the free list // of ME's anonymous variables. - if (var_formula_map.find(var) == var_formula_map.end() - && now_formula_map.find(var) == now_formula_map.end() - && acc_formula_map.find(var) == acc_formula_map.end()) - free_anonymous_list_of[me].release_n(var, 1); + if (bdd_map[v].type == anon) + free_anonymous_list_of[me].release_n(v, 1); if (!s.empty()) return; @@ -236,65 +248,52 @@ namespace spot // if this is a Now, a Var, or an Acc variable. int n = 1; const ltl::formula* f = 0; - vf_map::iterator vi = var_formula_map.find(var); - if (vi != var_formula_map.end()) + switch (bdd_map[v].type) { - f = vi->second; + case var: + f = bdd_map[v].f; var_map.erase(f); - var_formula_map.erase(vi); - } - else - { - vi = now_formula_map.find(var); - if (vi != now_formula_map.end()) - { - f = vi->second; - now_map.erase(f); - now_formula_map.erase(vi); - n = 2; - bdd_setpair(next_to_now, var + 1, var + 1); - bdd_setpair(now_to_next, var, var); - } - else - { - vi = acc_formula_map.find(var); - if (vi != acc_formula_map.end()) - { - f = vi->second; - acc_map.erase(f); - acc_formula_map.erase(vi); - } - else - { - free_anonymous_list_of_type::iterator i; - // Nobody use this variable as an anonymous variable - // anymore, so remove it entirely from the anonymous - // free list so it can be used for something else. - for (i = free_anonymous_list_of.begin(); - i != free_anonymous_list_of.end(); ++i) - i->second.remove(var, n); - } - } + break; + case now: + f = bdd_map[v].f; + now_map.erase(f); + bdd_setpair(now_to_next, v, v); + bdd_setpair(next_to_now, v + 1, v + 1); + n = 2; + break; + case next: + break; + case acc: + f = bdd_map[v].f; + acc_map.erase(f); + break; + case anon: + { + free_anonymous_list_of_type::iterator i; + // Nobody use this variable as an anonymous variable + // anymore, so remove it entirely from the anonymous + // free list so it can be used for something else. + for (i = free_anonymous_list_of.begin(); + i != free_anonymous_list_of.end(); ++i) + i->second.remove(v, n); + break; + } } // Actually release the associated BDD variables, and the // formula itself. - release_variables(var, n); + release_variables(v, n); if (f) f->destroy(); - var_refs.erase(cur); + while (n--) + bdd_map[v + n].type = anon; } void bdd_dict::unregister_all_my_variables(const void* me) { - vr_map::iterator i; - for (i = var_refs.begin(); i != var_refs.end();) - { - // Increment i++ now, we will possibly erase - // the current node (which would invalidate the iterator). - vr_map::iterator cur = i++; - unregister_variable(cur, me); - } + unsigned s = bdd_map.size(); + for (unsigned i = 0; i < s; ++i) + unregister_variable(i, me); free_anonymous_list_of.erase(me); } @@ -304,7 +303,7 @@ namespace spot fv_map::iterator fi = var_map.find(f); if (fi == var_map.end()) return false; - ref_set& s = var_refs[fi->second]; + ref_set& s = bdd_map[fi->second].refs; return s.find(by_me) != s.end(); } @@ -314,59 +313,59 @@ namespace spot fv_map::iterator fi = now_map.find(f); if (fi == now_map.end()) return false; - ref_set& s = var_refs[fi->second]; + ref_set& s = bdd_map[fi->second].refs; return s.find(by_me) != s.end(); } bool bdd_dict::is_registered_acceptance_variable(const ltl::formula* f, - const void* by_me) + const void* by_me) { fv_map::iterator fi = acc_map.find(f); if (fi == acc_map.end()) return false; - ref_set& s = var_refs[fi->second]; + ref_set& s = bdd_map[fi->second].refs; return s.find(by_me) != s.end(); } std::ostream& bdd_dict::dump(std::ostream& os) const { - fv_map::const_iterator fi; - os << "Atomic Propositions:" << std::endl; - for (fi = var_map.begin(); fi != var_map.end(); ++fi) + os << "Variable Map:\n"; + unsigned s = bdd_map.size(); + for (unsigned i = 0; i < s; ++i) { - os << " " << fi->second << " (x" - << var_refs.find(fi->second)->second.size() << "): "; - to_string(fi->first, os) << std::endl; + os << " " << i << " "; + const bdd_info& r = bdd_map[i]; + switch (r.type) + { + case anon: + os << (r.refs.empty() ? "Free" : "Anon"); + break; + case now: + os << "Now[" << to_string(r.f) << "]"; + break; + case next: + os << "Next[" << to_string(r.f) << "]"; + break; + case acc: + os << "Acc[" << to_string(r.f) << "]"; + break; + case var: + os << "Var[" << to_string(r.f) << "]"; + break; + } + if (!r.refs.empty()) + { + os << " x" << r.refs.size() << " {"; + for (ref_set::const_iterator si = r.refs.begin(); + si != r.refs.end(); ++si) + os << " " << *si; + os << " }"; + } + os << "\n"; } - os << "States:" << std::endl; - for (fi = now_map.begin(); fi != now_map.end(); ++fi) - { - int refs = var_refs.find(fi->second)->second.size(); - os << " " << fi->second << " (x" << refs << "): Now["; - to_string(fi->first, os) << "]" << std::endl; - os << " " << fi->second + 1 << " (x" << refs << "): Next["; - to_string(fi->first, os) << "]" << std::endl; - } - os << "Acceptance Conditions:" << std::endl; - for (fi = acc_map.begin(); fi != acc_map.end(); ++fi) - { - os << " " << fi->second << " (x" - << var_refs.find(fi->second)->second.size() << "): Acc["; - to_string(fi->first, os) << "]" << std::endl; - } - os << "Ref counts:" << std::endl; - vr_map::const_iterator ri; - for (ri = var_refs.begin(); ri != var_refs.end(); ++ri) - { - os << " " << ri->first << " :"; - for (ref_set::const_iterator si = ri->second.begin(); - si != ri->second.end(); ++si) - os << " " << *si; - os << std::endl; - } - os << "Anonymous lists:" << std::endl; + os << "Anonymous lists:\n"; free_anonymous_list_of_type::const_iterator ai; for (ai = free_anonymous_list_of.begin(); ai != free_anonymous_list_of.end(); ++ai) @@ -374,7 +373,7 @@ namespace spot os << " [" << ai->first << "] "; ai->second.dump_free_list(os) << std::endl; } - os << "Free list:" << std::endl; + os << "Free list:\n"; dump_free_list(os); os << std::endl; return os; @@ -384,36 +383,62 @@ namespace spot bdd_dict::assert_emptiness() const { bool fail = false; + + bool var_seen = false; + bool acc_seen = false; + bool now_seen = false; + bool next_seen = false; + bool refs_seen = false; + unsigned s = bdd_map.size(); + for (unsigned i = 0; i < s; ++i) + { + switch (bdd_map[i].type) + { + case var: + var_seen = true; + break; + case acc: + acc_seen = true; + break; + case now: + now_seen = true; + break; + case next: + next_seen = true; + break; + case anon: + break; + } + refs_seen |= !bdd_map[i].refs.empty(); + } if (var_map.empty() && now_map.empty() && acc_map.empty()) { - if (!var_formula_map.empty()) + if (var_seen) { - std::cerr << "var_map is empty but var_formula_map is not" - << std::endl; + std::cerr << "var_map is empty but Var in map" << std::endl; fail = true; } - if (!now_formula_map.empty()) + if (now_seen) { - std::cerr << "now_map is empty but now_formula_map is not" - << std::endl; + std::cerr << "now_map is empty but Now in map" << std::endl; fail = true; } - if (!acc_formula_map.empty()) + else if (next_seen) { - std::cerr << "acc_map is empty but acc_formula_map is not" - << std::endl; + std::cerr << "Next variable seen (without Now) in map" << std::endl; fail = true; } - if (!var_refs.empty()) + if (acc_seen) + { + std::cerr << "acc_map is empty but Acc in map" << std::endl; + fail = true; + } + if (refs_seen) { std::cerr << "maps are empty but var_refs is not" << std::endl; fail = true; - vr_map::const_iterator i; - for (i = var_refs.begin(); i != var_refs.end(); ++i) - std::cerr << " " << i->first << ":" << i->second.size(); - std::cerr << std::endl; } if (!fail) return; diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 70528d863..a33f9ba42 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -1,7 +1,8 @@ -// Copyright (C) 2011 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), -// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // // This file is part of Spot, a model checking library. @@ -29,6 +30,7 @@ #include #include #include +#include #include "ltlast/formula.hh" #include "misc/bddalloc.hh" @@ -57,15 +59,23 @@ namespace spot typedef std::map vf_map; fv_map now_map; ///< Maps formulae to "Now" BDD variables - vf_map now_formula_map; ///< Maps "Now" BDD variables to formulae fv_map var_map; ///< Maps atomic propositions to BDD variables - vf_map var_formula_map; ///< Maps BDD variables to atomic propositions fv_map acc_map; ///< Maps acceptance conditions to BDD variables - vf_map acc_formula_map; ///< Maps BDD variables to acceptance conditions - /// Clone counts. - typedef std::map cc_map; - cc_map clone_counts; + /// BDD-variable reference counts. + typedef std::set ref_set; + + enum var_type { anon = 0, now, next, var, acc }; + struct bdd_info { + bdd_info() : type(anon) {} + var_type type; + const ltl::formula* f; // Used unless t==anon. + ref_set refs; + int clone_counts; + }; + typedef std::vector bdd_info_map; + // Map BDD variables to their meaning. + bdd_info_map bdd_map; /// \brief Map Next variables to Now variables. /// @@ -182,13 +192,6 @@ namespace spot void assert_emptiness() const; protected: - /// BDD-variable reference counts. - typedef std::set ref_set; - typedef std::map vr_map; - vr_map var_refs; - - void unregister_variable(vr_map::iterator& cur, const void* me); - // SWIG does not grok the following definition, no idea why. // It's not important for the Python interface anyway. #ifndef SWIG diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 3e014c1bd..2188cf059 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -51,50 +51,37 @@ namespace spot /// Stream handler used by Buddy to display BDD variables. static void - print_handler(std::ostream& o, int var) + print_handler(std::ostream& o, int v) { - bdd_dict::vf_map::const_iterator isi = - dict->var_formula_map.find(var); - if (isi != dict->var_formula_map.end()) - to_string(isi->second, o); - else + assert(unsigned(v) < dict->bdd_map.size()); + const bdd_dict::bdd_info& ref = dict->bdd_map[v]; + switch (ref.type) { - isi = dict->acc_formula_map.find(var); - if (isi != dict->acc_formula_map.end()) + case bdd_dict::var: + to_string(ref.f, o); + break; + case bdd_dict::acc: + if (want_acc) { - if (want_acc) - { - o << "Acc["; - print_ltl(isi->second, o) << "]"; - } - else - { - o << "\""; - print_ltl(isi->second, o) << "\""; - } + o << "Acc["; + print_ltl(ref.f, o) << "]"; } else { - isi = dict->now_formula_map.find(var); - if (isi != dict->now_formula_map.end()) - { - o << "Now["; - print_ltl(isi->second, o) << "]"; - } - else - { - isi = dict->now_formula_map.find(var - 1); - if (isi != dict->now_formula_map.end()) - { - o << "Next["; - print_ltl(isi->second, o) << "]"; - } - else - { - o << "?" << var; - } - } + o << "\""; + print_ltl(ref.f, o) << "\""; } + break; + case bdd_dict::now: + o << "Now["; + print_ltl(ref.f, o) << "]"; + break; + case bdd_dict::next: + o << "Next["; + print_ltl(ref.f, o) << "]"; + break; + case bdd_dict::anon: + o << "?" << v; } } diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index a57fa61b8..0edbd4ff6 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -193,9 +193,9 @@ namespace spot while (b != bddtrue) { int var = bdd_var(b); - bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); - assert(isi != d->var_formula_map.end()); - const formula* res = isi->second->clone(); + const bdd_dict::bdd_info& i = d->bdd_map[var]; + assert(i.type == bdd_dict::var); + const formula* res = i.f->clone(); bdd high = bdd_high(b); if (high == bddfalse) diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 5f11657e5..f91eed2b9 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -283,16 +283,9 @@ namespace spot vf_map::const_iterator isi = next_formula_map.find(var); if (isi != next_formula_map.end()) return isi->second->clone(); - isi = dict->acc_formula_map.find(var); - if (isi != dict->acc_formula_map.end()) - return isi->second->clone(); - isi = dict->var_formula_map.find(var); - if (isi != dict->var_formula_map.end()) - return isi->second->clone(); - assert(0); - // Never reached, but some GCC versions complain about - // a missing return otherwise. - return 0; + const bdd_dict::bdd_info& i = dict->bdd_map[var]; + assert(i.type == bdd_dict::acc || i.type == bdd_dict::var); + return i.f->clone(); } bdd diff --git a/src/tgbaalgos/save.cc b/src/tgbaalgos/save.cc index 5169c3ae6..f2eaa491e 100644 --- a/src/tgbaalgos/save.cc +++ b/src/tgbaalgos/save.cc @@ -85,12 +85,10 @@ namespace spot if (bdd_high(cube) != bddfalse) { int v = bdd_var(cube); - bdd_dict::vf_map::const_iterator vi = - d->acc_formula_map.find(v); - assert(vi != d->acc_formula_map.end()); - std::string s = ltl::to_string(vi->second); - if (dynamic_cast(vi->second) - && s[0] == '"') + const bdd_dict::bdd_info& i = d->bdd_map[v]; + assert(i.type == bdd_dict::acc); + std::string s = ltl::to_string(i.f); + if (is_atomic_prop(i.f) && s[0] == '"') { // Unquote atomic propositions. s.erase(s.begin());