From db02e7c3d0cf4034b52139e05bd422a0092d3a76 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 17 Oct 2013 04:08:30 +0200
Subject: [PATCH 01/13] postproc: Add a degen-lskip option.

Also generalize the degen-lcache option.

* src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh: Add the option.
* src/bin/spot-x.cc: Document it.
* src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh: Implement it.
* src/tgbatest/ltlcross2.test: Add a test configuration.
* src/tgbatest/degenlskip.test: New file.
* src/tgbatest/Makefile.am (TESTS): Add degenlskip.test.
---
 src/bin/spot-x.cc            | 15 ++++++--
 src/tgbaalgos/degen.cc       | 69 ++++++++++++++++++++++++++---------
 src/tgbaalgos/degen.hh       |  9 +++--
 src/tgbaalgos/postproc.cc    | 14 ++++----
 src/tgbaalgos/postproc.hh    |  7 ++--
 src/tgbatest/Makefile.am     | 10 +++---
 src/tgbatest/degenlskip.test | 70 ++++++++++++++++++++++++++++++++++++
 src/tgbatest/ltlcross2.test  |  1 +
 8 files changed, 159 insertions(+), 36 deletions(-)
 create mode 100755 src/tgbatest/degenlskip.test

diff --git a/src/bin/spot-x.cc b/src/bin/spot-x.cc
index 3be50e8e6..7a1ab2a2f 100644
--- a/src/bin/spot-x.cc
+++ b/src/bin/spot-x.cc
@@ -1,6 +1,5 @@
-
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -70,10 +69,20 @@ a non-accepting SCC.") },
     { DOC("degen-lcache", "If non-zero (the default), whenever the \
 degeneralization algorithm enters an SCC on a state that has already \
 been associated to a level elsewhere, it should reuse that level. \
-The \"lcache\" stands for \"level cache\".") },
+Different values can be used to select which level to reuse: 1 always \
+uses the first level seen, 2 uses the minimum level seen so far, and \
+3 uses the maximum level seen so far. The \"lcache\" stands for \
+\"level cache\".") },
     { DOC("degen-order", "If non-zero, the degeneralization algorithm \
 will compute one degeneralization order for each SCC it processes. \
 This is currently disabled by default.") },
+    { DOC("degen-lskip", "If non-zero (the default), the degeneralization \
+algorithm will skip as much levels as possible for each transition.  This \
+is enabled by default as it very often reduce the number of resulting \
+states.  A consequence of skipping levels is that the degeneralized \
+automaton tends to have smaller cycles around the accepting states.  \
+Disabling skipping will produce automata with large cycles, and often \
+with more states.") },
     { DOC("simul", "Set to 0 to disable simulation-based reductions. \
 Set to 1 to use only direct simulation. Set to 2 to use only reverse \
 simulation. Set to 3 to iterate both direct and reverse simulations. \
diff --git a/src/tgbaalgos/degen.cc b/src/tgbaalgos/degen.cc
index a7e3e4760..0da2f5190 100644
--- a/src/tgbaalgos/degen.cc
+++ b/src/tgbaalgos/degen.cc
@@ -1,5 +1,6 @@
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita.
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita.
 //
 // This file is part of Spot, a model checking library.
 //
@@ -24,6 +25,7 @@
 #include "ltlast/constant.hh"
 #include <deque>
 #include <vector>
+#include <algorithm>
 #include "tgbaalgos/scc.hh"
 #include "tgba/bddprint.hh"
 
@@ -217,7 +219,7 @@ namespace spot
 
     public:
       unsigned
-      next_level(bdd all, int slevel, bdd acc)
+      next_level(bdd all, int slevel, bdd acc, bool skip_levels)
       {
         bdd temp = acc;
         if (all != found_)
@@ -243,7 +245,11 @@ namespace spot
         acc = temp;
         unsigned next = slevel;
         while (next < order_.size() && bdd_implies(order_[next], acc))
-          ++next;
+	  {
+	    ++next;
+	    if (!skip_levels)
+	      break;
+	  }
         return next;
       }
 
@@ -266,16 +272,18 @@ namespace spot
     {
       bdd all_;
       std::map<int, acc_order> orders_;
+      bool skip_levels_;
 
     public:
-      scc_orders(bdd all): all_(all)
+      scc_orders(bdd all, bool skip_levels):
+	all_(all), skip_levels_(skip_levels)
       {
       }
 
       unsigned
       next_level(int scc, int slevel, bdd acc)
       {
-        return orders_[scc].next_level(all_, slevel, acc);
+        return orders_[scc].next_level(all_, slevel, acc, skip_levels_);
       }
 
       void
@@ -290,7 +298,7 @@ namespace spot
 
   sba*
   degeneralize(const tgba* a, bool use_z_lvl, bool use_cust_acc_orders,
-               bool use_lvl_cache)
+               int use_lvl_cache, bool skip_levels)
   {
     bool use_scc = use_lvl_cache || use_cust_acc_orders || use_z_lvl;
 
@@ -333,7 +341,7 @@ namespace spot
     }
 
     // Initialize scc_orders
-    scc_orders orders(a->all_acceptance_conditions());
+    scc_orders orders(a->all_acceptance_conditions(), skip_levels);
 
     // Make sure we always use the same pointer for identical states
     // from the input automaton.
@@ -355,7 +363,7 @@ namespace spot
     tr_cache_t tr_cache;
 
     // State level cache
-    typedef std::map<const state*, int> lvl_cache_t;
+    typedef std::map<const state*, unsigned> lvl_cache_t;
     lvl_cache_t lvl_cache;
 
     // Compute SCCs in order to use any optimization.
@@ -385,7 +393,11 @@ namespace spot
 	  s.second = orders.next_level(m.initial(), s.second, acc);
 	else
 	  while (s.second < order.size() && bdd_implies(order[s.second], acc))
-	    ++s.second;
+	    {
+	      ++s.second;
+	      if (!skip_levels)
+		break;
+	    }
       }
 
 #ifdef DEGEN_DEBUG
@@ -523,7 +535,8 @@ namespace spot
             // }
             if (is_scc_acc)
               {
-                // If lvl_cache is used and switching SCCs, use level from cache
+                // If lvl_cache is used and switching SCCs, use level
+                // from cache
                 if (use_lvl_cache && s_scc != scc
 		    && lvl_cache.find(d.first) != lvl_cache.end())
                   {
@@ -564,10 +577,17 @@ namespace spot
 			    // Consider both the current acceptance
 			    // sets, and the acceptance sets common to
 			    // the outgoing transitions of the
-			    // destination state.
-			    while (next < order.size()
-				   && bdd_implies(order[next], acc))
-			      ++next;
+			    // destination state.  But don't do
+			    // that if the state is accepting and we
+			    // are not skipping levels.
+			    if (skip_levels || !is_acc)
+			      while (next < order.size()
+				     && bdd_implies(order[next], acc))
+				{
+				  ++next;
+				  if (!skip_levels)
+				    break;
+				}
 			    d.second = next;
 			  }
                       }
@@ -591,8 +611,23 @@ namespace spot
                 ds2num[d] = dest;
                 todo.push_back(d);
                 // Insert new state to cache
-                if (use_lvl_cache && lvl_cache.find(d.first) == lvl_cache.end())
-                  lvl_cache[d.first] = d.second;
+
+		if (use_lvl_cache)
+		  {
+		    std::pair<lvl_cache_t::iterator, bool> res =
+		      lvl_cache.insert(lvl_cache_t::value_type(d.first,
+							       d.second));
+
+		    if (!res.second)
+		      {
+			if (use_lvl_cache == 3)
+			  res.first->second =
+			    std::max(res.first->second, d.second);
+			else if (use_lvl_cache == 2)
+			  res.first->second =
+			    std::min(res.first->second, d.second);
+		      }
+		  }
               }
 
             state_explicit_number::transition*& t =
