From 4c0500a8a90a920222138248f4455569f495f376 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 19 Jul 2016 13:20:08 +0200
Subject: [PATCH] autfilt: add --stutter-invariant

* bin/autfilt.cc: Implement the option.
* NEWS: Mention it.
* tests/core/readsave.test, tests/core/stutter-tgba.test: Add some
tests.
---
 NEWS                         |  3 +++
 bin/autfilt.cc               | 23 ++++++++++++++++++-----
 tests/core/readsave.test     |  1 +
 tests/core/stutter-tgba.test |  3 +++
 4 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index a750e0658..d449e632d 100644
--- a/NEWS
+++ b/NEWS
@@ -23,6 +23,9 @@ New in spot 2.0.3a (not yet released)
   * autfilt can filter automata by count of nondeterministsic states
     with --nondet-states=RANGE.
 
+  * autfilt can filter automata representing stutter-invariant
+    properties with --is-stutter-invariant.
+
   * autfilt has two new options to highlight non-determinism:
     --highlight-nondet-states=NUM and --highlight-nondet-states=NUM
     where NUM is a color number.  Additionally --highlight-nondet=NUM
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index 5c4d8eca3..eb7f111e1 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -100,8 +100,9 @@ enum {
   OPT_IS_COMPLETE,
   OPT_IS_DETERMINISTIC,
   OPT_IS_EMPTY,
-  OPT_IS_UNAMBIGUOUS,
+  OPT_IS_STUTTER_INVARIANT,
   OPT_IS_TERMINAL,
+  OPT_IS_UNAMBIGUOUS,
   OPT_IS_WEAK,
   OPT_IS_INHERENTLY_WEAK,
   OPT_KEEP_STATES,
@@ -163,10 +164,12 @@ static const argp_option options[] =
       "keep deterministic automata", 0 },
     { "is-empty", OPT_IS_EMPTY, nullptr, 0,
       "keep automata with an empty language", 0 },
-    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
-      "keep only unambiguous automata", 0 },
+    { "is-stutter-invariant", OPT_IS_STUTTER_INVARIANT, nullptr, 0,
+      "keep automata representing stutter-invariant properties", 0 },
     { "is-terminal", OPT_IS_TERMINAL, nullptr, 0,
       "keep only terminal automata", 0 },
+    { "is-unambiguous", OPT_IS_UNAMBIGUOUS, nullptr, 0,
+      "keep only unambiguous automata", 0 },
     { "is-weak", OPT_IS_WEAK, nullptr, 0,
       "keep only weak automata", 0 },
     { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
@@ -365,6 +368,7 @@ static bool opt_is_unambiguous = false;
 static bool opt_is_terminal = false;
 static bool opt_is_weak = false;
 static bool opt_is_inherently_weak = false;
+static bool opt_is_stutter_invariant = false;
 static bool opt_invert = false;
 static range opt_states = { 0, std::numeric_limits<int>::max() };
 static range opt_edges = { 0, std::numeric_limits<int>::max() };
@@ -596,12 +600,15 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_IS_INHERENTLY_WEAK:
       opt_is_inherently_weak = true;
       break;
-    case OPT_IS_UNAMBIGUOUS:
-      opt_is_unambiguous = true;
+    case OPT_IS_STUTTER_INVARIANT:
+      opt_is_stutter_invariant = true;
       break;
     case OPT_IS_TERMINAL:
       opt_is_terminal = true;
       break;
+    case OPT_IS_UNAMBIGUOUS:
+      opt_is_unambiguous = true;
+      break;
     case OPT_IS_WEAK:
       opt_is_weak = true;
       break;
@@ -944,6 +951,12 @@ namespace
               matched = false;
               break;
             }
+      if (opt_is_stutter_invariant)
+        {
+          check_stutter_invariance(aut);
+          assert(aut->prop_stutter_invariant().is_known());
+          matched &= aut->prop_stutter_invariant().is_true();
+        }
 
       // Drop or keep matched automata depending on the --invert option
       if (matched == opt_invert)
diff --git a/tests/core/readsave.test b/tests/core/readsave.test
index eb790e048..567494549 100755
--- a/tests/core/readsave.test
+++ b/tests/core/readsave.test
@@ -930,6 +930,7 @@ State: 1
 EOF
 test `autfilt -c --is-inherently-weak input7` = 1
 test `autfilt -c --is-weak input7` = 0
+test `autfilt -c --is-stutter-invariant input7` = 1
 autfilt --check input7 -H >output7
 cat >expected7 <<EOF
 HOA: v1
diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test
index 467a6efd1..4cd1ed508 100755
--- a/tests/core/stutter-tgba.test
+++ b/tests/core/stutter-tgba.test
@@ -86,6 +86,7 @@ run 0 $ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2
 grep '!stutter-invariant' input.2
 # HOA v1 has no name, so we use "stutter-sensitive"
 run 0 $autfilt --check=stutter input > input.2
+test `autfilt -c -v --is-stutter-invariant input` = 1
 grep stutter-sensitive input.2
 
 $ltl2tgba 'F(a & X(!a & Gb))' > input
@@ -93,6 +94,7 @@ grep stutter-invariant input && exit 1
 grep deterministic input && exit 1
 # This will involve a complementation
 run 0 $autfilt --check=stutter input > input.2
+test `autfilt -c --is-stutter-invariant input` = 1
 grep ' stutter-invariant' input.2
 
 $ltl2tgba 'F(a & X(a & Gb))' > input
@@ -100,5 +102,6 @@ grep stutter input && exit 1
 grep deterministic input && exit 1
 # This will involve a complementation
 run 0 $autfilt -H1.1 --check=stutter input > input.2
+test `autfilt -c --is-stutter-invariant input` = 0
 grep '!deterministic' input.2
 grep '!stutter-invariant' input.2