From bfbe5b448b4bbf2c47b1df2f48ced167982e8529 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 21 Aug 2013 16:30:26 +0200 Subject: [PATCH] stats: add %r to display run-time * src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh: Add support for printing run-time. * src/bin/ltl2tgba.cc, src/bin/dstar2tgba.cc: Compute the run-time and show the option. * NEWS: Mention it. --- NEWS | 4 +++- src/bin/dstar2tgba.cc | 18 ++++++++++++++---- src/bin/ltl2tgba.cc | 10 +++++++++- src/tgbaalgos/stats.cc | 5 ++++- src/tgbaalgos/stats.hh | 6 ++++-- 5 files changed, 34 insertions(+), 9 deletions(-) diff --git a/NEWS b/NEWS index a6cbba013..404072776 100644 --- a/NEWS +++ b/NEWS @@ -54,7 +54,9 @@ New in spot 1.1.4a (not relased) new dstar2tgba command. Additionally, the %p escape can now be used to show whether the - output automaton is complete. + output automaton is complete, and the %r escape will give the + number of seconds spent building the output automaton (excluding + the time spent parsing the input). * All the parsers implemented in Spot now use the same type to store locations. diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 21d2d29d6..08b5451ed 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -24,6 +24,7 @@ #include #include "error.h" +#include "gethrxtime.h" #include "common_setup.hh" #include "common_finput.hh" @@ -102,6 +103,9 @@ static const argp_option options[] = "1 if the output is deterministic, 0 otherwise", 0 }, { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "1 if the output is complete, 0 otherwise", 0 }, + { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "conversion time (including post-processings, but not parsing)" + " in seconds", 0 }, { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, /**************************************************/ @@ -222,7 +226,7 @@ namespace /// to be output. std::ostream& print(const spot::dstar_aut* daut, const spot::tgba* aut, - const char* filename) + const char* filename, double run_time) { filename_ = filename; @@ -254,7 +258,7 @@ namespace daut_scc_ = m.scc_count(); } - return this->spot::stat_printer::print(aut); + return this->spot::stat_printer::print(aut, 0, run_time); } private: @@ -302,9 +306,16 @@ namespace { error(2, 0, "failed to read automaton from %s", filename); } + + const xtime_t before = gethrxtime(); + spot::tgba* nba = spot::dstar_to_tgba(daut); const spot::tgba* aut = post.run(nba, 0); + const xtime_t after = gethrxtime(); + const double prec = XTIME_PRECISION; + const double conversion_time = (after - before) / prec; + if (utf8) { spot::tgba* a = const_cast(aut); @@ -336,8 +347,7 @@ namespace spot::never_claim_reachable(std::cout, aut); break; case Stats: - // FIXME: filename - statistics.print(daut, aut, filename) << "\n"; + statistics.print(daut, aut, filename, conversion_time) << "\n"; break; } delete aut; diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 5b87b22f8..d17ee4d85 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -24,6 +24,7 @@ #include #include "error.h" +#include "gethrxtime.h" #include "common_setup.hh" #include "common_r.hh" @@ -93,6 +94,9 @@ static const argp_option options[] = "1 if the automaton is deterministic, 0 otherwise", 0 }, { "%p", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "1 if the automaton is complete, 0 otherwise", 0 }, + { "%r", 0, 0, OPTION_DOC | OPTION_NO_USAGE, + "translation time (including pre- and post-processings, but not parsing)" + " in seconds", 0 }, { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE, "a single %", 0 }, /**************************************************/ @@ -201,7 +205,11 @@ namespace process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { + const xtime_t before = gethrxtime(); const spot::tgba* aut = trans.run(&f); + const xtime_t after = gethrxtime(); + const double prec = XTIME_PRECISION; + const double translation_time = (after - before) / prec; // This should not happen, because the parser we use can only // read PSL/LTL formula, but since our ltl::formula* type can @@ -246,7 +254,7 @@ namespace spot::never_claim_reachable(std::cout, aut, f); break; case Stats: - statistics.print(aut, f) << "\n"; + statistics.print(aut, f, translation_time) << "\n"; break; } delete aut; diff --git a/src/tgbaalgos/stats.cc b/src/tgbaalgos/stats.cc index a71726449..175552ffd 100644 --- a/src/tgbaalgos/stats.cc +++ b/src/tgbaalgos/stats.cc @@ -148,6 +148,7 @@ namespace spot declare('f', &form_); declare('n', &nondetstates_); declare('p', &complete_); + declare('r', &run_time_); declare('s', &states_); declare('S', &scc_); // Historical. Deprecated. Use %c instead. declare('t', &trans_); @@ -157,9 +158,11 @@ namespace spot std::ostream& stat_printer::print(const tgba* aut, - const ltl::formula* f) + const ltl::formula* f, + double run_time) { form_ = f; + run_time_ = run_time; if (has('t')) { diff --git a/src/tgbaalgos/stats.hh b/src/tgbaalgos/stats.hh index a8a58c4b8..3c4fa41d6 100644 --- a/src/tgbaalgos/stats.hh +++ b/src/tgbaalgos/stats.hh @@ -83,9 +83,10 @@ namespace spot /// \brief print the configured statistics. /// /// The \a f argument is not needed if the Formula does not need - /// to be output. + /// to be output, and so is \a run_time). std::ostream& - print(const tgba* aut, const ltl::formula* f = 0); + print(const tgba* aut, const ltl::formula* f = 0, + double run_time = -1.); private: const char* format_; @@ -99,6 +100,7 @@ namespace spot printable_value nondetstates_; printable_value deterministic_; printable_value complete_; + printable_value run_time_; }; /// @}