alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/misc/freelist.hh (free_list::remove, free_list::insert): New

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2004-03-23 09:39:38 +00:00
parent aba2dc75d7
commit 784ccafb1b
5 changed files with 213 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

17
ChangeLog
View file

@ -1,5 +1,22 @@
2004-03-23 Alexandre DURET-LUTZ <adl@src.lip6.fr>
* 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.

126
src/misc/freelist.cc
View file

@ -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.
if (cend >= end)
return;
// cur->second is set below.
}
// cur [....[ [..[
// to insert [....[ [.......[
// ----------------------------------
// result [......[ [.......[
else if (cend >= base && cur->first <= end)
{
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:
//
// 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;
if (next != fl.end() && next->first == end)
while (next != fl.end() && next->first <= end)
{
cur->second += next->second;
fl.erase(next);
cur->second =
std::max(next->first + next->second, end) - cur->first;
free_list_type::iterator next2 = next++;
fl.erase(next2);
}
return;
}
// ... or prepend to a range ...
if (cur->first == end)
{
cur->first -= n;
cur->second += n;
return;
}
// ... or insert a new range.
if (cur->first > end)
break;
}
// 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;
}
}

10
src/misc/freelist.hh
View file

@ -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<int, int> pos_lenght_pair;
typedef std::list<pos_lenght_pair> 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);
};
}

54
src/tgba/bdddict.cc
View file

@ -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,11 +217,20 @@ namespace spot
else
{
vi = acc_formula_map.find(var);
if (vi != acc_formula_map.end())
{
f = vi->second;
assert(vi != now_formula_map.end());
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
// formula itself.
@ -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;
}
}

29
src/tgba/bdddict.hh
View file

@ -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
@ -155,6 +164,24 @@ namespace spot
typedef Sgi::hash_map<int, ref_set> 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<const void*, annon_free_list,
ptr_hash<void> > free_annonymous_list_of_type;
free_annonymous_list_of_type free_annonymous_list_of;
private:
// Disallow copy.
bdd_dict(const bdd_dict& other);