diff --git a/src/tgbaalgos/degen.hh b/src/tgbaalgos/degen.hh
index f3354cac2..c67528bed 100644
--- a/src/tgbaalgos/degen.hh
+++ b/src/tgbaalgos/degen.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -44,7 +44,9 @@ namespace spot
   /// default because our benchmarks show that it usually does more
   /// harm than good).  If \a use_lvl_cache is set, everytime an SCC
   /// is entered on a state that as already been associated to some
-  /// level elsewhere, reuse that level).
+  /// level elsewhere, reuse that level (set it to 2 to keep the
+  /// smallest number, 3 to keep the largest level, and 1 to keep the
+  /// first level found).
   ///
   /// Any of these three options will cause the SCCs of the automaton
   /// \a a to be computed prior to its actual degeneralization.
@@ -53,7 +55,8 @@ namespace spot
   SPOT_API sba*
   degeneralize(const tgba* a, bool use_z_lvl = true,
 	       bool use_cust_acc_orders = false,
-	       bool use_lvl_cache = true);
+	       int use_lvl_cache = 1,
+	       bool skip_levels = true);
 }
 
 
diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc
index 0c2be1410..e7d6e6d3c 100644
--- a/src/tgbaalgos/postproc.cc
+++ b/src/tgbaalgos/postproc.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -39,15 +39,16 @@ namespace spot
   postprocessor::postprocessor(const option_map* opt)
     : type_(TGBA), pref_(Small), level_(High),
       degen_reset_(true), degen_order_(false), degen_cache_(true),
-      simul_(-1), scc_filter_(-1), ba_simul_(-1), tba_determinisation_(false),
-      sat_minimize_(0), sat_acc_(0), sat_states_(0), state_based_(false),
-      wdba_minimize_(true)
+      degen_lskip_(true), simul_(-1), scc_filter_(-1), ba_simul_(-1),
+      tba_determinisation_(false), sat_minimize_(0), sat_acc_(0),
+      sat_states_(0), state_based_(false), wdba_minimize_(true)
   {
     if (opt)
       {
 	degen_order_ = opt->get("degen-order", 0);
 	degen_reset_ = opt->get("degen-reset", 1);
 	degen_cache_ = opt->get("degen-lcache", 1);
+	degen_lskip_ = opt->get("degen-lskip", 1);
 	simul_ = opt->get("simul", -1);
 	simul_limit_ = opt->get("simul-limit", -1);
 	scc_filter_ = opt->get("scc-filter", -1);
@@ -116,7 +117,8 @@ namespace spot
     const tgba* d = degeneralize(a,
 				 degen_reset_,
 				 degen_order_,
-				 degen_cache_);
+				 degen_cache_,
+				 degen_lskip_);
     delete a;
     if (ba_simul_ <= 0)
       return d;
diff --git a/src/tgbaalgos/postproc.hh b/src/tgbaalgos/postproc.hh
index 693089b42..52b812ec0 100644
--- a/src/tgbaalgos/postproc.hh
+++ b/src/tgbaalgos/postproc.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -110,7 +110,8 @@ namespace spot
     // Fine-tuning options fetched from the option_map.
     bool degen_reset_;
     bool degen_order_;
-    bool degen_cache_;
+    int degen_cache_;
+    bool degen_lskip_;
     int simul_;
     int simul_limit_;
     int scc_filter_;
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 7866d0060..7e2e674d9 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -1,8 +1,9 @@
-## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-## D�veloppement de l'Epita (LRDE).
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
+## Développement de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
-## Paris 6 (LIP6), d�partement Syst�mes R�partis Coop�ratifs (SRC),
-## Universit� Pierre et Marie Curie.
+## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+## Université Pierre et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -106,6 +107,7 @@ TESTS = \
   dupexp.test \
   degendet.test \
   degenid.test \
+  degenlskip.test \
   kv.test \
   lbttparse.test \
   scc.test \
diff --git a/src/tgbatest/degenlskip.test b/src/tgbatest/degenlskip.test
new file mode 100755
index 000000000..3836d2cb5
--- /dev/null
+++ b/src/tgbatest/degenlskip.test
@@ -0,0 +1,70 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
+# de l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+
+# Make sure degen-skip=0 and degen-skip=1 produce the expected
+# automata for 'GFa & GFb'
+
+../../bin/ltl2tgba -B 'GFa & GFb' > out1
+../../bin/ltl2tgba -B -x degen-lskip=1 'GFa & GFb' > out2
+../../bin/ltl2tgba -B -x degen-lskip=0 'GFa & GFb' > out3
+
+diff out1 out2
+cmp out2 out3 && exit 1
+
+cat <<EOF >expected2
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0", peripheries=2]
+  1 -> 1 [label="a & b\n{Acc[1]}"]
+  1 -> 2 [label="!a & b\n{Acc[1]}"]
+  1 -> 3 [label="!b\n{Acc[1]}"]
+  2 [label="1"]
+  2 -> 1 [label="a\n"]
+  2 -> 2 [label="!a\n"]
+  3 [label="2"]
+  3 -> 1 [label="a & b\n"]
+  3 -> 2 [label="!a & b\n"]
+  3 -> 3 [label="!b\n"]
+}
+EOF
+
+
+cat <<EOF >expected3
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0", peripheries=2]
+  1 -> 2 [label="1\n{Acc[1]}"]
+  2 [label="1"]
+  2 -> 3 [label="b\n"]
+  2 -> 2 [label="!b\n"]
+  3 [label="2"]
+  3 -> 1 [label="a\n"]
+  3 -> 3 [label="!a\n"]
+}
+EOF
+
+diff out2 expected2
+diff out3 expected3
diff --git a/src/tgbatest/ltlcross2.test b/src/tgbatest/ltlcross2.test
index b21e589d0..6150ac722 100755
--- a/src/tgbatest/ltlcross2.test
+++ b/src/tgbatest/ltlcross2.test
@@ -38,6 +38,7 @@ ltl2tgba=../../bin/ltl2tgba
 "$ltl2tgba --lbtt -x comp-susp,!skel-wdba --lbtt --small %f >%T" \
 "$ltl2tgba --lbtt -x comp-susp,early-susp --lbtt --small %f >%T" \
 "$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --lbtt --small %f >%T" \
