ltldo, ltl2tgba: support %< and %>

* bin/common_aoutput.hh, bin/common_aoutput.cc,
bin/ltl2tgba.cc, bin/ltldo.cc: Add support for %< and %>.
* tests/core/ltl2tgba.test, tests/core/ltldo.test: Test it.
* NEWS: Mention it.

NEWS

@@ -1,5 +1,10 @@
 New in spot 1.99.7a (not yet released)
 
+  Command-line tools:
+
+  * ltl2tgba and ltldo now support %< and %> in the string passed
+    to --stats when reading formulas from a CSV file.
+
   Library:
 
   * Building products with different dictionaries now raise an

bin/common_aoutput.cc

@@ -326,7 +326,9 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
 			 int loc,
 			 // Time and input automaton for statistics
 			 double time,
-			 const spot::const_parsed_aut_ptr& haut)
+			 const spot::const_parsed_aut_ptr& haut,
+			 const char* csv_prefix,
+			 const char* csv_suffix)
 {
   if (opt_check)
     {
@@ -342,7 +344,7 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
   if (opt_name)
     {
       name.str("");
-      namer.print(haut, aut, f, filename, loc, time);
+      namer.print(haut, aut, f, filename, loc, time, csv_prefix, csv_suffix);
       aut->set_named_prop("automaton-name", new std::string(name.str()));
     }
 
@@ -350,7 +352,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
   if (opt_output)
     {
       outputname.str("");
-      outputnamer.print(haut, aut, f, filename, loc, time);
+      outputnamer.print(haut, aut, f, filename, loc, time,
+			csv_prefix, csv_suffix);
       std::string fname = outputname.str();
       auto p = outputfiles.emplace(fname, nullptr);
       if (p.second)
@@ -379,7 +382,8 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
       break;
     case Stats:
       statistics.set_output(*out);
-      statistics.print(haut, aut, f, filename, loc, time) << '\n';
+      statistics.print(haut, aut, f, filename, loc, time,
+		       csv_prefix, csv_suffix) << '\n';
       break;
     }
   flush_cout();

bin/common_aoutput.hh

@@ -88,6 +88,8 @@ public:
 	declare('S', &haut_states_);
 	declare('T', &haut_trans_);
       }
+    declare('<', &csv_prefix_);
+    declare('>', &csv_suffix_);
     declare('F', &filename_);
     declare('L', &location_);
     if (input != ltl_input)
@@ -107,9 +109,12 @@ public:
   print(const spot::const_parsed_aut_ptr& haut,
 	const spot::const_twa_graph_ptr& aut,
 	spot::formula f,
-	const char* filename, int loc, double run_time)
+	const char* filename, int loc, double run_time,
+	const char* csv_prefix, const char* csv_suffix)
   {
     filename_ = filename ? filename : "";
+    csv_prefix_ = csv_prefix ? csv_prefix : "";
+    csv_suffix_ = csv_suffix ? csv_suffix : "";
     if (loc >= 0 && has('L'))
       {
 	std::ostringstream os;
@@ -205,6 +210,8 @@ private:
   spot::printable_value<unsigned> haut_trans_;
   spot::printable_value<unsigned> haut_acc_;
   spot::printable_value<unsigned> haut_scc_;
+  spot::printable_value<const char*> csv_prefix_;
+  spot::printable_value<const char*> csv_suffix_;
 };
 
 
@@ -229,7 +236,9 @@ public:
 	int loc = -1,
 	// Time and input automaton for statistics
 	double time = 0.0,
-	const spot::const_parsed_aut_ptr& haut = nullptr);
+	const spot::const_parsed_aut_ptr& haut = nullptr,
+	const char* csv_prefix = nullptr,
+	const char* csv_suffix = nullptr);
 
   void add_stat(char c, const spot::printable* p);
 };

bin/ltl2tgba.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
-// Développement de l'Epita (LRDE).
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -52,6 +52,12 @@ static const argp_option options[] =
     /**************************************************/
     { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "the formula, in Spot's syntax", 4 },
+    { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the part of the line before the formula if it "
+      "comes from a column extracted from a CSV file", 4 },
+    { "%>", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the part of the line after the formula if it "
+      "comes from a column extracted from a CSV file", 4 },
     /**************************************************/
     { "unambiguous", 'U', nullptr, 0, "output unambiguous automata", 2 },
     { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
@@ -135,7 +141,8 @@ namespace
       auto aut = trans.run(&f);
       const double translation_time = sw.stop();
 
-      printer.print(aut, f, filename, linenum, translation_time, nullptr);
+      printer.print(aut, f, filename, linenum, translation_time, nullptr,
+		    prefix, suffix);
       return 0;
     }
   };

bin/ltldo.cc

@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
-// l'Epita (LRDE).
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -63,6 +63,12 @@ static const argp_option more_o_format[] =
       "tool used for translation", 0 },
     { "%f", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
       "formula translated", 0 },
+    { "%<", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the part of the line before the formula if it "
+      "comes from a column extracted from a CSV file", 4 },
+    { "%>", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE,
+      "the part of the line after the formula if it "
+      "comes from a column extracted from a CSV file", 4 },
     { nullptr, 0, nullptr, 0, nullptr, 0 }
   };
 
@@ -284,7 +290,7 @@ namespace
 	      cmdname = translators[t].name;
 	      roundval = round;
 	      printer.print(aut, f, filename, linenum, translation_time,
-			    nullptr);
+			    nullptr, prefix, suffix);
 	    };
 	}
       spot::cleanup_tmpfiles();

tests/core/ltl2tgba.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
+# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016
-# de Recherche et Développement de l'Epita (LRDE).
+# Laboratoire de Recherche et Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
 # et Marie Curie.
@@ -100,6 +100,8 @@ run 0 ../checkpsl check.txt
 # Make sure False has one acceptance set when generating Büchi automata
 test 1 -eq `ltl2tgba -B false --stats %a`
 
+test "`echo 1,2,a,4 | ltl2tgba -F-/3 --stats='%<,%f,%>'`" = "1,2,a,4"
+
 # In particular, Spot 0.9 would incorrectly reject the sequence:
 # (a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);(a̅b;a̅b;a̅b̅);... in 'G!{(b;1)*;a}'
 # This means the following automaton was incorrectly empty in Spot 0.9.

tests/core/ltldo.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et
+# Copyright (C) 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -48,6 +48,8 @@ run 0 $ltldo -F- -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \
 test -z "`cat output`"
 test 4 = `grep -c warning: stderr`
 
+test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4'
+
 $genltl --and-gf=1..3 |
 run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \
 	     --stats="%T,%R,%f,%s,%t,%e" >output