From 40c457b6267405d2f379c8c576d0ec09caeca0ab Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 16 Dec 2014 11:25:43 +0100
Subject: [PATCH] autfilt: add support for --name, %M, and %m

* src/bin/autfilt.cc: Here.
* src/tgbaalgos/stats.cc: Do not segfault if format is nullptr.
* src/tgbatest/readsave.test: Exercise --name, %M, and %m.
---
 src/bin/autfilt.cc         | 50 +++++++++++++++++++++++++++++++++++---
 src/tgbaalgos/stats.cc     |  3 ++-
 src/tgbatest/readsave.test | 23 ++++++++++++++++++
 3 files changed, 71 insertions(+), 5 deletions(-)

diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc
index 4d61863e1..1a22f2b11 100644
--- a/src/bin/autfilt.cc
+++ b/src/bin/autfilt.cc
@@ -72,6 +72,7 @@ Exit status:\n\
 #define OPT_IS_DETERMINISTIC 12
 #define OPT_STATES 17
 #define OPT_COUNT 18
+#define OPT_NAME 19
 
 static const argp_option options[] =
   {
@@ -97,6 +98,8 @@ 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 },
+    { "name", OPT_NAME, "FORMAT", OPTION_ARG_OPTIONAL,
+      "set the name of the output automaton (default: %M)", 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 },
@@ -112,6 +115,8 @@ static const argp_option options[] =
       "name of the input file", 0 },
     { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "location in the input file", 0 },
+    { "%M, %m", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
+      "name of the automaton (as specified in the HOA format)", 0 },
     { "%S, %s", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
       "number of states", 0 },
     { "%E, %e", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
@@ -187,6 +192,7 @@ static bool opt_is_complete = false;
 static bool opt_is_deterministic = false;
 static bool opt_invert = false;
 static range opt_states = { 0, std::numeric_limits<int>::max() };
+static const char* opt_name = nullptr;
 
 static int
 to_int(const char* s)
@@ -273,6 +279,11 @@ parse_opt(int key, char* arg, struct argp_state*)
 	  format = Lbtt;
 	}
       break;
+    case OPT_NAME:
+      if (arg)
+	opt_name = arg;
+      else
+	opt_name = "%M";
     case OPT_MERGE:
       opt_merge = true;
       break;
@@ -362,6 +373,8 @@ namespace
       declare('F', &filename_);
       declare('f', &filename_);	// Override the formula printer.
       declare('L', &haut_loc_);
+      declare('M', &haut_name_);
+      declare('m', &aut_name_);
       declare('S', &haut_states_);
       declare('T', &haut_trans_);
     }
@@ -391,7 +404,23 @@ namespace
 	  haut_states_ = s.states;
 	  haut_edges_ = s.transitions;
 	}
-      else if (has('S'))
+      if (has('M'))
+	{
+	  auto n = haut->aut->get_named_prop<std::string>("automaton-name");
+	  if (n)
+	    haut_name_ = *n;
+	  else
+	    haut_name_.val().clear();
+	}
+      if (has('m'))
+	{
+	  auto n = aut->get_named_prop<std::string>("automaton-name");
+	  if (n)
+	    aut_name_ = *n;
+	  else
+	    aut_name_.val().clear();
+	}
+      if (has('S'))
 	{
 	  haut_states_ = haut->aut->num_states();
 	}
@@ -407,6 +436,8 @@ namespace
 
   private:
     spot::printable_value<const char*> filename_;
+    spot::printable_value<std::string> haut_name_;
+    spot::printable_value<std::string> aut_name_;
     spot::printable_value<unsigned> haut_states_;
     spot::printable_value<unsigned> haut_edges_;
     spot::printable_value<unsigned> haut_trans_;
@@ -415,15 +446,17 @@ namespace
     spot::printable_value<spot::location> haut_loc_;
   };
 
-
   class hoa_processor: public job_processor
   {
-  public:
+  private:
     spot::postprocessor& post;
     hoa_stat_printer statistics;
+    std::ostringstream name;
+    hoa_stat_printer namer;
+  public:
 
     hoa_processor(spot::postprocessor& post)
-      : post(post), statistics(std::cout, stats)
+      : post(post), statistics(std::cout, stats), namer(name, opt_name)
     {
     }
 
@@ -477,6 +510,15 @@ namespace
 
       const double conversion_time = sw.stop();
 
+      // Name the output automaton.
+      if (opt_name)
+	{
+	  name.str("");
+	  namer.print(haut, aut, filename, conversion_time);
+	  aut->set_named_prop("automaton-name", new std::string(name.str()));
+	}
+
+      // Output it.
       switch (format)
 	{
 	case Count:
diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc
index 18e028146..6247a3dfd 100644
--- a/src/tgbaalgos/stats.cc
+++ b/src/tgbaalgos/stats.cc
@@ -154,7 +154,8 @@ namespace spot
     declare('S', &scc_);	// Historical.  Deprecated.  Use %c instead.
     declare('t', &trans_);
     set_output(os);
-    prime(format);
+    if (format)
+      prime(format);
   }
 
   std::ostream&
diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test
index 5c32109dd..4e74b73f9 100755
--- a/src/tgbatest/readsave.test
+++ b/src/tgbatest/readsave.test
@@ -27,6 +27,8 @@
 set -e
 
 autfilt=../../bin/autfilt
+ltl2tgba=../../bin/ltl2tgba
+randltl=../../bin/randltl
 
 cat >input <<\EOF
 HOA: v1
@@ -102,3 +104,24 @@ run 0 ../../bin/autfilt -F input --isomorph stdout
 # But this second output should be the same as the first
 run 0 $autfilt --hoa stdout > stdout2
 diff stdout stdout2
+
+# Find formula that can be translated into a 3-state automaton, and
+# exercise both %M and %m.
+$randltl -n -1 a b |
+    $ltl2tgba -H -F - |
+    $autfilt --states=3 --name='%M, %S states' --stats='<%m>, %t' |
+    head -n 10 > output
+cat output
+cat >expected <<EOF
+<F(b | GF!a), 3 states>, 13
+<XFb, 3 states>, 6
+<XF!b, 3 states>, 6
+<G!b & XF!a, 3 states>, 6
+<F(b | GFa), 3 states>, 13
+<F(Ga | XG(!a & Fb)), 3 states>, 14
+<FG!b & F(b | GFb), 3 states>, 6
+<Ga | G!a, 3 states>, 4
+<a | G((!a & !b) | (a & b)), 3 states>, 9
+<Fb U G!a, 3 states>, 13
+EOF
+diff output expected