+"$ltl2tgba --lbtt --ba -x degen-skip=0 --lbtt %f >%T" \
 "$ltl2tgba --lbtt --ba --high %f > %T" \
 "$ltl2tgba --lbtt -BDC %f > %T" \
 "$ltl2tgba --lbtt -BC %f > %T" \

From f5914647aa3901c8a56d130073c281c0ee892419 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 26 Feb 2014 16:33:57 +0100
Subject: [PATCH 02/13] * src/dstarparse/nra2nba.cc: Fix comment.

---
 src/dstarparse/nra2nba.cc | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/dstarparse/nra2nba.cc b/src/dstarparse/nra2nba.cc
index f4472dc5c..06ef6cdd0 100644
--- a/src/dstarparse/nra2nba.cc
+++ b/src/dstarparse/nra2nba.cc
@@ -1,4 +1,5 @@
-// Copyright (C) 2013 Laboratoire de Recherche et Développement de
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -29,9 +30,9 @@ namespace spot
     // Transformation of ω-Automata: Complexity and Connection to
     // Second Order Logic.  Section 3.4.3: Rabin to Büchi.
     //
-    // However beware that the {...,(Ei,Fi),...} pairs used by
-    // are the reversed compared to the {...,(Li,Ui),...} pairs
-    // used by several other people.  We have Ei=Ui and Fi=Li.
+    // However beware that the {...,(Ei,Fi),...} pairs used by Löding
+    // are reversed compared to the {...,(Li,Ui),...} pairs used by
+    // several other people.  We have Ei=Ui and Fi=Li.
     class nra_to_nba_worker: public tgba_reachable_iterator_depth_first
     {
     public:

From ae62265ec8906d671b4de83cac615cdbb6d218d8 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 3 Apr 2014 17:14:09 +0200
Subject: [PATCH 03/13] Adjust to Swig 3.0.

* wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py: Use
Boolean instead of integers.
---
 wrap/python/tests/ltl2tgba.py | 6 +++---
 wrap/python/tests/ltlparse.py | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/wrap/python/tests/ltl2tgba.py b/wrap/python/tests/ltl2tgba.py
index a1dc464d4..bf46d43e2 100755
--- a/wrap/python/tests/ltl2tgba.py
+++ b/wrap/python/tests/ltl2tgba.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -51,7 +51,7 @@ except getopt.GetoptError:
     usage(prog)
 
 exit_code = 0
-debug_opt = 0
+debug_opt = False
 degeneralize_opt = None
 output = 0
 fm_opt = 0
@@ -62,7 +62,7 @@ for o, a in opts:
     elif o == '-A':
         output = 4
     elif o == '-d':
-        debug_opt = 1
+        debug_opt = True
     elif o == '-D':
         degeneralize_opt = 1
     elif o == '-f':
diff --git a/wrap/python/tests/ltlparse.py b/wrap/python/tests/ltlparse.py
index f972432ee..a97c74b81 100755
--- a/wrap/python/tests/ltlparse.py
+++ b/wrap/python/tests/ltlparse.py
@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 # 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.
@@ -29,7 +29,7 @@ p = spot.empty_parse_error_list()
 l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \/ a \/ b \/ a \/ a'];
 
 for str1 in l:
-    f = spot.parse(str1, p, e, 0)
+    f = spot.parse(str1, p, e, False)
     if spot.format_parse_errors(spot.get_cout(), str1, p):
         sys.exit(1)
     str2 = str(f)

From c4307e21ae20cff4a5e41fc3862d39d6246b60da Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Apr 2014 14:59:53 +0200
Subject: [PATCH 04/13] * NEWS: Mention recent changes.

---
 NEWS | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index 2ab30a083..e53749d6c 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,16 @@
 New in spot 1.2.3a (not yet released)
 
-  Nothing yet.
+  * New features:
+
+    - "-B -x degen-lskip" can be used to disable level-skipping in the
+      degeralization procedure.  This is mostly meant for running
+      experiments.
+    - "-B -x degen-lcache=N" can be used to experiment with different
+      type of level caching during degeneralization.
+
+  * Bug fixes:
+
+    - Change the Python bindings to make them compatible with Swig 3.0.
 
 New in spot 1.2.3 (2014-02-11)
 

From a5b6865c0b1eb84e936a8ce2a6ca3679472088af Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 7 Apr 2014 17:39:21 +0200
Subject: [PATCH 05/13] ltl2ta: fix a crash with --ta.

* src/taalgos/tgba2ta.cc: Do not assume the input is an sba.
* src/tgbatest/ltl2ta2.test: New file.
* src/tgbatest/Makefile.am: Add it.
* NEWS: Mention the fix.
---
 NEWS                      |  3 ++
 src/taalgos/tgba2ta.cc    | 63 ++++++++++++++++++---------------------
 src/tgbatest/Makefile.am  |  1 +
 src/tgbatest/ltl2ta2.test | 27 +++++++++++++++++
 4 files changed, 60 insertions(+), 34 deletions(-)
 create mode 100755 src/tgbatest/ltl2ta2.test

diff --git a/NEWS b/NEWS
index e53749d6c..b4fcd0617 100644
--- a/NEWS
+++ b/NEWS
@@ -11,6 +11,9 @@ New in spot 1.2.3a (not yet released)
   * Bug fixes:
 
     - Change the Python bindings to make them compatible with Swig 3.0.
+    - "ltl2tgta --ta" could crash in certain conditions due to the
+      introduction of a simulation-based reduction after
+      degeneralization.
 
 New in spot 1.2.3 (2014-02-11)
 
diff --git a/src/taalgos/tgba2ta.cc b/src/taalgos/tgba2ta.cc
index fb619caf4..d326f7dd6 100644
--- a/src/taalgos/tgba2ta.cc
+++ b/src/taalgos/tgba2ta.cc
@@ -1,6 +1,6 @@
 // -*- coding utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -431,35 +431,31 @@ namespace spot
 
       std::stack<state_ta_explicit*> todo;
       const tgba* tgba_ = ta->get_tgba();
-      const sba* sba_ = down_cast<const sba*>(tgba_);
-      assert(!degeneralized || sba_);
 
       // build Initial states set:
       state* tgba_init_state = tgba_->get_init_state();
 
       bdd tgba_condition = tgba_->support_conditions(tgba_init_state);
 
+      bool is_acc = false;
+      if (degeneralized)
+	{
+	  tgba_succ_iterator* it = tgba_->succ_iter(tgba_init_state);
+	  it->first();
+	  if (!it->done())
+	    is_acc = it->current_acceptance_conditions() != bddfalse;
+	  delete it;
+	}
+
       bdd satone_tgba_condition;
       while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
 						    atomic_propositions_set_,
 						    bddtrue)) != bddfalse)
 	{
 	  tgba_condition -= satone_tgba_condition;
-	  state_ta_explicit* init_state;
-	  if (degeneralized)
-	    {
-	      init_state = new
-		state_ta_explicit(tgba_init_state->clone(),
-				  satone_tgba_condition, true,
-				  sba_->state_is_accepting(tgba_init_state));
-	    }
-	  else
-	    {
-	      init_state = new
-		state_ta_explicit(tgba_init_state->clone(),
-				  satone_tgba_condition, true, false);
-	    }
-
+	  state_ta_explicit* init_state = new
+	    state_ta_explicit(tgba_init_state->clone(),
+			      satone_tgba_condition, true, is_acc);
 	  state_ta_explicit* s = ta->add_state(init_state);
 	  assert(s == init_state);
 	  ta->add_to_initial_states_set(s);
@@ -492,6 +488,17 @@ namespace spot
 
 		  bdd all_props = bddtrue;
 		  bdd dest_condition;
+
+		  bool is_acc = false;
+		  if (degeneralized)
+		  {
+		    tgba_succ_iterator* it = tgba_->succ_iter(tgba_state);
+		    it->first();
+		    if (!it->done())
+		      is_acc = it->current_acceptance_conditions() != bddfalse;
+		    delete it;
+		  }
+
 		  if (satone_tgba_condition == source->get_tgba_condition())
 		    while ((dest_condition =
 			    bdd_satoneset(all_props,
@@ -499,21 +506,9 @@ namespace spot
 			   != bddfalse)
 		      {
 			all_props -= dest_condition;
-			state_ta_explicit* new_dest;
-			if (degeneralized)
-			  {
-			    new_dest = new state_ta_explicit
-			      (tgba_state->clone(),
-			       dest_condition,
-			       false,
-			       sba_->state_is_accepting(tgba_state));
-			  }
-			else
-			  {
-			    new_dest = new state_ta_explicit
-			      (tgba_state->clone(),
-			       dest_condition, false, false);
-			  }
+			state_ta_explicit* new_dest =
+			  new state_ta_explicit(tgba_state->clone(),
+						dest_condition, false, is_acc);
 			state_ta_explicit* dest = ta->add_state(new_dest);
 
 			if (dest != new_dest)
diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am
index 7e2e674d9..e9fff81f8 100644
--- a/src/tgbatest/Makefile.am
+++ b/src/tgbatest/Makefile.am
@@ -96,6 +96,7 @@ TESTS = \
   ltl2neverclaim.test \
   ltl2neverclaim-lbtt.test \
   ltl2ta.test \
+  ltl2ta2.test \
   ltlprod.test \
   bddprod.test \
   explprod.test \
diff --git a/src/tgbatest/ltl2ta2.test b/src/tgbatest/ltl2ta2.test
new file mode 100755
index 000000000..eed0c9739
--- /dev/null
+++ b/src/tgbatest/ltl2ta2.test
@@ -0,0 +1,27 @@
+#!/bin/sh
+# Copyright (C) 2014 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+
+. ./defs
+
+set -e
+
+# This used to trigger an assert because of BA simulation not
+# returning an instance of spot::sba.
+run 0 ../../bin/ltl2tgta --ta 'G(F(a U b) U (c M d))'

From 34fd27a38126a084972ca5e310821fb8a8f0c8f6 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 11 Apr 2014 11:37:25 +0200
Subject: [PATCH 06/13] * AUTHORS: Fix So[u]heib's name at his request.

---
 AUTHORS | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/AUTHORS b/AUTHORS
index 73d749b2b..6a485edb2 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -12,7 +12,7 @@ Guillaume Sadegh
 Heikki Tauriainen
 Pierre Parutto
 Rachid Rebiha
-Soheib Baarir
+Souheib Baarir
 Thomas Badie
 Thomas Martinez
 Tomáš Babiak

From 48471b51147f777fe35f4c005b32a2b90dfe903d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 13 May 2014 16:59:51 +0200
Subject: [PATCH 07/13] simplify: fix 3 incorrect simplification rules

* src/ltlvisit/simplify.cc: Remove two incorrect rules, and
partially disable another one.
* doc/tl/tl.tex: Reflect the change.
* src/ltltest/reduccmp.test: Likewise.
* src/ltltest/equals.cc: Add safety checks to catch such errors in the
future.
* NEWS: Mention the bug.
---
 NEWS                      |   3 +
 doc/tl/tl.tex             |  10 ++--
 src/ltltest/equals.cc     |  39 ++++++++++--
 src/ltltest/reduccmp.test |  11 ++--
 src/ltlvisit/simplify.cc  | 121 +++++---------------------------------
 5 files changed, 61 insertions(+), 123 deletions(-)

diff --git a/NEWS b/NEWS
index b4fcd0617..3509f9e3c 100644
--- a/NEWS
+++ b/NEWS
@@ -14,6 +14,9 @@ New in spot 1.2.3a (not yet released)
     - "ltl2tgta --ta" could crash in certain conditions due to the
       introduction of a simulation-based reduction after
       degeneralization.
+    - Fix three incorrect simplifications rules, all related to the
+      factorization of Boolean subformulas in operands of the
+      non-length-matching "&" SERE operator.
 
 New in spot 1.2.3 (2014-02-11)
 
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 6c1c5d79e..18d89f1f8 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1460,13 +1460,11 @@ SERE.
     \0 &\text{else}\\
   \end{cases}\\
   \sere{b_1\CONCAT r_1}\ANDALT\sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\ANDALT r_2} &
-  \sere{b_1\CONCAT r_1}\AND   \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND    r_2} \\
+  \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} \\
   \sere{b_1\FUSION r_1}\ANDALT\sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\ANDALT r_2} &
