From 784ccafb1b924c2899b8fefeb4cd9857d5d05199 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 23 Mar 2004 09:39:38 +0000 Subject: [PATCH] * src/misc/freelist.hh (free_list::remove, free_list::insert): New methods. * src/misc/freelist.cc (free_list::register_n, free_list::releases_n): Rewrite using free_list::remove and free_list::insert. (free_list::remove, free_list::insert): New methods. * src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables): New method. (bdd_dict::annon_free_list): New subclass. (bdd_dict::free_annonymous_list_of_type_of): New attribute. * src/tgba/bdddict.cc (bdd_dict::register_all_variables_of, bdd_dict::unregister_all_my_variables): Handle anonymous variables too. (bdd_dict::register_anonymous_variables, bdd_dict::annon_free_list::annon_free_list, bdd_dict::annon_free_list::extend): New methods. --- ChangeLog | 17 ++++++ src/misc/freelist.cc | 128 ++++++++++++++++++++++++++++++++++--------- src/misc/freelist.hh | 10 ++++ src/tgba/bdddict.cc | 60 ++++++++++++++++++-- src/tgba/bdddict.hh | 31 ++++++++++- 5 files changed, 213 insertions(+), 33 deletions(-) diff --git a/ChangeLog b/ChangeLog index 346d6a97d..d408324a5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,22 @@ 2004-03-23 Alexandre DURET-LUTZ + * src/misc/freelist.hh (free_list::remove, free_list::insert): New + methods. + * src/misc/freelist.cc (free_list::register_n, + free_list::releases_n): Rewrite using free_list::remove and + free_list::insert. + (free_list::remove, free_list::insert): New methods. + * src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables): + New method. + (bdd_dict::annon_free_list): New subclass. + (bdd_dict::free_annonymous_list_of_type_of): New attribute. + * src/tgba/bdddict.cc (bdd_dict::register_all_variables_of, + bdd_dict::unregister_all_my_variables): Handle anonymous variables + too. + (bdd_dict::register_anonymous_variables, + bdd_dict::annon_free_list::annon_free_list, + bdd_dict::annon_free_list::extend): New methods. + * src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path) Fix handling of PATH when backtracking. Report from Soheib Baarir. diff --git a/src/misc/freelist.cc b/src/misc/freelist.cc index ce2d0bfbb..52c5a8638 100644 --- a/src/misc/freelist.cc +++ b/src/misc/freelist.cc @@ -56,13 +56,7 @@ namespace spot if (best != fl.end()) { int result = best->first; - best->second -= n; - assert(best->second >= 0); - // Erase the range if it's now empty. - if (best->second == 0) - fl.erase(best); - else - best->first += n; + remove(best, result, n); return result; } @@ -72,40 +66,119 @@ namespace spot } void - free_list::release_n(int base, int n) + free_list::insert(int base, int n) { free_list_type::iterator cur; int end = base + n; for (cur = fl.begin(); cur != fl.end(); ++cur) { - // Append to a range ... - if (cur->first + cur->second == base) + int cend = cur->first + cur->second; + // cur [....[ [......[ + // to insert [....[ [..[ + // ---------------------------------- + // result [......[ [......[ + if (cend >= base) { - cur->second += n; - // Maybe the next item on the list can be merged. - free_list_type::iterator next = cur; - ++next; - if (next != fl.end() && next->first == end) - { - cur->second += next->second; - fl.erase(next); - } - return; + if (cend >= end) + return; + // cur->second is set below. } - // ... or prepend to a range ... - if (cur->first == end) + // cur [....[ [..[ + // to insert [....[ [.......[ + // ---------------------------------- + // result [......[ [.......[ + else if (cend >= base && cur->first <= end) { - cur->first -= n; - cur->second += n; - return; + cur->first = base; + if (cend >= end) + return; + // cur->second is set below. } - // ... or insert a new range. - if (cur->first > end) + else if (cur->first > end) + // Insert a new range, unconnected. break; + else + continue; + + // We get here in one of these two situations: + // + // cur [....[ [..[ + // to insert [....[ [.......[ + // ---------------------------------- + // result [......[ [.......[ + // + // cur->first is already set, be cur->second has yet to be. + cur->second = end - cur->first; + // Since we have extended the current range, maybe the next + // items on the list should be merged. + free_list_type::iterator next = cur; + ++next; + while (next != fl.end() && next->first <= end) + { + cur->second = + std::max(next->first + next->second, end) - cur->first; + free_list_type::iterator next2 = next++; + fl.erase(next2); + } + return; } + + // We reach this place either because a new unconnected range + // should be inserted in the middle of FL, or at the end. fl.insert(cur, pos_lenght_pair(base, n)); } + void + free_list::remove(int base, int n) + { + free_list_type::iterator cur; + int end = base + n; + for (cur = fl.begin(); cur != fl.end() && cur->first <= end; ++cur) + { + int cend = cur->first + cur->second; + if (cend >= end) + remove(cur, base, std::max(n, cend - base)); + } + } + + void + free_list::remove(free_list_type::iterator i, int base, int n) + { + if (base == i->first) + { + i->second -= n; + assert(i->second >= 0); + // Erase the range if it's now empty. + if (i->second == 0) + fl.erase(i); + else + i->first += n; + } + else if (base + n == i->first + i->second) + { + i->second -= n; + assert(i->second > 0); // cannot be empty because base != i->first + } + else + { + // Removing in the middle of a range. + int b1 = i->first; + int n1 = base - i->first; + int n2 = i->second - n - base; + assert(n1 > 0); + assert(n2 > 0); + *i = pos_lenght_pair(base + n, n2); + fl.insert(i, pos_lenght_pair(b1, n1)); + } + } + + + void + free_list::release_n(int base, int n) + { + insert(base, n); + } + std::ostream& free_list::dump_free_list(std::ostream& os) const { @@ -115,4 +188,5 @@ namespace spot return os; } + } diff --git a/src/misc/freelist.hh b/src/misc/freelist.hh index a6cb7dcb0..90fa38e74 100644 --- a/src/misc/freelist.hh +++ b/src/misc/freelist.hh @@ -47,6 +47,13 @@ namespace spot /// Dump the list to \a os for debugging. std::ostream& dump_free_list(std::ostream& os) const; + + /// Extend the list by inserting a new pos-lenght pair. + void insert(int base, int n); + + /// Remove \a n consecutive entries from the list, starting at \a base. + void remove(int base, int n = 0); + protected: /// Allocate \a n integer. @@ -62,6 +69,9 @@ namespace spot typedef std::pair pos_lenght_pair; typedef std::list free_list_type; free_list_type fl; ///< Tracks unused BDD variables. + + /// Remove \a n consecutive entries from the list, starting at \a base. + void remove(free_list_type::iterator i, int base, int n); }; } diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 7b8d10a13..8ac4f44ab 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -32,6 +32,7 @@ namespace spot next_to_now(bdd_newpair()), now_to_next(bdd_newpair()) { + free_annonymous_list_of[0] = annon_free_list(this); } bdd_dict::~bdd_dict() @@ -138,6 +139,25 @@ namespace spot } + int + bdd_dict::register_anonymous_variables(int n, const void* for_me) + { + free_annonymous_list_of_type::iterator i = + free_annonymous_list_of.find(for_me); + + if (i == free_annonymous_list_of.end()) + { + typedef free_annonymous_list_of_type fal; + i = (free_annonymous_list_of.insert + (fal::value_type(for_me, free_annonymous_list_of[0]))).first; + } + int res = i->second.register_n(n); + while (n--) + var_refs[res + n].insert(for_me); + return res; + } + + void bdd_dict::register_all_variables_of(const void* from_other, const void* for_me) @@ -149,6 +169,7 @@ namespace spot if (s.find(from_other) != s.end()) s.insert(for_me); } + free_annonymous_list_of[for_me] = free_annonymous_list_of[from_other]; } void @@ -196,10 +217,19 @@ namespace spot else { vi = acc_formula_map.find(var); - f = vi->second; - assert(vi != now_formula_map.end()); - acc_map.erase(f); - acc_formula_map.erase(vi); + if (vi != acc_formula_map.end()) + { + f = vi->second; + acc_map.erase(f); + acc_formula_map.erase(vi); + } + else + { + free_annonymous_list_of_type::iterator i; + for (i = free_annonymous_list_of.begin(); + i != free_annonymous_list_of.end(); ++i) + i->second.remove(var, n); + } } } // Actually release the associated BDD variables, and the @@ -208,6 +238,7 @@ namespace spot ltl::destroy(f); var_refs.erase(cur); } + free_annonymous_list_of.erase(me); } bool @@ -319,4 +350,25 @@ namespace spot dump(std::cerr); assert(0); } + + + bdd_dict::annon_free_list::annon_free_list(bdd_dict* d) + : dict_(d) + { + } + + int + bdd_dict::annon_free_list::extend(int n) + { + assert(dict_); + int b = dict_->allocate_variables(n); + + free_annonymous_list_of_type::iterator i; + for (i = dict_->free_annonymous_list_of.begin(); + i != dict_->free_annonymous_list_of.end(); ++i) + if (&i->second != this) + i->second.insert(b, n); + return b; + } + } diff --git a/src/tgba/bdddict.hh b/src/tgba/bdddict.hh index 09c3d0f94..2b3236f85 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -118,6 +118,15 @@ namespace spot /// automaton). void register_acceptance_variables(bdd f, const void* for_me); + /// \brief Register anonymous BDD variables. + /// + /// Return (and maybe allocate) \a n consecutive BDD variables which + /// will be used only by \a for_me. + /// + /// \return The variable number. Use bdd_ithvar() or bdd_nithvar() + /// to convert this to a BDD. + int register_anonymous_variables(int n, const void* for_me); + /// \brief Duplicate the variable usage of another object. /// /// This tells this dictionary that the \a for_me object @@ -136,7 +145,7 @@ namespace spot bool is_registered_proposition(const ltl::formula* f, const void* by_me); bool is_registered_state(const ltl::formula* f, const void* by_me); bool is_registered_acceptance_variable(const ltl::formula* f, - const void* by_me); + const void* by_me); /// @} /// \brief Dump all variables for debugging. @@ -155,6 +164,24 @@ namespace spot typedef Sgi::hash_map vr_map; vr_map var_refs; + + class annon_free_list : public spot::free_list + { + public: + // WARNING: We need a default constructor so this can be used in + // a hash; but we should ensure that no object in the hash is + // constructed with d==0. + annon_free_list(bdd_dict* d = 0); + virtual int extend(int n); + private: + bdd_dict* dict_; + }; + + /// List of unused anonymous variable number for each automaton. + typedef Sgi::hash_map > free_annonymous_list_of_type; + free_annonymous_list_of_type free_annonymous_list_of; + private: // Disallow copy. bdd_dict(const bdd_dict& other);