From f423c424ebffa23b8534933f39b967cf6b3bbd57 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 8 Aug 2016 10:48:06 +0200
Subject: [PATCH] bin: --stats=%H --stats=%h

Part of #91.

* bin/common_aoutput.cc, bin/common_aoutput.hh: implement %H and %h.
* tests/core/readsave.test: Test them.
* NEWS: Mention it.
---
 NEWS                     |  5 +++++
 bin/common_aoutput.cc    | 20 ++++++++++++++++++++
 bin/common_aoutput.hh    | 22 +++++++++++++++++++++-
 tests/core/readsave.test | 11 +++++++++++
 4 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/NEWS b/NEWS
index 515bbe460..ed85be019 100644
--- a/NEWS
+++ b/NEWS
@@ -107,6 +107,11 @@ New in spot 2.0.3a (not yet released)
     is now deprecated.  The option is still here, but hidden and
     undocumented.
 
+  * The --stats option of autfilt, dstar2tgba, ltl2tgba, ltldo,
+    randaut learned to display the output (or input if that makes
+    sense) automaton as a HOA one-liner using %H (or %h), helping to
+    create CSV files contained automata.
+
   * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba)
     that are not used are now reported as they might be typos.
     This ocurred a couple of times in our test-suite.  A similar
diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc
index 285234b45..afeabec4c 100644
--- a/bin/common_aoutput.cc
+++ b/bin/common_aoutput.cc
@@ -152,6 +152,9 @@ static const argp_option io_options[] =
       " minuscules for output):", 4 },
     { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
     { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
+    { "%H, %h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the automaton in HOA format on a single line (use %[opt]H or %[opt]h "
+      "to specify additional options as in --hoa=opt)", 0 },
     { "%M, %m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "name of the automaton", 0 },
     { "%S, %s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@@ -192,6 +195,9 @@ static const argp_option o_options[] =
       "the following interpreted sequences:", 4 },
     { "%F", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, F_doc, 0 },
     { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, L_doc, 0 },
+    { "%h", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the automaton in HOA format on a single line (use %[opt]h "
+      "to specify additional options as in --hoa=opt)", 0 },
     { "%m", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "name of the automaton", 0 },
     { "%s", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
@@ -396,3 +402,17 @@ void automaton_printer::add_stat(char c, const spot::printable* p)
   statistics.declare(c, p);
   outputnamer.declare(c, p);
 }
+
+void printable_automaton::print(std::ostream& os, const char* pos) const
+{
+  std::string options = "l";
+  if (*pos == '[')
+    {
+      ++pos;
+      auto end = strchr(pos, ']');
+      options = std::string(pos, end - pos);
+      options += 'l';
+      pos = end + 1;
+    }
+  print_hoa(os, val_, options.c_str());
+}
diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh
index 9df32fda9..de078dab9 100644
--- a/bin/common_aoutput.hh
+++ b/bin/common_aoutput.hh
@@ -66,6 +66,14 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state* state);
 
 enum stat_style { no_input, aut_input, ltl_input };
 
+
+struct printable_automaton final:
+  public spot::printable_value<spot::const_twa_graph_ptr>
+{
+  using spot::printable_value<spot::const_twa_graph_ptr>::operator=;
+  void print(std::ostream& os, const char* pos) const override;
+};
+
 /// \brief prints various statistics about a TGBA
 ///
 /// This object can be configured to display various statistics
@@ -84,6 +92,7 @@ public:
         declare('C', &haut_scc_);
         declare('E', &haut_edges_);
         declare('G', &haut_gen_acc_);
+        declare('H', &input_aut_);
         declare('M', &haut_name_);
         declare('S', &haut_states_);
         declare('T', &haut_trans_);
@@ -94,6 +103,7 @@ public:
     declare('L', &location_);
     if (input != ltl_input)
       declare('f', &filename_);        // Override the formula printer.
+    declare('h', &output_aut_);
     declare('m', &aut_name_);
     declare('w', &aut_word_);
   }
@@ -121,8 +131,10 @@ public:
         os << loc;
         location_ = os.str();
       }
+    output_aut_ = aut;
     if (haut)
       {
+        input_aut_ = haut->aut;
         if (loc < 0 && has('L'))
           {
             std::ostringstream os;
@@ -190,7 +202,13 @@ public:
             }
         }
 
-    return this->spot::stat_printer::print(aut, f, run_time);
+    auto& res = this->spot::stat_printer::print(aut, f, run_time);
+    // Make sure we do not store the automaton until the next one is
+    // printed, as the registered APs will affect how the next
+    // automata are built.
+    output_aut_ = nullptr;
+    input_aut_ = nullptr;
+    return res;
   }
 
 private:
@@ -207,6 +225,8 @@ private:
   spot::printable_value<unsigned> haut_scc_;
   spot::printable_value<const char*> csv_prefix_;
   spot::printable_value<const char*> csv_suffix_;
+  printable_automaton input_aut_;
+  printable_automaton output_aut_;
 };
 
 
diff --git a/tests/core/readsave.test b/tests/core/readsave.test
index 25d7b4639..bdfbad1b3 100755
--- a/tests/core/readsave.test
+++ b/tests/core/readsave.test
@@ -971,6 +971,17 @@ EOF
 test `autfilt -c --is-inherently-weak input8` = 0
 test `autfilt -c --is-weak input8` = 0
 
+autfilt input8 -Hl >oneline.hoa
+autfilt input8 --stats='%h' >oneline2.hoa
+autfilt input8 --stats='%H' >oneline3.hoa
+autfilt input8 --randomize --stats='%h' >oneline4.hoa
+autfilt input8 --randomize --stats='%H' >oneline5.hoa
+diff oneline.hoa oneline2.hoa
+diff oneline.hoa oneline3.hoa
+diff oneline.hoa oneline4.hoa && exit 1
+diff oneline.hoa oneline5.hoa
+
+
 cat >input9 <<EOF
 HOA: v1
 name: "a U (b U c)"