From 6a11e149b7271e741741abebc034253db314f3d5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 28 Dec 2016 08:24:08 +0100
Subject: [PATCH] autfilt: add --is-very-weak

* bin/autfilt.cc: Implement --is-very-weak.
* tests/core/strength.test: Test it.
* NEWS: Mention it.
---
 NEWS                     |  2 ++
 bin/autfilt.cc           |  9 +++++++++
 tests/core/strength.test | 35 +++++++++++++++++++++++++++++++++++
 3 files changed, 46 insertions(+)

diff --git a/NEWS b/NEWS
index d01a80c50..d1bd22868 100644
--- a/NEWS
+++ b/NEWS
@@ -11,6 +11,8 @@ New in spot 2.2.2.dev (Not yet released)
     alternating automata, but in any case they should display a
     diagnostic: if you see a crash, please report it.
 
+  * autfilt has a new --is-very-weak filter.
+
   Library:
 
   * A twa is required to have at least one state, the initial state.
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index 4abab6196..09c4246c6 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -110,6 +110,7 @@ enum {
   OPT_IS_UNAMBIGUOUS,
   OPT_IS_WEAK,
   OPT_IS_INHERENTLY_WEAK,
+  OPT_IS_VERY_WEAK,
   OPT_KEEP_STATES,
   OPT_MASK_ACC,
   OPT_MERGE,
@@ -179,6 +180,8 @@ static const argp_option options[] =
       "keep only weak automata", 0 },
     { "is-inherently-weak", OPT_IS_INHERENTLY_WEAK, nullptr, 0,
       "keep only inherently weak automata", 0 },
+    { "is-very-weak", OPT_IS_VERY_WEAK, nullptr, 0,
+      "keep only very-weak automata", 0 },
     { "intersect", OPT_INTERSECT, "FILENAME", 0,
       "keep automata whose languages have an non-empty intersection with"
       " the automaton from FILENAME", 0 },
@@ -412,6 +415,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_very_weak = false;
 static bool opt_is_stutter_invariant = false;
 static bool opt_invert = false;
 static range opt_states = { 0, std::numeric_limits<int>::max() };
@@ -658,6 +662,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_IS_INHERENTLY_WEAK:
       opt_is_inherently_weak = true;
       break;
+    case OPT_IS_VERY_WEAK:
+      opt_is_very_weak = true;
+      break;
     case OPT_IS_STUTTER_INVARIANT:
       opt_is_stutter_invariant = true;
       break;
@@ -1061,6 +1068,8 @@ namespace
         matched &= is_unambiguous(aut);
       if (opt_is_terminal)
         matched &= is_terminal_automaton(aut);
+      else if (opt_is_very_weak)
+        matched &= is_very_weak_automaton(aut);
       else if (opt_is_weak)
         matched &= is_weak_automaton(aut);
       else if (opt_is_inherently_weak)
diff --git a/tests/core/strength.test b/tests/core/strength.test
index c7d6563c4..bc7a7598e 100755
--- a/tests/core/strength.test
+++ b/tests/core/strength.test
@@ -590,6 +590,41 @@ EOF
 diff out expected
 autfilt -q expected
 
+autfilt --is-very-weak in >out
+cat >expected <<EOF
+HOA: v1
+name: "a U b"
+States: 2
+Start: 1
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic
+properties: very-weak
+--BODY--
+State: 0 {0}
+[t] 0
+State: 1
+[1] 0
+[0&!1] 1
+--END--
+HOA: v1
+States: 2
+Start: 1
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc colored
+properties: deterministic very-weak
+--BODY--
+State: 0 {0}
+[t] 1
+State: 1 {0}
+[!0] 1
+--END--
+EOF
+diff out expected
+
 
 cat >input <<EOF
 /* This Büchi automaton is not terminal, because of the