From 9e97543e33f4227d82158bae6eb812ac89588d15 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Jul 2006 15:30:23 +0000 Subject: [PATCH] * src/tgba/bdddict.cc, src/tgba/bdddict.hh (free_annonymous_list_of): Rename as ... (free_anonymous_list_of): ... this, and correct their update on release. Also correct yesterday's the correction (ahem!). (dump): Improve verbosity. * src/misc/freelist.cc (free_list::remove, free_list::insert): Fix longstanding thinkos. (free_list::free_count): New function. --- ChangeLog | 13 ++++++-- src/misc/freelist.cc | 70 ++++++++++++++++++++++++++++------------- src/misc/freelist.hh | 5 ++- src/tgba/bdddict.cc | 74 ++++++++++++++++++++++++++++++++------------ src/tgba/bdddict.hh | 10 +++--- 5 files changed, 123 insertions(+), 49 deletions(-) diff --git a/ChangeLog b/ChangeLog index 05fe09272..3d79edc1e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,10 +1,19 @@ 2006-07-14 Alexandre Duret-Lutz + * src/tgba/bdddict.cc, src/tgba/bdddict.hh (free_annonymous_list_of): + Rename as ... + (free_anonymous_list_of): ... this, and correct their update on + release. Also correct yesterday's the correction (ahem!). + (dump): Improve verbosity. + * src/misc/freelist.cc (free_list::remove, free_list::insert): Fix + longstanding thinkos. + (free_list::free_count): New function. + Merge this fix from proviso-branch: 2006-05-22 Alexandre Duret-Lutz * src/misc/bddalloc.cc (bdd_allocator::bdd_allocator): Count the - number of BDD variable after they have been allocated. Otherwise - the first bdd_dict() created was leaking BDD variable #1. + number of BDD variable after they have been allocated. Otherwise + the first bdd_dict() created was leaking BDD variable #1. * src/tgba/tgbabddconcrete.hh, src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.hh, src/tgba/tgbareduc.hh, src/tgba/tgbatba.hh: diff --git a/src/misc/freelist.cc b/src/misc/freelist.cc index ef82984bc..d2434f3fc 100644 --- a/src/misc/freelist.cc +++ b/src/misc/freelist.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -73,13 +73,31 @@ namespace spot for (cur = fl.begin(); cur != fl.end(); ++cur) { int cend = cur->first + cur->second; + // cur [...] + // to insert [...] + // ----------------------- + // result [...] [...] + // (Insert a new range, unconnected.) + if (cur->first > end) + { + break; + } + // cur [...] + // to insert [...] + // ----------------------- + // result unknown : we should look at the rest of the freelist. + else if (base > cend) + { + continue; + } // cur [....[ [......[ // to insert [....[ [..[ // ---------------------------------- // result [......[ [......[ - if (cend >= base) + else if (cur->first <= base) { if (cend >= end) + // second case : nothing to do return; // cur->second is set below. } @@ -87,27 +105,21 @@ namespace spot // to insert [....[ [.......[ // ---------------------------------- // result [......[ [.......[ - else if (cend >= base && cur->first <= end) + else { cur->first = base; - if (cend >= end) - return; // cur->second is set below. } - else if (cur->first > end) - // Insert a new range, unconnected. - break; - else - continue; - // We get here in one of these two situations: + // We get here in one of these three situations: // - // cur [....[ [..[ - // to insert [....[ [.......[ - // ---------------------------------- - // result [......[ [.......[ + // cur [....[ [....[ [..[ + // to insert [....[ [....[ [.......[ + // ------------------------------------------- + // result [......[ [......[ [.......[ // // cur->first is already set, be cur->second has yet to be. + end = std::max(cend, end); cur->second = end - cur->first; // Since we have extended the current range, maybe the next // items on the list should be merged. @@ -115,8 +127,8 @@ namespace spot ++next; while (next != fl.end() && next->first <= end) { - cur->second = - std::max(next->first + next->second, end) - cur->first; + end = std::max(next->first + next->second, end); + cur->second = end - cur->first; free_list_type::iterator next2 = next++; fl.erase(next2); } @@ -133,13 +145,17 @@ namespace spot { free_list_type::iterator cur = fl.begin(); int end = base + n; - while (cur != fl.end() && cur->first <= end) + while (cur != fl.end() && cur->first < end) { int cend = cur->first + cur->second; // Remove may invalidate the current iterator, so advance it first. free_list_type::iterator old = cur++; - if (cend >= end) - remove(old, base, std::max(n, cend - base)); + if (cend >= base) + { + int newbase = std::max(base, old->first); + int q = std::min(cend, end) - newbase; + remove(old, newbase, q); + } } } @@ -148,6 +164,7 @@ namespace spot { if (base == i->first) { + // Removing at the beginning of the range i->second -= n; assert(i->second >= 0); // Erase the range if it's now empty. @@ -158,6 +175,7 @@ namespace spot } else if (base + n == i->first + i->second) { + // Removing at the end of the range i->second -= n; assert(i->second > 0); // cannot be empty because base != i->first } @@ -166,7 +184,7 @@ namespace spot // Removing in the middle of a range. int b1 = i->first; int n1 = base - i->first; - int n2 = i->second - n - base; + int n2 = i->first + i->second - base - n; assert(n1 > 0); assert(n2 > 0); *i = pos_lenght_pair(base + n, n2); @@ -174,7 +192,6 @@ namespace spot } } - void free_list::release_n(int base, int n) { @@ -190,5 +207,14 @@ namespace spot return os; } + int + free_list::free_count() const + { + int res = 0; + free_list_type::const_iterator i; + for (i = fl.begin(); i != fl.end(); ++i) + res += i->second; + return res; + } } diff --git a/src/misc/freelist.hh b/src/misc/freelist.hh index 0838bfc5f..6368d9dd8 100644 --- a/src/misc/freelist.hh +++ b/src/misc/freelist.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -55,6 +55,9 @@ namespace spot /// Remove \a n consecutive entries from the list, starting at \a base. void remove(int base, int n = 0); + /// Return the number of free integers on the list. + int free_count() const; + protected: /// Allocate \a n integer. diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index 763ed5f09..c7d51258a 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -33,7 +33,7 @@ namespace spot next_to_now(bdd_newpair()), now_to_next(bdd_newpair()) { - free_annonymous_list_of[0] = annon_free_list(this); + free_anonymous_list_of[0] = anon_free_list(this); } bdd_dict::~bdd_dict() @@ -143,18 +143,20 @@ 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); + free_anonymous_list_of_type::iterator i = + free_anonymous_list_of.find(for_me); - if (i == free_annonymous_list_of.end()) + if (i == free_anonymous_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; + typedef free_anonymous_list_of_type fal; + i = (free_anonymous_list_of.insert + (fal::value_type(for_me, free_anonymous_list_of[0]))).first; } int res = i->second.register_n(n); + while (n--) var_refs[res + n].insert(for_me); + return res; } @@ -170,7 +172,11 @@ 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]; + + free_anonymous_list_of_type::const_iterator j = + free_anonymous_list_of.find(from_other); + if (j != free_anonymous_list_of.end()) + free_anonymous_list_of[for_me] = j->second; } void @@ -188,14 +194,23 @@ namespace spot 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 (!s.empty()) return; // ME was the last user of this variable. // Let's free it. First, we need to find // if this is a Now, a Var, or an Acc variable. - int var = cur->first; int n = 1; const ltl::formula* f = 0; vf_map::iterator vi = var_formula_map.find(var); @@ -228,10 +243,13 @@ namespace spot } else { - free_annonymous_list_of_type::iterator i; - for (i = free_annonymous_list_of.begin(); - i != free_annonymous_list_of.end(); ++i) - i->second.release_n(var, n); + 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); } } } @@ -254,7 +272,7 @@ namespace spot vr_map::iterator cur = i++; unregister_variable(cur, me); } - free_annonymous_list_of.erase(me); + free_anonymous_list_of.erase(me); } bool @@ -315,6 +333,24 @@ namespace spot << 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; + free_anonymous_list_of_type::const_iterator ai; + for (ai = free_anonymous_list_of.begin(); + ai != free_anonymous_list_of.end(); ++ai) + { + os << " [" << ai->first << "] "; + ai->second.dump_free_list(os) << std::endl; + } os << "Free list:" << std::endl; dump_free_list(os); os << std::endl; @@ -368,20 +404,20 @@ namespace spot } - bdd_dict::annon_free_list::annon_free_list(bdd_dict* d) + bdd_dict::anon_free_list::anon_free_list(bdd_dict* d) : dict_(d) { } int - bdd_dict::annon_free_list::extend(int n) + bdd_dict::anon_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) + free_anonymous_list_of_type::iterator i; + for (i = dict_->free_anonymous_list_of.begin(); + i != dict_->free_anonymous_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 1d79c31fa..43ac4670c 100644 --- a/src/tgba/bdddict.hh +++ b/src/tgba/bdddict.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -172,13 +172,13 @@ namespace spot // SWIG does not grok the following definition, no idea why. // It's not important for the Python interface anyway. #ifndef SWIG - class annon_free_list : public spot::free_list + class anon_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); + anon_free_list(bdd_dict* d = 0); virtual int extend(int n); private: bdd_dict* dict_; @@ -186,8 +186,8 @@ namespace spot #endif /// List of unused anonymous variable number for each automaton. - typedef std::map free_annonymous_list_of_type; - free_annonymous_list_of_type free_annonymous_list_of; + typedef std::map free_anonymous_list_of_type; + free_anonymous_list_of_type free_anonymous_list_of; private: // Disallow copy.