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

@@ -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/tgbaalgos/degen.cc

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

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/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

@@ -1,8 +1,9 @@
-## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et
+## -*- coding: utf-8 -*-
-## Développement de l'Epita (LRDE).
+## 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),
+## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
-## Université Pierre et Marie Curie.
+## 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 \

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