From d17d7469c34db364c93de19a07da337eca968840 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 14 Feb 2015 17:39:51 +0100 Subject: [PATCH] ltlcross: allow appending to files via >>FILENAME Suggested by Joachim Klein. Fixes #57. * src/bin/common_file.hh, src/bin/common_file.cc: New file. * src/bin/Makefile.am: Build them. * src/bin/ltlcross.cc: Use the output_file class. * src/tgbatest/ltlcross3.test: Test >>. * NEWS: mention it. --- NEWS | 7 ++ src/bin/Makefile.am | 2 + src/bin/common_file.cc | 43 ++++++++++++ src/bin/common_file.hh | 54 +++++++++++++++ src/bin/ltlcross.cc | 129 ++++++++++++++++-------------------- src/tgbatest/ltlcross3.test | 19 +++++- 6 files changed, 178 insertions(+), 76 deletions(-) create mode 100644 src/bin/common_file.cc create mode 100644 src/bin/common_file.hh diff --git a/NEWS b/NEWS index 01a87e330..585362ed4 100644 --- a/NEWS +++ b/NEWS @@ -47,6 +47,13 @@ New in spot 1.99a (not yet released) 'ltlcross "spin -f %s>%N" ...'. This feature is much more useful for ltldo. + - For options that take an output filename (i.e., ltlcross's + --save-bogus, --grind, --csv, --json) you can force the file + to be open in append mode (instead of being truncated) by + by prefix the filename with ">>". For instance: + --save-bogus=">>bugs.ltl" + will append to the end of the file. + - There is a parser for the HOA format (http://adl.github.io/hoaf/) available as a spot::hoa_stream_parser object or spot::hoa_parse() function. diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index ce21f16f4..97ad1f8ee 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -32,6 +32,8 @@ libcommon_a_SOURCES = \ common_conv.cc \ common_cout.hh \ common_cout.cc \ + common_file.cc \ + common_file.hh \ common_finput.cc \ common_finput.hh \ common_output.cc \ diff --git a/src/bin/common_file.cc b/src/bin/common_file.cc new file mode 100644 index 000000000..56e5dbeb6 --- /dev/null +++ b/src/bin/common_file.cc @@ -0,0 +1,43 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "common_file.hh" +#include +#include + + +output_file::output_file(const char* name) +{ + std::ios_base::openmode mode = std::ios_base::trunc; + if (name[0] == '>' && name[1] == '>') + { + mode = std::ios_base::app; + append_ = true; + name += 2; + } + if (name[0] == '-' && name[1] == 0) + { + os_ = &std::cout; + return; + } + of_ = new std::ofstream(name, mode); + if (!*of_) + error(2, errno, "cannot open '%s'", name); + os_ = of_; +} diff --git a/src/bin/common_file.hh b/src/bin/common_file.hh new file mode 100644 index 000000000..038a4a72c --- /dev/null +++ b/src/bin/common_file.hh @@ -0,0 +1,54 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#ifndef SPOT_BIN_COMMON_FILE_HH +#define SPOT_BIN_COMMON_FILE_HH + +#include "common_sys.hh" +#include +#include + +class output_file +{ + std::ostream* os_; + std::ofstream* of_ = nullptr; + bool append_ = false; +public: + // Open a file for output. "-" is interpreted as stdout. + // Names that start with ">>" are opened for append. + // The function calls error() on... error. + output_file(const char* name); + + ~output_file() + { + delete of_; + } + + bool append() const + { + return append_; + } + + std::ostream& ostream() + { + return *os_; + } +}; + +#endif // SPOT_BIN_COMMON_FILE_HH diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index f42ac4463..9289131df 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -23,7 +23,6 @@ #include #include #include -#include #include #include #include @@ -36,6 +35,7 @@ #include "common_cout.hh" #include "common_conv.hh" #include "common_trans.hh" +#include "common_file.hh" #include "common_finput.hh" #include "dstarparse/public.hh" #include "hoaparse/public.hh" @@ -123,25 +123,29 @@ static const argp_option options[] = "averaged unless the number is prefixed with '+'", 0 }, /**************************************************/ { 0, 0, 0, 0, "Statistics output:", 7 }, - { "json", OPT_JSON, "FILENAME", OPTION_ARG_OPTIONAL, + { "json", OPT_JSON, "[>>]FILENAME", OPTION_ARG_OPTIONAL, "output statistics as JSON in FILENAME or on standard output", 0 }, - { "csv", OPT_CSV, "FILENAME", OPTION_ARG_OPTIONAL, - "output statistics as CSV in FILENAME or on standard output", 0 }, + { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL, + "output statistics as CSV in FILENAME or on standard output " + "(if '>>' is used to request append mode, the header line is " + "not output)", 0 }, { "omit-missing", OPT_OMIT, 0, 0, "do not output statistics for timeouts or failed translations", 0 }, /**************************************************/ - { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { 0, 0, 0, 0, "Miscellaneous options:", -2 }, { "color", OPT_COLOR, "WHEN", OPTION_ARG_OPTIONAL, "colorize output; WHEN can be 'never', 'always' (the default if " "--color is used without argument), or " "'auto' (the default if --color is not used)", 0 }, - { "grind", OPT_GRIND, "FILENAME", 0, + { "grind", OPT_GRIND, "[>>]FILENAME", 0, "for each formula for which a problem was detected, write a simpler " \ "formula that fails on the same test in FILENAME", 0 }, - { "save-bogus", OPT_BOGUS, "FILENAME", 0, + { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0, "save formulas for which problems were detected in FILENAME", 0 }, { "verbose", OPT_VERBOSE, 0, 0, "print what is being done, for debugging", 0 }, + { 0, 0, 0, 0, "If an output FILENAME is prefixed with '>>', is it open " + "in append mode instead of being truncated.", -1 }, { 0, 0, 0, 0, 0, 0 } }; @@ -149,7 +153,7 @@ const struct argp_child children[] = { { &finput_argp, 0, 0, 1 }, { &trans_argp, 0, 0, 0 }, - { &misc_argp, 0, 0, -1 }, + { &misc_argp, 0, 0, -2 }, { 0, 0, 0, 0 } }; @@ -190,8 +194,8 @@ static bool products_avg = true; static bool opt_omit = false; static bool has_sr = false; // Has Streett or Rabin automata to process. static const char* bogus_output_filename = 0; -static std::ofstream* bogus_output = 0; -static std::ofstream* grind_output = 0; +static output_file* bogus_output = 0; +static output_file* grind_output = 0; static bool verbose = false; static bool ignore_exec_fail = false; static unsigned ignored_exec_fail = 0; @@ -398,9 +402,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_BOGUS: { - bogus_output = new std::ofstream(arg); - if (!*bogus_output) - error(2, errno, "cannot open '%s'", arg); + bogus_output = new output_file(arg); bogus_output_filename = arg; break; } @@ -423,9 +425,7 @@ parse_opt(int key, char* arg, struct argp_state*) allow_dups = true; break; case OPT_GRIND: - grind_output = new std::ofstream(arg); - if (!*grind_output) - error(2, errno, "cannot open '%s'", arg); + grind_output = new output_file(arg); break; case OPT_IGNORE_EXEC_FAIL: ignore_exec_fail = true; @@ -894,7 +894,7 @@ namespace int res = process_formula(f, filename, linenum); if (res && bogus_output) - *bogus_output << input << std::endl; + bogus_output->ostream() << input << std::endl; if (res && grind_output) { std::string bogus = input; @@ -935,7 +935,7 @@ namespace else bogus = spot::ltl::to_string(f); if (bogus_output) - *bogus_output << bogus << std::endl; + bogus_output->ostream() << bogus << std::endl; } } std::cerr << "Smallest bogus mutation found for "; @@ -951,7 +951,7 @@ namespace if (color_opt) std::cerr << reset_color; std::cerr << ".\n\n"; - *grind_output << bogus << std::endl; + grind_output->ostream() << bogus << std::endl; } f->destroy(); @@ -1272,39 +1272,33 @@ print_stats_csv(const char* filename) if (verbose) std::cerr << "info: writing CSV to " << filename << '\n'; - std::ofstream* outfile = 0; - std::ostream* out; - if (!strncmp(filename, "-", 2)) - { - out = &std::cout; - } - else - { - out = outfile = new std::ofstream(filename); - if (!*outfile) - error(2, errno, "cannot open '%s'", filename); - } + output_file outf(filename); + std::ostream& out = outf.ostream(); unsigned ntrans = translators.size(); unsigned rounds = vstats.size(); assert(rounds == formulas.size()); - *out << "\"formula\",\"tool\","; - statistics::fields(*out, !opt_omit, has_sr); - *out << '\n'; + if (!outf.append()) + { + // Do not output the header line if we append to a file. + // (Even if that file was empty initially.) + out << "\"formula\",\"tool\","; + statistics::fields(out, !opt_omit, has_sr); + out << '\n'; + } for (unsigned r = 0; r < rounds; ++r) for (unsigned t = 0; t < ntrans; ++t) if (!opt_omit || vstats[r][t].ok) { - *out << '"'; - spot::escape_rfc4180(*out, formulas[r]); - *out << "\",\""; - spot::escape_rfc4180(*out, translators[t].name); - *out << "\","; - vstats[r][t].to_csv(*out, !opt_omit, has_sr); - *out << '\n'; + out << '"'; + spot::escape_rfc4180(out, formulas[r]); + out << "\",\""; + spot::escape_rfc4180(out, translators[t].name); + out << "\","; + vstats[r][t].to_csv(out, !opt_omit, has_sr); + out << '\n'; } - delete outfile; } static void @@ -1313,56 +1307,44 @@ print_stats_json(const char* filename) if (verbose) std::cerr << "info: writing JSON to " << filename << '\n'; - std::ofstream* outfile = 0; - std::ostream* out; - if (!strncmp(filename, "-", 2)) - { - out = &std::cout; - } - else - { - out = outfile = new std::ofstream(filename); - if (!*outfile) - error(2, errno, "cannot open '%s'", filename); - } + output_file outf(filename); + std::ostream& out = outf.ostream(); unsigned ntrans = translators.size(); unsigned rounds = vstats.size(); assert(rounds == formulas.size()); - *out << "{\n \"tool\": [\n \""; - spot::escape_str(*out, translators[0].name); + out << "{\n \"tool\": [\n \""; + spot::escape_str(out, translators[0].name); for (unsigned t = 1; t < ntrans; ++t) { - *out << "\",\n \""; - spot::escape_str(*out, translators[t].name); + out << "\",\n \""; + spot::escape_str(out, translators[t].name); } - *out << "\"\n ],\n \"formula\": [\n \""; - spot::escape_str(*out, formulas[0]); + out << "\"\n ],\n \"formula\": [\n \""; + spot::escape_str(out, formulas[0]); for (unsigned r = 1; r < rounds; ++r) { - *out << "\",\n \""; - spot::escape_str(*out, formulas[r]); + out << "\",\n \""; + spot::escape_str(out, formulas[r]); } - *out << ("\"\n ],\n \"fields\": [\n \"formula\",\"tool\","); - statistics::fields(*out, !opt_omit, has_sr); - *out << "\n ],\n \"inputs\": [ 0, 1 ],"; - *out << "\n \"results\": ["; + out << ("\"\n ],\n \"fields\": [\n \"formula\",\"tool\","); + statistics::fields(out, !opt_omit, has_sr); + out << "\n ],\n \"inputs\": [ 0, 1 ],"; + out << "\n \"results\": ["; bool notfirst = false; for (unsigned r = 0; r < rounds; ++r) for (unsigned t = 0; t < ntrans; ++t) if (!opt_omit || vstats[r][t].ok) { if (notfirst) - *out << ','; + out << ','; notfirst = true; - *out << "\n [ " << r << ',' << t << ','; - vstats[r][t].to_csv(*out, !opt_omit, has_sr, "null"); - *out << " ]"; + out << "\n [ " << r << ',' << t << ','; + vstats[r][t].to_csv(out, !opt_omit, has_sr, "null"); + out << " ]"; } - *out << "\n ]\n}\n"; - - delete outfile; + out << "\n ]\n}\n"; } int @@ -1451,6 +1433,7 @@ main(int argc, char** argv) } delete bogus_output; + delete grind_output; if (json_output) print_stats_json(json_output); diff --git a/src/tgbatest/ltlcross3.test b/src/tgbatest/ltlcross3.test index 84b6d69ce..4a92fa61b 100755 --- a/src/tgbatest/ltlcross3.test +++ b/src/tgbatest/ltlcross3.test @@ -123,17 +123,19 @@ test $q -eq `expr $p + 12` # Check with Rabin/Streett output +first="should not be erased" +echo "$first" > bug.txt run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ - -f 'X a' --csv=out.csv --save-bogus=bug.txt 2>stderr + -f 'X a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr q=`sed 's/[^,]//g;q' out.csv | wc -c` +test $q -eq `expr $p + 6` grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2 test `grep '"exit code",1' out.csv | wc -l` -eq 2 check_csv out.csv grep 'X a' bug.txt - -test $q -eq `expr $p + 6` +test "`head -n 1 bug.txt`" = "$first" # Support for --ABORT-- in HOA. @@ -143,6 +145,17 @@ grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'error:.*aborted' stderr | wc -l` -eq 2 test `grep '"aborted",-1' out.csv | wc -l` -eq 2 +test 3 = `wc -l < out.csv` +check_csv out.csv + +# The header of CSV file is not output in append mode +run 1 ../../bin/ltlcross 'echo HOA: --ABORT-- %f > %H' \ + -f a --csv='>>out.csv' 2>stderr +grep '"exit_status"' out.csv +grep '"exit_code"' out.csv +test `grep 'error:.*aborted' stderr | wc -l` -eq 2 +test `grep '"aborted",-1' out.csv | wc -l` -eq 4 +test 5 = `wc -l < out.csv` check_csv out.csv