degen: fix handling of degen-lcache=1

* spot/twaalgos/degen.cc: Here.
* tests/core/degendet.test: Add test case.
* tests/core/ltl2ta.test: Adjust expected output.
* NEWS: Mention the issue.

tests/core/degendet.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2015 Laboratoire de Recherche et Développement
+# Copyright (C) 2011, 2015, 2016 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -23,7 +23,7 @@
 
 set -e
 
-# The following command, reported by Tomáš Babiak, used to output many
+# The following command, reported by Tomáš Babiak, used to output many
 # different automata, because state addresses were used to order the
 # successors in the degeneralization.
 
@@ -36,3 +36,10 @@ for i in 2 3 4 5; do
   ../ikwiad -r7 -x -R3 -N "XF(Gp2 | F(p0 U (p1 & (! p4 | p3))))" > out
   cmp out out1 || exit 1
 done
+
+# The next formula used to be translated into a 6-state automaton
+# instead of a 4-state automaton, because of an error in the
+# implementation of the degen-lcache=1 option causing the last level
+# used to be reused, instead of the first one.
+run 0 ltl2tgba -B -f '(b & Fa) U XXG(a M Gb)' --stats=%s,%t >out
+test "4,14" = "`cat out`"