-  \sere{b_1\FUSION r_1}\AND   \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND    r_2} \\
-  \sere{r_1\CONCAT b_1}\ANDALT\sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\ANDALT b_2} &
-  \sere{r_1\CONCAT b_1}\AND   \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND    b_2} \\
-  \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} &
-  \sere{r_1\FUSION b_1}\AND   \sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\AND    b_2} \\
+  \sere{r_1\FUSION b_1}\ANDALT\sere{r_2\FUSION b_2} &\equiv \sere{r_1\ANDALT r_2}\FUSION\sere{b_1\ANDALT b_2} \\
+  \sere{b_1\CONCAT r_1}\AND \sere{b_2\CONCAT r_2} &\equiv \sere{b_1\ANDALT b_2}\CONCAT\sere{r_1\AND r_2} \\
+  \sere{b_1\FUSION r_1}\AND \sere{b_2\FUSION r_2} &\equiv \sere{b_1\ANDALT b_2}\FUSION\sere{r_1\AND r_2} \mathrlap{\quad\text{if~}\varepsilon\nVDash r_1\land\varepsilon\nVDash r_2}\\
 \end{align*}
 
 Starred subformul\ae{} are rewritten in Star Normal
diff --git a/src/ltltest/equals.cc b/src/ltltest/equals.cc
index a9b5905f9..99ae46cfe 100644
--- a/src/ltltest/equals.cc
+++ b/src/ltltest/equals.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // 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.
@@ -68,7 +68,7 @@ main(int argc, char** argv)
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
     return 2;
 
