Merge branch 'master' into next

Conflicts:
	src/ltlvisit/simplify.cc
	src/tgbatest/Makefile.am

AUTHORS

@@ -12,7 +12,7 @@ Guillaume Sadegh
 Heikki Tauriainen
 Pierre Parutto
 Rachid Rebiha
-Soheib Baarir
+Souheib Baarir
 Thomas Badie
 Thomas Martinez
 Tomáš Babiak

NEWS

@@ -1,4 +1,4 @@
-New in spot 1.2.3a (not yet released)
+New in spot 1.2.4a (not yet released)
 
   * Major changes (including backward incompatible changes):
 
@@ -69,6 +69,30 @@ New in spot 1.2.3a (not yet released)
       implementation of Couvreur's FM'99 emptiness check.
 
 
+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 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.
+
+  * 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.
+    - 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.
+
 New in spot 1.2.3 (2014-02-11)
 
   * New features:
@@ -100,8 +124,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
+    - If the SAT-based minimization is asked for a 10-state automaton
-      and return a 6-state automaton, do not ask for a 9-state
+      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.

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.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])

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

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
 
@@ -60,9 +60,9 @@ the following articles:
 
   This focuses on =ltlfilt=, =randltl=, and =ltlcross=.
 
-- *LTL translation improvements in Spot*, /Alexandre Duret-Lutz/.
+- *LTL translation improvements in Spot 1.0*, /Alexandre Duret-Lutz/.
-  In Proc. of VECoS'11.  Electronic Workshops in Computing. Tunis, Tunisia, Sep. 2011.
+  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.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]])
+  ([[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=.

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\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\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\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}\AND   \sere{r_2\CONCAT b_2} &\equiv \sere{r_1\ANDALT r_2}\CONCAT\sere{b_1\AND    b_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}\\
-  \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} \\
 \end{align*}
 
 Starred subformul\ae{} are rewritten in Star Normal
@@ -1582,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*}

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)

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)

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

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;

src/ltltest/equals.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
-// et Développement de l'Epita (LRDE).
+// 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!"
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
-		  << std::endl;
+	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;
       }
 

src/ltltest/eventuniv.test

@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2013 Laboratoire de Recherche et Developpement
+# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
-# de l'Epita (LRDE).
+# 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'

src/ltltest/reduccmp.test

@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
+# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
-# et Developpement de l'Epita (LRDE).
+# 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 '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}'
-     run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*&r2*};{b1&&b2}}'
+     run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced
-     run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*&r2*}:{b1&&b2}}'
+     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}}*}!'
@@ -347,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)'

src/ltlvisit/simplify.cc

@@ -2068,7 +2068,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)
@@ -2092,24 +2091,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))
 		      {
@@ -3438,22 +3419,14 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				head1->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail1->push_back(f->all_but(0));
-				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));
 				i->destroy();
 				i = 0;
 			      }
 			    else if (op == multop::Fusion)
 			      {
 				head2->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail2->push_back(f->all_but(0));
-				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));
 				i->destroy();
 				i = 0;
 			      }
@@ -3516,20 +3489,14 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				tail3->push_back(t->clone());
-				multop::vec* head = new multop::vec;
+				head3->push_back(f->all_but(s));
-				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;
+				head4->push_back(f->all_but(s));
-				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;
 			      }
@@ -4127,6 +4094,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;
@@ -4146,22 +4115,20 @@ namespace spot
 			    if (op == multop::Concat)
 			      {
 				head1->push_back(h->clone());
-				multop::vec* tail = new multop::vec;
+				tail1->push_back(f->all_but(0));
-				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));
 				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;
+				tail2->push_back(t);
-				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));
 				i->destroy();
 				i = 0;
 			      }
@@ -4201,82 +4168,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 (auto& i: *s.res_other)
-			  {
-			    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.

src/taalgos/tgba2ta.cc

@@ -417,35 +417,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;
+	  state_ta_explicit* init_state = new
-	  if (degeneralized)
+	    state_ta_explicit(tgba_init_state->clone(),
-	    {
+			      satone_tgba_condition, true, is_acc);
-	      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* s = ta->add_state(init_state);
 	  assert(s == init_state);
 	  ta->add_to_initial_states_set(s);
@@ -478,6 +474,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,
@@ -485,21 +492,9 @@ namespace spot
 			   != bddfalse)
 		      {
 			all_props -= dest_condition;
-			state_ta_explicit* new_dest;
+			state_ta_explicit* new_dest =
-			if (degeneralized)
+			  new state_ta_explicit(tgba_state->clone(),
-			  {
+						dest_condition, false, is_acc);
-			    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* dest = ta->add_state(new_dest);
 
 			if (dest != new_dest)

src/tgbaalgos/degen.cc

@@ -25,6 +25,7 @@
 #include "ltlast/constant.hh"
 #include <deque>
 #include <vector>
+#include <algorithm>
 #include "tgbaalgos/scc.hh"
 #include "tgba/bddprint.hh"
 
@@ -174,7 +175,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_)
@@ -200,7 +201,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;
       }
 
@@ -223,16 +228,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
@@ -247,7 +254,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;
 
@@ -290,7 +297,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.
@@ -312,7 +319,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.
@@ -342,7 +349,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
@@ -479,7 +490,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())
                   {
@@ -520,10 +532,17 @@ namespace spot
 			    // Consider both the current acceptance
 			    // sets, and the acceptance sets common to
 			    // the outgoing transitions of the
-			    // destination state.
+			    // destination state.  But don't do
-			    while (next < order.size()
+			    // that if the state is accepting and we
-				   && bdd_implies(order[next], acc))
+			    // are not skipping levels.
-			      ++next;
+			    if (skip_levels || !is_acc)
+			      while (next < order.size()
+				     && bdd_implies(order[next], acc))
+				{
+				  ++next;
+				  if (!skip_levels)
+				    break;
+				}
 			    d.second = next;
 			  }
                       }
@@ -547,8 +566,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 =

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);
 }
 
 

src/tgbaalgos/ltl2tgba_fm.cc

@@ -913,11 +913,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_)

src/tgbaalgos/postproc.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// 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),
+      degen_lskip_(true), simul_(-1), scc_filter_(-1), ba_simul_(-1),
-      sat_minimize_(0), sat_acc_(0), sat_states_(0), state_based_(false),
+      tba_determinisation_(false), sat_minimize_(0), sat_acc_(0),
-      wdba_minimize_(true)
+      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;

src/tgbaalgos/postproc.hh

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
-// de l'Epita (LRDE).
+// 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_;

src/tgbatest/Makefile.am

@@ -99,6 +99,7 @@ TESTS = \
   ltl2neverclaim.test \
   ltl2neverclaim-lbtt.test \
   ltl2ta.test \
+  ltl2ta2.test \
   ltlprod.test \
   bddprod.test \
   explprod.test \
@@ -110,6 +111,7 @@ TESTS = \
   dupexp.test \
   degendet.test \
   degenid.test \
+  degenlskip.test \
   kv.test \
   lbttparse.test \
   scc.test \

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

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))'

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" \