* 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

 2006-07-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* 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  <adl@src.lip6.fr>
 	* 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:

src/misc/freelist.cc

-// 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;
+  }
 
 }

src/misc/freelist.hh

-// 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.

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;

src/tgba/bdddict.hh

-// 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<const void*, annon_free_list> free_annonymous_list_of_type;
-    free_annonymous_list_of_type free_annonymous_list_of;
+    typedef std::map<const void*, anon_free_list> free_anonymous_list_of_type;
+    free_anonymous_list_of_type free_anonymous_list_of;
 
   private:
     // Disallow copy.