From 7d8a5310e4b831fd0e1cd07c27aaa8d8dcd475a4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 25 Nov 2010 12:58:33 +0100
Subject: [PATCH] Fix bugs in minimize().

* src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory
leaks and a usage of the wrong automaton.
* src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with
valgrind.  This caught all the bugs fixed above.
---
 ChangeLog                 |  9 +++++++++
 src/tgbaalgos/minimize.cc | 29 +++++++++++++++++++++++++----
 src/tgbatest/wdba.test    | 10 ++++++++++
 3 files changed, 44 insertions(+), 4 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 5250db7dc..a125f28f5 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,12 @@
+2010-11-25  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Fix bugs in minimize().
+
+	* src/tgbaalgos/minimize.cc (init_sets, minimize): Fix memory
+	leaks and a usage of the wrong automaton.
+	* src/tgbatest/wdba.test: Try using -Rm with -R3 or -R3b, and with
+	valgrind.  This caught all the bugs fixed above.
+
 2010-04-13  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Fix bugs in minimize(), caught by spotlbtt.test.
diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc
index f986d17dc..b9b146eaa 100644
--- a/src/tgbaalgos/minimize.cc
+++ b/src/tgbaalgos/minimize.cc
@@ -49,8 +49,8 @@ namespace spot
       tovisit.pop();
       // Is the state final ?
       if (final.find(src) == final.end())
-        // No, add it to the set non_final
-        non_final.insert(src);
+	// No, add it to the set non_final
+	non_final.insert(src->clone());
       tgba_succ_iterator* sit = a->succ_iter(src);
       for (sit->first(); !sit->done(); sit->next())
       {
@@ -67,6 +67,15 @@ namespace spot
       }
       delete sit;
     }
+
+    while (!seen.empty())
+      {
+	hash_set::iterator i = seen.begin();
+	const state* s = *i;
+	seen.erase(i);
+	delete s;
+      }
+
   }
 
   // From the base automaton and the list of sets, build the minimal
@@ -154,6 +163,8 @@ namespace spot
       free_var.insert(i);
     std::map<int, int> used_var;
 
+    hash_set* final_copy;
+
     if (!final->empty())
       {
 	unsigned s = final->size();
@@ -166,7 +177,14 @@ namespace spot
 	for (hash_set::const_iterator i = final->begin();
 	     i != final->end(); ++i)
 	  state_set_map[*i] = set_num;
+
+	final_copy = new hash_set(*final);
       }
+    else
+      {
+	final_copy = final;
+      }
+
     if (!non_final->empty())
       {
 	unsigned s = non_final->size();
@@ -181,8 +199,11 @@ namespace spot
 	     i != non_final->end(); ++i)
 	  state_set_map[*i] = num;
       }
+    else
+      {
+	delete non_final;
+      }
 
-    hash_set* final_copy = new hash_set(*final);
     // A bdd_states_map is a list of formulae (in a BDD form) associated with a
     // destination set of states.
     typedef std::list<std::pair<bdd, hash_set*> > bdd_states_map;
@@ -198,7 +219,7 @@ namespace spot
       {
         const state* src = *hi;
         bdd f = bddfalse;
-        tgba_succ_iterator* si = a->succ_iter(src);
+        tgba_succ_iterator* si = det_a->succ_iter(src);
         for (si->first(); !si->done(); si->next())
         {
           const state* dst = si->current_state();
diff --git a/src/tgbatest/wdba.test b/src/tgbatest/wdba.test
index a78a2bab7..68b102e8c 100755
--- a/src/tgbatest/wdba.test
+++ b/src/tgbatest/wdba.test
@@ -87,6 +87,11 @@ EOF
 
 success=:
 while read f; do
+  # Run ltl2tgba through valgrind with some combination of options to
+  # detect any crash
+  run 0 ../ltl2tgba -f -R3 -DS -Rm "!($f)" >/dev/null
+  run 0 ../ltl2tgba -l -R3b -DS -Rm "!($f)" >/dev/null
+
   # If the labels of the state have only digits, assume the minimization
   # worked.
   x=`../ltl2tgba -f -Rm "!($f)" |
@@ -102,6 +107,11 @@ done < obligations.txt
 echo ====
 
 while read f; do
+  # Run ltl2tgba through valgrind with some combination of options to
+  # detect any crash
+  run 0 ../ltl2tgba -f -R3 -DS -Rm "!($f)" >/dev/null
+  run 0 ../ltl2tgba -l -R3b -DS -Rm "!($f)" >/dev/null
+
   # If the labels of the state have only digits, assume the minimization
   # worked.
   x=`../ltl2tgba -f -Rm "!($f)" |