-  int exit_code;
+  int exit_code = 0;
 
   {
 #if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
@@ -112,6 +112,14 @@ main(int argc, char** argv)
       const spot::ltl::formula* tmp;
       tmp = f1;
       f1 = simp.simplify(f1);
+
+      if (!simp.are_equivalent(f1, tmp))
+	{
+	  std::cerr << "Source and simplified formulae are not equivalent!\n";
+	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+	  exit_code = 1;
+	}
+
       tmp->destroy();
     }
     spot::ltl::dump(std::cout, f1);
@@ -124,6 +132,14 @@ main(int argc, char** argv)
       const spot::ltl::formula* tmp;
       tmp = f1;
       f1 = simp.simplify(f1);
+
+      if (!simp.are_equivalent(f1, tmp))
+	{
+	  std::cerr << "Source and simplified formulae are not equivalent!\n";
+	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+	  exit_code = 1;
+	}
+
       tmp->destroy();
     }
     spot::ltl::dump(std::cout, f1);
@@ -136,13 +152,21 @@ main(int argc, char** argv)
       const spot::ltl::formula* tmp;
       tmp = f1;
       f1 = simp.simplify(f1);
+
+      if (!simp.are_equivalent(f1, tmp))
+	{
+	  std::cerr << "Source and simplified formulae are not equivalent!\n";
+	  std::cerr << "Simplified: " << spot::ltl::to_string(f1) << "\n";
+	  exit_code = 1;
+	}
+
       tmp->destroy();
     }
     spot::ltl::dump(std::cout, f1);
     std::cout << std::endl;
 #endif
 
-    exit_code = f1 != f2;
+    exit_code |= f1 != f2;
 
 #if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
     spot::ltl::ltl_simplifier simp;
@@ -150,8 +174,11 @@ main(int argc, char** argv)
 
     if (!simp.are_equivalent(f1, f2))
       {
-	std::cerr << "Source and destination formulae are not equivalent!"
-		  << std::endl;
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
+	std::cerr << "Source and destination formulae are not equivalent!\n";
+#else
+	std::cerr << "Simpl. and destination formulae are not equivalent!\n";
+#endif
 	exit_code = 1;
       }
 
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 0068be820..65338f1cd 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
-# et Developpement de l'Epita (LRDE).
+# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
+# Recherche et Developpement de l'Epita (LRDE).
 # 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.
@@ -317,9 +317,10 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
               '{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
      run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
-     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1&&b2}:{r1*&r2*}}'
-     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
-     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
+     run 0 $x '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}'
+     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced
+     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*;b1}&{r2*;b2}}' # Not reduced
+     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*:b1}&{r2*:b2}}' # Not reduced
      run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
               '{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
      run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index 3d57e8647..c2ce125d7 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+// Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 // Developpement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -3456,22 +3456,14 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				head1->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail1->push_back(multop::instance(op, tail));
+				tail1->push_back(f->all_but(0));
 				(*i)->destroy();
 				*i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
 				head2->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail2->push_back(multop::instance(op, tail));
+				tail2->push_back(f->all_but(0));
 				(*i)->destroy();
 				*i = 0;
 			      }
@@ -3535,20 +3527,14 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				tail3->push_back(t->clone());
-				multop::vec* head = new multop::vec;
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head3->push_back(multop::instance(op, head));
+				head3->push_back(f->all_but(s));
 				(*i)->destroy();
 				*i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
 				tail4->push_back(t->clone());
-				multop::vec* head = new multop::vec;
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head4->push_back(multop::instance(op, head));
+				head4->push_back(f->all_but(s));
 				(*i)->destroy();
 				*i = 0;
 			      }
@@ -4155,6 +4141,8 @@ namespace spot
 			//                    head1   tail1
 			// {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2}
 			//                    head2   tail2
+			// BEWARE: The second rule is correct only when
+			// both r1 and r2 do not accept [*0].
 
 			multop::vec* head1 = new multop::vec;
 			multop::vec* tail1 = new multop::vec;
@@ -4175,22 +4163,20 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				head1->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail1->push_back(multop::instance(op, tail));
+				tail1->push_back(f->all_but(0));
 				(*i)->destroy();
 				*i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
+				const formula* t = f->all_but(0);
+				if (t->accepts_eword())
+				  {
+				    t->destroy();
+				    continue;
+				  }
 				head2->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
