autfilt: --instut, --destut, --is-empty

* src/bin/autfilt.cc: Add these new options.
* src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Make it
possible to call sl() and sl2() without passing the set of atomic
propositions.
* src/tgbatest/stutter.test: New file.
* src/tgbatest/Makefile.am: Add it.

src/bin/autfilt.cc

@@ -40,6 +40,8 @@
 #include "tgbaalgos/save.hh"
 #include "tgbaalgos/stats.hh"
 #include "tgbaalgos/isdet.hh"
+#include "tgbaalgos/stutterize.hh"
+#include "tgbaalgos/closure.hh"
 #include "tgba/bddprint.hh"
 #include "misc/optionmap.hh"
 #include "misc/timer.hh"
@@ -75,6 +77,9 @@ Exit status:\n\
 #define OPT_NAME 19
 #define OPT_EDGES 20
 #define OPT_ACC_SETS 21
+#define OPT_DESTUT 22
+#define OPT_INSTUT 23
+#define OPT_IS_EMPTY 24
 
 static const argp_option options[] =
   {
@@ -150,6 +155,8 @@ static const argp_option options[] =
     { "randomize", OPT_RANDOMIZE, "s|t", OPTION_ARG_OPTIONAL,
       "randomize states and transitions (specify 's' or 't' to "
       "randomize only states or transitions)", 0 },
+    { "instut", OPT_INSTUT, 0, 0, "allow more stuttering", 0 },
+    { "destut", OPT_DESTUT, 0, 0, "allow less stuttering", 0 },
     /**************************************************/
     { 0, 0, 0, 0, "Filters:", 6 },
     { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0,
@@ -159,6 +166,8 @@ static const argp_option options[] =
       "the automaton is complete", 0 },
     { "is-deterministic", OPT_IS_DETERMINISTIC, 0, 0,
       "the automaton is deterministic", 0 },
+    { "is-empty", OPT_IS_EMPTY, 0, 0,
+      "keep automata with an empty language", 0 },
     { "invert-match", 'v', 0, 0, "select non-matching automata", 0 },
     { "states", OPT_STATES, "RANGE", 0,
       "keep automata whose number of states are in RANGE", 0 },
@@ -204,6 +213,9 @@ static range opt_edges = { 0, std::numeric_limits<int>::max() };
 static range opt_accsets = { 0, std::numeric_limits<int>::max() };
 static const char* opt_name = nullptr;
 static int opt_max_count = -1;
+static bool opt_destut = false;
+static bool opt_instut = false;
+static bool opt_is_empty = false;
 
 static int
 to_int(const char* s)
@@ -289,12 +301,21 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_EDGES:
       opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
       break;
+    case OPT_INSTUT:
+      opt_instut = true;
+      break;
+    case OPT_DESTUT:
+      opt_destut = true;
+      break;
     case OPT_IS_COMPLETE:
       opt_is_complete = true;
       break;
     case OPT_IS_DETERMINISTIC:
       opt_is_deterministic = true;
       break;
+    case OPT_IS_EMPTY:
+      opt_is_empty = true;
+      break;
     case OPT_LBTT:
       if (arg)
 	{
@@ -526,6 +547,8 @@ namespace
 	matched &= is_deterministic(aut);
       if (opt_are_isomorphic)
         matched &= !are_isomorphic(aut, opt_are_isomorphic).empty();
+      if (opt_is_empty)
+	matched &= aut->is_empty();
 
       // Drop or keep matched automata depending on the --invert option
       if (matched == opt_invert)
@@ -535,6 +558,11 @@ namespace
 
       // Postprocessing.
 
+      if (opt_destut)
+	aut = spot::closure(std::move(aut));
+      if (opt_instut)
+	aut = spot::sl(aut);
+
       if (opt_product)
 	aut = spot::product(std::move(aut), opt_product);
 

src/tgbaalgos/stutterize.cc

@@ -54,17 +54,30 @@ namespace spot
     typedef std::deque<stutter_state> queue_t;
   }
 
+  static bdd
+  get_all_ap(const const_tgba_digraph_ptr& a)
+  {
+    bdd res = bddtrue;
+    for (auto& i: a->transitions())
+      res &= bdd_support(i.cond);
+    return res;
+  }
+
   tgba_digraph_ptr
   sl(const const_tgba_digraph_ptr& a, const ltl::formula* f)
   {
-    bdd aps = atomic_prop_collect_as_bdd(f, a);
+    bdd aps = f
+      ? atomic_prop_collect_as_bdd(f, a)
+      : get_all_ap(a);
     return sl(a, aps);
   }
 
   tgba_digraph_ptr
   sl2(const const_tgba_digraph_ptr& a, const ltl::formula* f)
   {
-    bdd aps = atomic_prop_collect_as_bdd(f, a);
+    bdd aps = f
+      ? atomic_prop_collect_as_bdd(f, a)
+      : get_all_ap(a);
     return sl2(a, aps);
   }
 
@@ -135,6 +148,8 @@ namespace spot
   tgba_digraph_ptr
   sl2(tgba_digraph_ptr&& a, bdd atomic_propositions)
   {
+    if (atomic_propositions == bddfalse)
+      atomic_propositions = get_all_ap(a);
     unsigned num_states = a->num_states();
     unsigned num_transitions = a->num_transitions();
     for (unsigned state = 0; state < num_states; ++state)

src/tgbaalgos/stutterize.hh

@@ -28,20 +28,20 @@
 namespace spot
 {
   SPOT_API tgba_digraph_ptr
-  sl(const const_tgba_digraph_ptr&, const ltl::formula*);
+  sl(const const_tgba_digraph_ptr&, const ltl::formula* = nullptr);
 
   SPOT_API tgba_digraph_ptr
   sl(const const_tgba_digraph_ptr&, bdd);
 
   SPOT_API tgba_digraph_ptr
-  sl2(const const_tgba_digraph_ptr&, const ltl::formula*);
+  sl2(const const_tgba_digraph_ptr&, const ltl::formula* = nullptr);
 
   SPOT_API tgba_digraph_ptr
   sl2(const const_tgba_digraph_ptr&, bdd);
 
 #ifndef SWIG
   SPOT_API tgba_digraph_ptr
-  sl2(tgba_digraph_ptr&&);
+  sl2(tgba_digraph_ptr&&, bdd = bddfalse);
 #endif
 }
 

src/tgbatest/Makefile.am

@@ -119,6 +119,7 @@ TESTS = \
   randaut.test \
   randtgba.test \
   isomorph.test \
+  stutter.test \
   emptchk.test \
   emptchke.test \
   dfs.test \

src/tgbatest/stutter.test

@@ -0,0 +1,38 @@
+#! /bin/sh
+# -*- coding: utf-8 -*-
+# 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 || exit 1
+
+set -e
+
+ltl2tgba=../../bin/ltl2tgba
+autfilt=../../bin/autfilt
+
+$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --destut > pos.hoa
+$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa
+$autfilt pos.hoa --product neg.hoa -H > prod.hoa
+$autfilt --is-empty prod.hoa -q && exit 1
+$autfilt --states=10 prod.hoa -q
+
+$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --instut > pos.hoa
+$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa
+$autfilt pos.hoa --product neg.hoa -H > prod.hoa
+$autfilt --is-empty prod.hoa -q && exit 1
+$autfilt --states=12 prod.hoa -q