From c6a5de3e23dfa8c9f7c2022feedf9427ba59275a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 4 Jan 2015 12:55:26 +0100
Subject: [PATCH] dstar2tgba: add support for --name and --stats=%m

* src/bin/dstar2tgba.cc: Here.
* src/tgbatest/dstar.test: Test them.
---
 src/bin/dstar2tgba.cc   | 47 +++++++++++++++++++++++++++++++++--------
 src/tgbatest/dstar.test |  7 ++++--
 2 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc
index e6033e148..5c3a3f6b1 100644
--- a/src/bin/dstar2tgba.cc
+++ b/src/bin/dstar2tgba.cc
@@ -42,7 +42,7 @@
 #include "dstarparse/public.hh"
 #include "tgbaalgos/sccinfo.hh"
 
-const char argp_program_doc[] ="\
+static const char argp_program_doc[] ="\
 Convert Rabin and Streett automata into Büchi automata.\n\n\
 This reads the output format of ltl2dstar and will output a \n\
 Transition-based Generalized Büchi Automata in GraphViz's format by default.\n\
@@ -54,6 +54,7 @@ will be output.";
 #define OPT_LBTT 3
 #define OPT_SPOT 4
 #define OPT_STATS 5
+#define OPT_NAME 6
 
 static const argp_option options[] =
   {
@@ -82,6 +83,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", 0,
+      "set the name of the output automaton", 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 "
@@ -122,19 +125,20 @@ static const argp_option options[] =
     { 0, 0, 0, 0, 0, 0 }
   };
 
-const struct argp_child children[] =
+static const struct argp_child children[] =
   {
     { &post_argp, 0, 0, 20 },
     { &misc_argp, 0, 0, -1 },
     { 0, 0, 0, 0 }
   };
 
-enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
-const char* opt_dot = nullptr;
-bool utf8 = false;
-const char* stats = "";
-const char* hoa_opt = 0;
-spot::option_map extra_options;
+enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa };
+static output_format format = Dot;
+static const char* opt_dot = nullptr;
+static const char* stats = "";
+static const char* hoa_opt = nullptr;
+static const char* opt_name = nullptr;
+static spot::option_map extra_options;
 
 static int
 parse_opt(int key, char* arg, struct argp_state*)
@@ -187,6 +191,9 @@ parse_opt(int key, char* arg, struct argp_state*)
 	  format = Lbtt;
 	}
       break;
+    case OPT_NAME:
+      opt_name = arg;
+      break;
     case OPT_SPOT:
       format = Spot;
       break;
@@ -232,6 +239,7 @@ namespace
       declare('f', &filename_);	// Override the formula printer.
       declare('S', &daut_states_);
       declare('T', &daut_trans_);
+      declare('m', &aut_name_);
     }
 
     /// \brief print the configured statistics.
@@ -269,6 +277,15 @@ namespace
       if (has('C'))
 	daut_scc_ = spot::scc_info(daut->aut).scc_count();
 
+      if (has('m'))
+	{
+	  auto n = aut->get_named_prop<std::string>("automaton-name");
+	  if (n)
+	    aut_name_ = *n;
+	  else
+	    aut_name_.val().clear();
+	}
+
       return this->spot::stat_printer::print(aut, 0, run_time);
     }
 
@@ -279,6 +296,7 @@ namespace
     spot::printable_value<unsigned> daut_trans_;
     spot::printable_value<unsigned> daut_acc_;
     spot::printable_value<unsigned> daut_scc_;
+    spot::printable_value<std::string> aut_name_;
   };
 
 
@@ -287,9 +305,12 @@ namespace
   public:
     spot::postprocessor& post;
     dstar_stat_printer statistics;
+    std::ostringstream name;
+    dstar_stat_printer namer;
 
     dstar_processor(spot::postprocessor& post)
-      : post(post), statistics(std::cout, stats)
+      : post(post), statistics(std::cout, stats),
+	namer(name, opt_name)
     {
     }
 
@@ -316,6 +337,14 @@ namespace
       auto aut = post.run(nba, 0);
       const double conversion_time = sw.stop();
 
+      // Name the output automaton.
+      if (opt_name)
+	{
+	  name.str("");
+	  namer.print(daut, aut, filename, conversion_time);
+	  aut->set_named_prop("automaton-name", new std::string(name.str()));
+	}
+
       switch (format)
 	{
 	case Dot:
diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test
index 01eac6de4..5aee1a7c4 100755
--- a/src/tgbatest/dstar.test
+++ b/src/tgbatest/dstar.test
@@ -240,7 +240,8 @@ EOF
 
 diff expected stdout
 
-test "`../../bin/dstar2tgba -D dra.dstar --stats '%s %t %p %d'`" = "3 12 1 1"
+test "`../../bin/dstar2tgba --name=%F -D dra.dstar --stats '%s %t %p %d %m'`" \
+     = "3 12 1 1 dra.dstar"
 
 # This has caused a crash at some point when dealing with 0-sized
 # bitsets to represent acceptance sets.
@@ -256,11 +257,13 @@ State: 0
 Acc-Sig:
 0
 EOF
-run 0 ../../bin/dstar2tgba --dot=t aut.dsa | tee stdout
+run 0 ../../bin/dstar2tgba --name=%F --dot=nt aut.dsa | tee stdout
 
 cat >expected<<EOF
 digraph G {
   rankdir=LR
+  label="aut.dsa"
+  labelloc="t"
   I [label="", style=invis, width=0]
   I -> 0
   0 [label="0"]