-				unsigned s = f->size();
-				for (unsigned j = 1; j < s; ++j)
-				  tail->push_back(f->nth(j)->clone());
-				tail2->push_back(multop::instance(op, tail));
+				tail2->push_back(t);
 				(*i)->destroy();
 				*i = 0;
 			      }
@@ -4230,83 +4216,6 @@ namespace spot
 			    delete tail2;
 			  }
 
-			// {r1;b1}&{r2;b2} = {r1&r2};{b1∧b2}
-			//                    head3   tail3
-			// {r1:b1}&{r2:b2} = {r1&r2}:{b1∧b2}
-			//                    head4   tail4
-			multop::vec* head3 = new multop::vec;
-			multop::vec* tail3 = new multop::vec;
-			multop::vec* head4 = new multop::vec;
-			multop::vec* tail4 = new multop::vec;
-			for (multop::vec::iterator i = s.res_other->begin();
-			     i != s.res_other->end(); ++i)
-			  {
-			    if (!*i)
-			      continue;
-			    if ((*i)->kind() != formula::MultOp)
-			      continue;
-			    const multop* f = down_cast<const multop*>(*i);
-			    unsigned s = f->size() - 1;
-			    const formula* t = f->nth(s);
-			    if (!t->is_boolean())
-			      continue;
-			    multop::type op = f->op();
-			    if (op == multop::Concat)
-			      {
-				tail3->push_back(t->clone());
-				multop::vec* head = new multop::vec;
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head3->push_back(multop::instance(op, head));
-				(*i)->destroy();
-				*i = 0;
-			      }
-			    else if (op == multop::Fusion)
-			      {
-				tail4->push_back(t->clone());
-				multop::vec* head = new multop::vec;
-				for (unsigned j = 0; j < s; ++j)
-				  head->push_back(f->nth(j)->clone());
-				head4->push_back(multop::instance(op, head));
-				(*i)->destroy();
-				*i = 0;
-			      }
-			    else
-			      {
-				continue;
-			      }
-			  }
-			if (!head3->empty())
-			  {
-			    const formula* h =
-			      multop::instance(multop::AndNLM, head3);
-			    const formula* t =
-			      multop::instance(multop::And, tail3);
-			    const formula* f =
-			      multop::instance(multop::Concat, h, t);
-			    s.res_other->push_back(f);
-			  }
-			else
-			  {
-			    delete head3;
-			    delete tail3;
-			  }
-			if (!head4->empty())
-			  {
-			    const formula* h =
-			      multop::instance(multop::AndNLM, head4);
-			    const formula* t =
-			      multop::instance(multop::And, tail4);
-			    const formula* f =
-			      multop::instance(multop::Fusion, h, t);
-			    s.res_other->push_back(f);
-			  }
-			else
-			  {
-			    delete head4;
-			    delete tail4;
-			  }
-
 			result_ = multop::instance(multop::AndNLM, s.res_other);
 			// If we altered the formula in some way, process
 			// it another time.

From 362862dace0b341da351e67fa710c79b2a540a17 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 13 May 2014 17:08:18 +0200
Subject: [PATCH 08/13] llt2tgba_fm: fix translation of ":" in some SERE

* src/tgbaalgos/ltl2tgba_fm.cc: Here.
* src/ltltest/reduccmp.test: Add a test case.
* NEWS: Mention it.
---
 NEWS                         |  2 ++
 src/ltltest/reduccmp.test    |  2 ++
 src/tgbaalgos/ltl2tgba_fm.cc | 13 +++++++------
 3 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/NEWS b/NEWS
index 3509f9e3c..7d026bea7 100644
--- a/NEWS
+++ b/NEWS
@@ -17,6 +17,8 @@ New in spot 1.2.3a (not yet released)
     - Fix three incorrect simplifications rules, all related to the
       factorization of Boolean subformulas in operands of the
       non-length-matching "&" SERE operator.
+    - Fix incorrect translation of the fusion operator (":") in SERE
+      such as {xx;1}:yy[*] where the left operand has 1 as tail.
 
 New in spot 1.2.3 (2014-02-11)
 
diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test
index 65338f1cd..cfa5de45c 100755
--- a/src/ltltest/reduccmp.test
+++ b/src/ltltest/reduccmp.test
@@ -348,6 +348,8 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x '{s[*]}<>->b' 'b M s'
      run 0 $x '{s[+]}<>->b' 'b M s'
      run 0 $x '{s[*2..]}<>->b' 's & X(b M s)'
+     run 0 $x '{1:a*}!' 'a'
+     run 0 $x '{(1;1):a*}!' 'Xa'
      run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))'
      run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)'
      run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index bde8ec011..a972cb12c 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire
 // d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
 // Coopératifs (SRC), Université Pierre et Marie Curie.
@@ -912,11 +912,12 @@ namespace spot
 
 		    }
 
