diff --git a/NEWS b/NEWS index a7a26b3fb..06a665c97 100644 --- a/NEWS +++ b/NEWS @@ -18,6 +18,15 @@ New in spot 2.4.0.dev (not yet released) deterministic co-Büchi automaton using the new functions [nsa-dnf]_to_dca() described below. + - ltlfilt learned to measure wall-time using --format=%r. + + - ltlfilt learned to measure cpu-time (as opposed to wall-time) using + --format=%R. User or system time, for children or parent, can be + measured separately by adding additional %[LETTER]R options. + The difference between %r (wall-clock time) and %R (CPU time) can + also be used to detect unreliable measurements. See + https://spot.lrde.epita.fr/oaut.html#timing + Library: - Rename three methods of spot::scc_info. New names are clearer. The diff --git a/bin/common_output.cc b/bin/common_output.cc index f141c5d17..e28761159 100644 --- a/bin/common_output.cc +++ b/bin/common_output.cc @@ -209,6 +209,8 @@ namespace declare('b', &bool_size_); declare('f', &fl_); declare('F', &filename_); + declare('R', &timer_); + declare('r', &timer_); declare('L', &line_); declare('s', &size_); declare('h', &class_); @@ -220,8 +222,11 @@ namespace } std::ostream& - print(const formula_with_location& fl) + print(const formula_with_location& fl, spot::process_timer* ptimer) { + if (has('R') || has('r')) + timer_ = *ptimer; + fl_ = &fl; filename_ = fl.filename ? fl.filename : ""; line_ = fl.line; @@ -252,6 +257,7 @@ namespace private: const char* format_; printable_formula fl_; + printable_timer timer_; spot::printable_value filename_; spot::printable_value line_; spot::printable_value prefix_; @@ -317,7 +323,7 @@ parse_opt_output(int key, char* arg, struct argp_state*) static void output_formula(std::ostream& out, - spot::formula f, + spot::formula f, spot::process_timer* ptimer = nullptr, const char* filename = nullptr, int linenum = 0, const char* prefix = nullptr, const char* suffix = nullptr) { @@ -355,7 +361,7 @@ output_formula(std::ostream& out, else { formula_with_location fl = { f, filename, linenum, prefix, suffix }; - format->print(fl); + format->print(fl, ptimer); } } @@ -366,7 +372,7 @@ void } void -output_formula_checked(spot::formula f, +output_formula_checked(spot::formula f, spot::process_timer* ptimer, const char* filename, int linenum, const char* prefix, const char* suffix) { @@ -384,14 +390,14 @@ output_formula_checked(spot::formula f, { outputname.str(""); formula_with_location fl = { f, filename, linenum, prefix, suffix }; - outputnamer->print(fl); + outputnamer->print(fl, ptimer); std::string fname = outputname.str(); auto p = outputfiles.emplace(fname, nullptr); if (p.second) p.first->second.reset(new output_file(fname.c_str())); out = &p.first->second->ostream(); } - output_formula(*out, f, filename, linenum, prefix, suffix); + output_formula(*out, f, ptimer, filename, linenum, prefix, suffix); *out << output_terminator; // Make sure we abort if we can't write to std::cout anymore // (like disk full or broken pipe with SIGPIPE ignored). diff --git a/bin/common_output.hh b/bin/common_output.hh index 5aeb1d81f..a200f1324 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -26,6 +26,7 @@ #include #include #include +#include #include "common_output.hh" #include "common_file.hh" @@ -71,6 +72,7 @@ stream_formula(std::ostream& out, spot::formula f, const char* filename, int linenum); void output_formula_checked(spot::formula f, + spot::process_timer* ptimer = nullptr, const char* filename = nullptr, int linenum = 0, const char* prefix = nullptr, const char* suffix = nullptr); diff --git a/bin/genltl.cc b/bin/genltl.cc index ed88035f2..e4722f89a 100644 --- a/bin/genltl.cc +++ b/bin/genltl.cc @@ -250,13 +250,13 @@ output_pattern(gen::ltl_pattern_id pattern, int n) if (opt_positive || !opt_negative) { - output_formula_checked(f, gen::ltl_pattern_name(pattern), n); + output_formula_checked(f, nullptr, gen::ltl_pattern_name(pattern), n); } if (opt_negative) { std::string tmp = "!"; tmp += gen::ltl_pattern_name(pattern); - output_formula_checked(formula::Not(f), tmp.c_str(), n); + output_formula_checked(formula::Not(f), nullptr, tmp.c_str(), n); } } diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index e29102707..8fe358b6f 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -238,6 +238,13 @@ static const argp_option options[] = "the name of the input file", 0 }, { "%L", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, "the original line number in the input file", 0 }, + { "%r", 0, nullptr, OPTION_DOC | OPTION_NO_USAGE, + "wall-clock time elapsed in seconds (excluding parsing)", 0 }, + { "%R, %[LETTERS]R", 0, nullptr, + OPTION_DOC | OPTION_NO_USAGE, + "CPU time (excluding parsing), in seconds; Add LETTERS to restrict to" + "(u) user time, (s) system time, (p) parent process, " + "or (c) children processes.", 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", 0 }, @@ -796,7 +803,7 @@ namespace p.second, filename, linenum) << ")\n"; } one_match = true; - output_formula_checked(f, filename, linenum, prefix, suffix); + output_formula_checked(f, &timer, filename, linenum, prefix, suffix); ++match_count; } return 0; diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index 6e112516f..4676dd8d2 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -120,7 +120,7 @@ namespace auto mutations = spot::mutate(f, mut_opts, max_output, mutation_nb, opt_sort); for (auto g: mutations) - output_formula_checked(g, filename, linenum, prefix, suffix); + output_formula_checked(g, nullptr, filename, linenum, prefix, suffix); return 0; } }; diff --git a/bin/randltl.cc b/bin/randltl.cc index 2f7970e19..3d27e5b31 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -316,7 +316,7 @@ main(int argc, char** argv) } else { - output_formula_checked(f, nullptr, ++count); + output_formula_checked(f, nullptr, nullptr, ++count); } }; }