From 1e84bb1ee742305e050ea5cdbcbe97b459fed564 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 11 Dec 2014 15:15:23 +0100
Subject: [PATCH] autfilt: add a --quiet option

* src/bin/autfilt.cc: Add option.
* src/tgbatest/det.test: Test it.
---
 src/bin/autfilt.cc    |  9 ++++-
 src/tgbatest/det.test | 78 +++++++++++++++++++++++++++----------------
 2 files changed, 58 insertions(+), 29 deletions(-)

diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 8df20f0a5..39c896592 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -89,6 +89,7 @@ static const argp_option options[] =
     { "lbtt", OPT_LBTT, "t", OPTION_ARG_OPTIONAL,
       "LBTT's format (add =t to force transition-based acceptance even"
       " on Büchi automata)", 0 },
+    { "quiet", 'q', 0, 0, "suppress all normal output", 0 },
     { "spin", 's', 0, 0, "Spin neverclaim (implies --ba)", 0 },
     { "spot", OPT_SPOT, 0, 0, "SPOT's format", 0 },
     { "utf8", '8', 0, 0, "enable UTF-8 characters in output "
@@ -151,7 +152,7 @@ static const struct argp_child children[] =
     { 0, 0, 0, 0 }
   };
 
-static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa }
+static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa, Quiet }
   format = Dot;
 static bool one_match = false;
 static const char* stats = "";
@@ -197,6 +198,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case 'M':
       type = spot::postprocessor::Monitor;
       break;
+    case 'q':
+      format = Quiet;
+      break;
     case 's':
       format = Spin;
       if (type != spot::postprocessor::Monitor)
@@ -443,6 +447,9 @@ namespace
 	case Hoa:
 	  spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
 	  break;
+	case Quiet:
+	  // Do not output anything.
+	  break;
 	case Spot:
 	  spot::tgba_save_reachable(std::cout, aut);
 	  break;
diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test
index 410e9cedc..08ce1e20c 100755
--- a/src/tgbatest/det.test
+++ b/src/tgbatest/det.test
@@ -59,39 +59,61 @@ EOF
 $ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out
 diff formulas out
 
-cat >in.tgba <<'EOF'
-acc = "1";
-"1", "2", "a", "1";
-"1", "1", "!a",;
-"2", "3", "a", "1";
-"2", "1", "!a",;
-"3", "3", "a",;
-"3", "1", "!a",;
+cat >in.hoa <<'EOF'
+HOA: v1
+States: 3
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels trans-acc complete deterministic
+--BODY--
+State: 0
+[!0] 0
+[0] 1 {0}
+State: 1
+[!0] 0
+[0] 2 {0}
+State: 2
+[!0] 0
+[0] 2
+--END--
 EOF
 
 # FIXME: we should improve this output
-cat >ex.tgba <<'EOF'
-acc = "0";
-"0", "0", "!a",;
-"0", "1", "a",;
-"0", "3", "!a",;
-"1", "0", "!a",;
-"1", "2", "a",;
-"1", "3", "!a",;
-"3", "3", "!a", "0";
-"2", "0", "!a",;
-"2", "2", "a",;
-"2", "3", "!a",;
-"2", "5", "a",;
-"5", "3", "!a", "0";
-"5", "5", "a", "0";
+cat >ex.hoa <<'EOF'
+HOA: v1
+States: 5
+Start: 0
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0
+[!0] 0
+[0] 1
+[!0] 2
+State: 1
+[!0] 0
+[0] 3
+[!0] 2
+State: 2 {0}
+[!0] 2
+State: 3
+[!0] 0
+[0] 3
+[!0] 2
+[0] 4
+State: 4 {0}
+[!0] 2
+[0] 4
+--END--
 EOF
 
-
-run 0 ../ltl2tgba -b -DC -X in.tgba > out.tgba
-# FIXME: use are-isomorphic once it is available
-diff out.tgba ex.tgba
-
+run 0 ../ltl2tgba -H -DC -XH in.hoa > out.hoa
+run 1 ../../bin/autfilt -q --are-isomorph in.hoa out.hoa
+run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa
 
 run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba
 cat >ex.tgba <<EOF