-		  if (dest->kind() != formula::Constant)
+		  // If the destination is not 0 or [*0], it means it
+		  // can have successors.  Fusion the tail and append
+		  // anything to concatenate.
+		  if (dest->kind() != formula::Constant
+		      || dest == ltl::constant::true_instance())
 		    {
-		      // If the destination is not a constant, it
-		      // means it can have successors.  Fusion the
-		      // tail and append anything to concatenate.
 		      const formula* dest2 =
 			multop::instance(multop::Fusion, dest, tail->clone());
 		      if (to_concat_)

From d741d9266d1acc5b2698e3edb0bbaada0aa38da0 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 13 May 2014 17:26:53 +0200
Subject: [PATCH 09/13] simplify: remove an incorrect simplification rule

Fortunately was only enabled with the
ltl_simplifier_options::favor_event_univ option, which cannot yet be
turned on from the command-line tools.

* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/eventuniv.test: Adjust.
* NEWS: Mention the bug.
---
 NEWS                       |  8 +++++---
 doc/tl/tl.tex              |  1 -
 src/ltltest/eventuniv.test |  6 +++---
 src/ltlvisit/simplify.cc   | 19 -------------------
 4 files changed, 8 insertions(+), 26 deletions(-)

diff --git a/NEWS b/NEWS
index 7d026bea7..b481495e0 100644
--- a/NEWS
+++ b/NEWS
@@ -14,9 +14,11 @@ New in spot 1.2.3a (not yet released)
     - "ltl2tgta --ta" could crash in certain conditions due to the
       introduction of a simulation-based reduction after
       degeneralization.
-    - Fix three incorrect simplifications rules, all related to the
-      factorization of Boolean subformulas in operands of the
-      non-length-matching "&" SERE operator.
+    - Fix four incorrect formula-simplification rules, three were
+      related to the factorization of Boolean subformulas in
+      operands of the non-length-matching "&" SERE operator, and
+      a fourth one could only be enabled by explicitely passing the
+      favor_event_univ option to the simplifier (not the default).
     - Fix incorrect translation of the fusion operator (":") in SERE
       such as {xx;1}:yy[*] where the left operand has 1 as tail.
 
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index 18d89f1f8..b843ff41e 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1580,7 +1580,6 @@ $q,\,q_i$           & a pure eventuality that is also purely universal \\
               &                     & f \U (g\AND q) & \equivEU (f \U g)\AND q & (f\AND q)\M g & \equivEU (f \M g)\AND q                                \\
   \G u        & \equiv u            & u \W g         & \equiv u\OR g           & f \R u        & \equiv u       & e_1 \W e_2 & \equiV (\G e_1) \OR e_2  \\
   \G(e)\AND q & \equiv \G(e\AND q)  & f \W (g\OR e)  & \equivEU (f \W g)\OR e  & f\R (g\AND u) & \equivEU (f \R g)\AND u                                \\
-              &                     & (f\OR u) \W g  & \equivEU (f \W g)\OR u                                                                           \\
   \X q        & \equiv q            & q \AND \X f    & \equivNeu \X(q \AND f)  & q\OR \X f     & \equivNeu \X(q \OR f)                                  \\
               &                     & \X(q \AND f)   & \equivEU q \AND \X f    & \X(q \OR f)   & \equivEU q\OR \X f                                     \\
 \end{align*}
diff --git a/src/ltltest/eventuniv.test b/src/ltltest/eventuniv.test
index 195322795..304e3c903 100755
--- a/src/ltltest/eventuniv.test
+++ b/src/ltltest/eventuniv.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
-# de l'Epita (LRDE).
+# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+# Developpement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -48,7 +48,7 @@ check 'a U (b | Fc)'  '(a U b) | Fc'
 check 'a W (b | Fc)'  '(a W b) | Fc'
 check 'a U (b & GFc)' '(a U b) & GFc'
 check 'a W (b & GFc)' 'a W (b & GFc)'  # Unchanged
-check '(a | Gc) W g'  '(a W g) | Gc'
+check '(a | Gc) W g'  '(a | Gc) W g'   # Unchanged
 check '(a | Gc) U g'  '(a | Gc) U g'   # Unchanged
 
 check '(a & GFc) M b' '(a M b) & GFc'
diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc
index c2ce125d7..88c93c5be 100644
--- a/src/ltlvisit/simplify.cc
+++ b/src/ltlvisit/simplify.cc
@@ -2075,7 +2075,6 @@ namespace spot
 	      // (a W (b|e)) = (a W b)|e
 	      // (a U (b&q)) = (a U b)&q
 	      // ((a&q) M b) = (a M b)&q
-	      // ((a|u) W b) = u|(a W b)
 	      // (a R (b&u)) = (a R b)&u
 	      // (a M (b&u)) = (a M b)&u
 	      if (opt_.favor_event_univ)
@@ -2099,24 +2098,6 @@ namespace spot
 			b2->destroy();
 			delete s.res_Event;
 		      }
