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.
This commit is contained in:
Alexandre Duret-Lutz
parent
7daea8d3cb
commit
d17d7469c3
6 changed files with 178 additions and 76 deletions
7
NEWS
7
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.
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
43
src/bin/common_file.cc
Normal file
43
src/bin/common_file.cc
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include "common_file.hh"
|
||||
#include <error.h>
|
||||
#include <iostream>
|
||||
|
||||
|
||||
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_;
|
||||
}
|
||||
54
src/bin/common_file.hh
Normal file
54
src/bin/common_file.hh
Normal file
|
|
@ -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 <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_BIN_COMMON_FILE_HH
|
||||
#define SPOT_BIN_COMMON_FILE_HH
|
||||
|
||||
#include "common_sys.hh"
|
||||
#include <iosfwd>
|
||||
#include <fstream>
|
||||
|
||||
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
|
||||
|
|
@ -23,7 +23,6 @@
|
|||
#include <string>
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include <fstream>
|
||||
#include <cstdlib>
|
||||
#include <cstdio>
|
||||
#include <argp.h>
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue