diff --git a/NEWS b/NEWS index d91043dff..930eb576d 100644 --- a/NEWS +++ b/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 diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 0c7c722f0..03d7d01c3 100644 --- a/bin/common_aoutput.cc +++ b/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(); diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index d9df1fb45..e28d4d776 100644 --- a/bin/common_aoutput.hh +++ b/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 haut_trans_; spot::printable_value haut_acc_; spot::printable_value haut_scc_; + spot::printable_value csv_prefix_; + spot::printable_value 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); }; diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 5731b5fc0..1707a3b67 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche +// 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; } }; diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 7de127fe9..2bf71b0cb 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement +// 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(); diff --git a/tests/core/ltl2tgba.test b/tests/core/ltl2tgba.test index bdb114092..ec556f23c 100755 --- a/tests/core/ltl2tgba.test +++ b/tests/core/ltl2tgba.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire -# de Recherche et Développement de l'Epita (LRDE). +# Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 +# 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. diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index d009e21eb..70e53a331 100755 --- a/tests/core/ltldo.test +++ b/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