-		  if (op == binop::W)
-		    if (const multop* mo = is_Or(a))
-		      {
-			a->clone();
-			mospliter s(mospliter::Split_Univ, mo, c_);
-			const formula* a2 =
-			  multop::instance(multop::Or, s.res_other);
-			if (a2 != a)
-			  {
-			    a->destroy();
-			    s.res_Univ->push_back(binop::instance(op, a2, b));
-			    result_ = recurse_destroy
-			      (multop::instance(multop::Or, s.res_Univ));
-			    return;
-			  }
-			a2->destroy();
-			delete s.res_Univ;
-		      }
 		  if (op == binop::U)
 		    if (const multop* mo = is_And(b))
 		      {

From c46d6cee9a7514b81d413022ae4dcc3d539e66c9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 13 May 2014 18:26:32 +0200
Subject: [PATCH 10/13] * src/ltlast/multop.hh: Typo in comment.

---
 src/ltlast/multop.hh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index a2a970964..900620c37 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -140,7 +140,7 @@ namespace spot
 
       /// \brief construct a formula without the nth child.
       ///
-      /// If the formula \c f is <code>a|b|c|d</code> and <code>d</code>
+      /// If the formula \c f is <code>a|b|c|d</code> and <code>c</code>
       /// is child number 2, then calling <code>f->all_but(2)</code> will
       /// return a new formula <code>a|b|d</code>.
       const formula* all_but(unsigned n) const;

From 9761703736f3d0c49e566a82648ca1ab6ab53385 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 14 May 2014 18:16:12 +0200
Subject: [PATCH 11/13] doc: update bibliographic references

* doc/org/satmin.org, src/bin/man/dstar2tgba.x, src/bin/man/ltl2tgba.x:
Cite the FORTE'14 paper.
* doc/org/tools.org, src/bin/man/ltl2tgba.x: Replace the VECOS'11
citation by IJCCBS'14.
* src/bin/man/ltl2tgba.x: Cite SPIN'13.
---
 doc/org/satmin.org       |  4 +++-
 doc/org/tools.org        |  6 +++---
 src/bin/man/dstar2tgba.x | 12 +++++++++++-
 src/bin/man/ltl2tgba.x   | 13 ++++++++++++-
 4 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/doc/org/satmin.org b/doc/org/satmin.org
index 4fc1244a8..f2f8c394c 100644
--- a/doc/org/satmin.org
+++ b/doc/org/satmin.org
@@ -31,8 +31,10 @@ Let us first state a few facts about this minimization procedure.
    automaton: when the number of clauses output by Spot (and to be fed
    to the SAT solver) exceeds $2^{31}$, or when the SAT-solver was
    killed by a signal.
+6) Details about the SAT encoding used in the two procedures can be
+   found in our [[http://www.lrde.epita.fr/~adl/dl/adl/baarir.14.forte.pdf][FORTE'14 paper]].
 
-* How change the SAT solver used
+* How to change the SAT solver used
 
 The environment variable =SPOT_SATSOLVER= can be used to change the
 SAT solver used by Spot.  The default is "=glucose -verb=0 -model %I
diff --git a/doc/org/tools.org b/doc/org/tools.org
index 0d1cd597d..beccf501f 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -60,9 +60,9 @@ the following articles:
 
   This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
 
-- *LTL translation improvements in Spot*, /Alexandre Duret-Lutz/.
-  In Proc. of VECoS'11.  Electronic Workshops in Computing. Tunis, Tunisia, Sep. 2011.
-  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.11.vecos][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.pdf][pdf]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.11.vecos.slides.pdf][slides]])
+- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/.
+  Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
+  ([[https://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.14.ijccbs][bib]] | [[https://www.lrde.epita.fr/~adl/dl/adl/duret.14.ijccbs.draft.pdf][pdf]])
 
   This describes the translation from LTL to TGBA used by =ltl2tgba=
   and =ltl2tgta=.
diff --git a/src/bin/man/dstar2tgba.x b/src/bin/man/dstar2tgba.x
index ce7cec939..1198b6e94 100644
--- a/src/bin/man/dstar2tgba.x
+++ b/src/bin/man/dstar2tgba.x
@@ -2,7 +2,7 @@
 dstar2tgba \- convert Rabin or Streett automata into Büchi automata
 [BIBLIOGRAPHY]
 .TP
-1. 
+1.
 <http://www.ltl2dstar.de/docs/ltl2dstar.html>
 
 Documents the output format of ltl2dstar.
@@ -28,5 +28,15 @@ dstar2tgba implements this for the Rabin case only.  In other words,
 translating a deterministic Rabin automaton with dstar2tgba will
 produce a deterministic TGBA or BA if such a automaton exists.
 
+.TP
+4.
+Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
+of deterministic generalized Büchi automata.  Proceedings of FORTE'14.
+LNCS 8461.
+
+Explains the SAT-based minimization techniques that can be used (on
+request only) by dstar2tgba to minimize deterministic Büchi automata.
+
+
 [SEE ALSO]
 .BR spot-x (7)
diff --git a/src/bin/man/ltl2tgba.x b/src/bin/man/ltl2tgba.x
index 986e3a63d..3df465814 100644
--- a/src/bin/man/ltl2tgba.x
+++ b/src/bin/man/ltl2tgba.x
@@ -85,11 +85,22 @@ If you would like to give a reference to this tool in an article,
 we suggest you cite one of the following papers:
 .TP
 \(bu
-Alexandre Duret-Lutz: LTL translation improvements in Spot. Proceedings of VECoS'11.
+Alexandre Duret-Lutz: LTL translation improvements in Spot 1.0.
+Int. J. on Critical Computer-Based Systems, 5(1/2):31--54, March 2014.
 .TP
 \(bu
 Alexandre Duret-Lutz: Manipulating LTL formulas using Spot 1.0.
 Proceedings of ATVA'13.  LNCS 8172.
+.TP
+\(bu
+Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský,
+and Jan Strejček: Compositional approach to suspension and other
+improvements to LTL translation.  Proceedings of SPIN'13.  LNCS 7976.
+.TP
+\(bu
+Souheib Baarir and Alexandre Duret-Lutz: Mechanizing the minimization
+of deterministic generalized Büchi automata.  Proceedings of FORTE'14.
+LNCS 8461.
 
 [SEE ALSO]
 .BR spot-x (7)

From c11f15c76c753da159d070ea287de9049461d345 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 15 May 2014 10:51:38 +0200
Subject: [PATCH 12/13] Release Spot 1.2.4

* NEWS, configure.ac, doc/org/tools.org: Bump version.
---
 NEWS              | 10 +++++-----
 configure.ac      |  2 +-
 doc/org/tools.org |  2 +-
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/NEWS b/NEWS
index b481495e0..3ede1b904 100644
--- a/NEWS
+++ b/NEWS
@@ -1,10 +1,10 @@
-New in spot 1.2.3a (not yet released)
+New in spot 1.2.4 (2014-05-15)
 
   * New features:
 
     - "-B -x degen-lskip" can be used to disable level-skipping in the
-      degeralization procedure.  This is mostly meant for running
-      experiments.
+      degeralization procedure called by ltl2tgba and dstar2tgba.
+      This is mostly meant for running experiments.
     - "-B -x degen-lcache=N" can be used to experiment with different
       type of level caching during degeneralization.
 
@@ -53,8 +53,8 @@ New in spot 1.2.3 (2014-02-11)
     - Fix determinism of the SAT-based minimization encoding.
       (It would sometimes produce different equivalent automata,
       because of a different encoding order.)
-    - A the SAT-based minimization is asked for a 10-state automaton
-      and return a 6-state automaton, do not ask for a 9-state
+    - If the SAT-based minimization is asked for a 10-state automaton
+      and returns a 6-state automaton, do not ask for a 9-state
       automaton in the next iteration...
     - Fix some compilation issue with the version of Apple's Clang
       that is installed with MacOS X 10.9.
diff --git a/configure.ac b/configure.ac
index e0ec68fc3..86a43c6d8 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AC_PREREQ([2.61])
-AC_INIT([spot], [1.2.3a], [spot@lrde.epita.fr])
+AC_INIT([spot], [1.2.4], [spot@lrde.epita.fr])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
 AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])
diff --git a/doc/org/tools.org b/doc/org/tools.org
index beccf501f..24c937364 100644
--- a/doc/org/tools.org
+++ b/doc/org/tools.org
@@ -1,4 +1,4 @@
-#+TITLE: Command-line tools installed by Spot 1.2.3
+#+TITLE: Command-line tools installed by Spot 1.2.4
 #+EMAIL spot@lrde.epita.fr
 #+OPTIONS: H:2 num:nil toc:t
 

From f431852af99bedc61fdf457612126ce2227a3585 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 15 May 2014 12:13:29 +0200
Subject: [PATCH 13/13] * NEWS, configure.ac: Bump version to 1.2.4a.

---
 NEWS         | 4 ++++
 configure.ac | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index 3ede1b904..f41560a51 100644
--- a/NEWS
+++ b/NEWS
@@ -1,3 +1,7 @@
+New in spot 1.2.4a (not yet released)
+
+  Nothing yet.
+
 New in spot 1.2.4 (2014-05-15)
 
   * New features:
diff --git a/configure.ac b/configure.ac
index 86a43c6d8..3df567c20 100644
--- a/configure.ac
+++ b/configure.ac
@@ -21,7 +21,7 @@
 # along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 AC_PREREQ([2.61])
-AC_INIT([spot], [1.2.4], [spot@lrde.epita.fr])
+AC_INIT([spot], [1.2.4a], [spot@lrde.epita.fr])
 AC_CONFIG_AUX_DIR([tools])
 AC_CONFIG_MACRO_DIR([m4])
 AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])