From dd16f58ef4ac616a2eef71d676d717600b86e474 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 30 Sep 2012 15:19:05 +0200
Subject: [PATCH] enumerate_cycles: fix memory management.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* src/tgbaalgos/cycles.cc (tag_state): Destroy duplicate states, not
new states!
* src/tgbatest/cycles.test: Add a test case that used to segfault.
Reported by Étienne Renault.
---
 src/tgbaalgos/cycles.cc  |  2 +-
 src/tgbatest/cycles.test | 16 +++++-----------
 2 files changed, 6 insertions(+), 12 deletions(-)

diff --git a/src/tgbaalgos/cycles.cc b/src/tgbaalgos/cycles.cc
index 907e3e636..351103815 100644
--- a/src/tgbaalgos/cycles.cc
+++ b/src/tgbaalgos/cycles.cc
@@ -71,7 +71,7 @@ namespace spot
   {
     std::pair<tagged_state, bool> p =
       tags_.insert(std::make_pair(s, state_info()));
-    if (p.second)
+    if (!p.second)
       s->destroy();
     return p.first;
   }
diff --git a/src/tgbatest/cycles.test b/src/tgbatest/cycles.test
index 8a51cc031..5c479bca8 100755
--- a/src/tgbatest/cycles.test
+++ b/src/tgbatest/cycles.test
@@ -19,20 +19,12 @@
 # Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
 # 02111-1307, USA.
 
-# While running some benchmark, Tomáš Babiak found that Spot took too
-# much time (i.e. >1h) to translate those six formulae.  It turns out
-# that the WDBA minimization was performed after the degeneralization
-# algorithm, while this is not necessary (WDBA will produce a BA, so
-# we may as well skip degeneralization).  Translating these formulae
-# in the test-suite ensure that they don't take too much time (the
-# buildfarm will timeout if it does).
-
 . ./defs
-
 set -e
 
 # GNU systems have seq,
 # BSD systems have jot.
+# Neither of those are POSIX...
 if test "*`(seq 1 1 2>/dev/null)`" = "1"; then
   have_seq=true
 else
@@ -89,8 +81,10 @@ echo "s$x,s$w,,;"
 run 0 ../ltl2tgba -KC -X johnson-fig1.tgba > out
 test `wc -l < out` -eq 10
 
-
-
 run 0 ../ltl2tgba -KW '(Ga -> Gb) W c' > out
 test `grep 'is weak' out | wc -l` -eq 4
 test `grep 'is not weak' out | wc -l` -eq 1
+
+run 0 ../ltl2tgba -l -KW 'F(Fa R (Gb & !a))' > out
+test `grep 'is weak' out | wc -l` -eq 7
+test `grep 'is not weak' out | wc -l` -eq 1