From ad9bc644bab16368c8e19576f426f53a680146f5 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Mon, 24 Jul 2017 17:27:23 +0200 Subject: [PATCH] misc/timer: Gather handling of %r and %R options * bin/autcross.cc: Update. * bin/autfilt.cc: Update. * bin/common_aoutput.cc: Gather them. Move process_timer struct. * bin/common_aoutput.hh: Gather them. * bin/common_output.hh: Update. * bin/dstar2tgba.cc: Update. * bin/ltl2tgba.cc: Update. * bin/ltlcross.cc: Update. * bin/ltldo.cc: Update. * bin/ltlfilt.cc: Update. * bin/randaut.cc: Update. * spot/misc/formater.hh: Remove an useless function. * spot/misc/timer.hh: Add process_timer struct definition. * spot/misc/timer.cc: Remove old dead code. * spot/twaalgos/stats.cc: Update. * spot/twaalgos/stats.hh: Update. --- bin/autcross.cc | 5 +++-- bin/autfilt.cc | 2 +- bin/common_aoutput.cc | 34 +++++++++++++++++++++++----------- bin/common_aoutput.hh | 38 +++++++++----------------------------- bin/common_output.hh | 5 ++--- bin/dstar2tgba.cc | 2 +- bin/ltl2tgba.cc | 2 +- bin/ltlcross.cc | 4 ++-- bin/ltldo.cc | 7 ++++--- bin/ltlfilt.cc | 7 +++++++ bin/randaut.cc | 2 +- spot/misc/formater.hh | 11 ----------- spot/misc/timer.cc | 9 --------- spot/misc/timer.hh | 33 +++++++++++++++++++++++++++++++++ spot/twaalgos/stats.cc | 5 +---- spot/twaalgos/stats.hh | 4 +--- 16 files changed, 89 insertions(+), 81 deletions(-) diff --git a/bin/autcross.cc b/bin/autcross.cc index 6fccad3c8..78b3c6000 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -52,6 +52,7 @@ #include #include #include +#include const char argp_program_doc[] ="\ Call several tools that process automata and cross-compare their output \ @@ -377,7 +378,7 @@ namespace std::string cmd = command.str(); std::cerr << "Running [" << l << tool_num << "]: " << cmd << std::endl; - process_timer timer; + spot::process_timer timer; timer.start(); int es = exec_with_timeout(cmd.c_str()); timer.stop(); @@ -459,7 +460,7 @@ namespace stats.status_str = status_str; stats.status_code = es; - stats.time = timer.get_lap_sw(); + stats.time = timer.walltime(); if (res) { stats.ok = true; diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 29cb9f342..0455aa45e 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -991,7 +991,7 @@ namespace int process_automaton(const spot::const_parsed_aut_ptr& haut) override { - process_timer timer; + spot::process_timer timer; timer.start(); // If --stats or --name is used, duplicate the automaton so we diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index ac0a5cf4d..c175da88b 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -384,6 +384,7 @@ hoa_stat_printer::hoa_stat_printer(std::ostream& os, const char* format, declare('F', &filename_); declare('L', &location_); declare('R', &timer_); + declare('r', &timer_); if (input != ltl_input) declare('f', &filename_); // Override the formula printer. declare('h', &output_aut_); @@ -396,11 +397,11 @@ std::ostream& hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, - const char* filename, int loc, process_timer& ptimer, + const char* filename, int loc, + spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix) { - timer_ = ptimer.dt; - double run_time = ptimer.get_lap_sw(); + timer_ = ptimer; filename_ = filename ? filename : ""; csv_prefix_ = csv_prefix ? csv_prefix : ""; @@ -511,7 +512,7 @@ hoa_stat_printer::print(const spot::const_parsed_aut_ptr& haut, if (has('x')) aut_ap_ = aut->ap(); - auto& res = this->spot::stat_printer::print(aut, f, run_time); + auto& res = this->spot::stat_printer::print(aut, f); // Make sure we do not store the automaton until the next one is // printed, as the registered APs will affect how the next // automata are built. @@ -536,7 +537,7 @@ automaton_printer::automaton_printer(stat_style input) void automaton_printer::print(const spot::twa_graph_ptr& aut, // Time for statistics - process_timer& ptimer, + spot::process_timer& ptimer, spot::formula f, // Input location for errors and statistics. const char* filename, @@ -662,11 +663,19 @@ void printable_timer::print(std::ostream& os, const char* pos) const #endif if (*pos != '[') - { - res = val_.get_uscp(true, true, true, true); - os << res / clocks_per_sec; - return; - } + { + if (*pos == 'r') + { + res = val_.walltime(); + os << res; + } + else + { + res = val_.cputime(true, true, true, true); + os << res / clocks_per_sec; + } + return; + } bool user = false; bool system = false; @@ -700,12 +709,15 @@ void printable_timer::print(std::ostream& os, const char* pos) const } while (*pos != ']'); + if (*(pos + 1) == 'r') + percent_error(beg, pos-1); + if (!parent && !children) parent = children = true; if (!user && !system) user = system = true; - res = val_.get_uscp(user, system, children, parent); + res = val_.cputime(user, system, children, parent); os << res / clocks_per_sec; } diff --git a/bin/common_aoutput.hh b/bin/common_aoutput.hh index 678b65bea..bde94d0cd 100644 --- a/bin/common_aoutput.hh +++ b/bin/common_aoutput.hh @@ -74,37 +74,17 @@ struct printable_automaton final: void print(std::ostream& os, const char* pos) const override; }; - -struct process_timer +struct printable_timer final: public spot::printable { - void start() +protected: + spot::process_timer val_; +public: + printable_timer& operator=(const spot::process_timer& val) { - sw.start(); - dt.start(); + val_ = val; + return *this; } - void stop() - { - // sw.stop() --> It always returns the duration since the last call to - // start(). Therefore, it wont't stop timing, moreover, it can be called - // multiple times. - sw_lap_ = sw.stop(); - dt.stop(); - } - double get_lap_sw() - { - return sw_lap_; - } - - spot::timer dt; - spot::stopwatch sw; - double sw_lap_ = 0; -}; - -struct printable_timer final: - public spot::printable_value -{ - using spot::printable_value::operator=; void print(std::ostream& os, const char* pos) const override; }; @@ -166,7 +146,7 @@ public: print(const spot::const_parsed_aut_ptr& haut, const spot::const_twa_graph_ptr& aut, spot::formula f, - const char* filename, int loc, process_timer& ptimer, + const char* filename, int loc, spot::process_timer& ptimer, const char* csv_prefix, const char* csv_suffix); private: @@ -210,7 +190,7 @@ public: void print(const spot::twa_graph_ptr& aut, - process_timer& ptimer, + spot::process_timer& ptimer, spot::formula f = nullptr, // Input location for errors and statistics. const char* filename = nullptr, diff --git a/bin/common_output.hh b/bin/common_output.hh index cff7222a5..5aeb1d81f 100644 --- a/bin/common_output.hh +++ b/bin/common_output.hh @@ -104,11 +104,10 @@ public: std::ostream& print(const spot::const_twa_graph_ptr& aut, - spot::formula f = nullptr, - double run_time = -1.) + spot::formula f = nullptr) { formula_ = f; - return this->spot::stat_printer::print(aut, f, run_time); + return this->spot::stat_printer::print(aut, f); } printable_formula formula_; diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc index db101211a..6eedfd7c9 100644 --- a/bin/dstar2tgba.cc +++ b/bin/dstar2tgba.cc @@ -122,7 +122,7 @@ namespace int process_automaton(const spot::const_parsed_aut_ptr& haut) override { - process_timer timer; + spot::process_timer timer; timer.start(); auto nba = spot::to_generalized_buchi(haut->aut); auto aut = post.run(nba, nullptr); diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc index 44cd1dca4..41383218f 100644 --- a/bin/ltl2tgba.cc +++ b/bin/ltl2tgba.cc @@ -139,7 +139,7 @@ namespace s.c_str()); } - process_timer timer; + spot::process_timer timer; timer.start(); auto aut = trans.run(&f); timer.stop(); diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index d6cb397a1..f6c1f1b3a 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -519,7 +519,7 @@ namespace std::string cmd = command.str(); std::cerr << "Running [" << l << translator_num << "]: " << cmd << std::endl; - process_timer timer; + spot::process_timer timer; timer.start(); int es = exec_with_timeout(cmd.c_str()); timer.stop(); @@ -603,7 +603,7 @@ namespace statistics* st = &(*fstats)[translator_num]; st->status_str = status_str; st->status_code = es; - st->time = timer.get_lap_sw(); + st->time = timer.walltime(); // Compute statistics. if (res) diff --git a/bin/ltldo.cc b/bin/ltldo.cc index 0916e8195..159e56b5e 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -190,7 +190,8 @@ namespace } spot::twa_graph_ptr - translate(unsigned int translator_num, bool& problem, process_timer& timer) + translate(unsigned int translator_num, bool& problem, + spot::process_timer& timer) { output.reset(translator_num); @@ -343,13 +344,13 @@ namespace spot::twa_graph_ptr best_aut = nullptr; std::string best_stats; std::string best_cmdname; - process_timer best_timer; + spot::process_timer best_timer; roundval = round; for (unsigned t = 0; t < ts; ++t) { bool problem; - process_timer timer; + spot::process_timer timer; auto aut = runner.translate(t, problem, timer); if (problem) { diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index d956f049b..e29102707 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -36,6 +36,7 @@ #include "common_range.hh" #include +#include #include #include #include @@ -578,6 +579,10 @@ namespace process_formula(spot::formula f, const char* filename = nullptr, int linenum = 0) override { + spot::process_timer timer; + timer.start(); + + if (opt_max_count >= 0 && match_count >= opt_max_count) { abort_run = true; @@ -773,6 +778,8 @@ namespace if (unique && !unique_set.insert(f).second) matched = false; + timer.stop(); + if (matched) { if (opt->output_define diff --git a/bin/randaut.cc b/bin/randaut.cc index 971f4664b..e4dc0cb03 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -341,7 +341,7 @@ main(int argc, char** argv) for (;;) { - process_timer timer; + spot::process_timer timer; timer.start(); if (ap_count_given.max > 0 diff --git a/spot/misc/formater.hh b/spot/misc/formater.hh index 879cbebd0..753ca0a8b 100644 --- a/spot/misc/formater.hh +++ b/spot/misc/formater.hh @@ -25,8 +25,6 @@ #include #include -#define UNUSED(expr) do { (void)(expr); } while (0) - namespace spot { class printable @@ -88,15 +86,6 @@ namespace spot } }; - // This function was defined to avoid compilation error when - // instantiating function spot::printable_value::print - // because of: os << val_; - std::ostream& operator<<(std::ostream& os, const timer& dt) - { - UNUSED(dt); - return os; - } - /// The default callback simply writes "%c". class printable_id: public printable { diff --git a/spot/misc/timer.cc b/spot/misc/timer.cc index 649f59884..1004aa19b 100644 --- a/spot/misc/timer.cc +++ b/spot/misc/timer.cc @@ -27,15 +27,6 @@ namespace spot { - /* - std::ostream& operator<<(std::ostream& os, const timer& dt) - { - os << "utime<" << dt.utime() << ">, cutime<" << dt.cutime() - << ">, stime<" << dt.stime() << ">, cstime<" << dt.cstime() << '>'; - return os; - } - */ - std::ostream& timer_map::print(std::ostream& os) const diff --git a/spot/misc/timer.hh b/spot/misc/timer.hh index 9b933e0e2..6be339688 100644 --- a/spot/misc/timer.hh +++ b/spot/misc/timer.hh @@ -290,5 +290,38 @@ namespace spot tm_type tm; }; + /// \brief Struct used to start and stop both timer and stopwatch clocks. + typedef struct process_timer + { + void start() + { + walltimer.start(); + cputimer.start(); + } + // sw.stop() --> It always returns the duration since the last call to + // start(). Therefore, it wont't stop timing, moreover, it can be called + // multiple times. + void stop() + { + walltime_lap_ = walltimer.stop(); + cputimer.stop(); + } + + double walltime() const + { + return walltime_lap_; + } + + clock_t cputime(bool user, bool system, bool children, bool parent) const + { + return cputimer.get_uscp(user, system, children, parent); + } + + private: + spot::timer cputimer; + spot::stopwatch walltimer; + double walltime_lap_ = 0; + } process_timer; + /// @} } diff --git a/spot/twaalgos/stats.cc b/spot/twaalgos/stats.cc index 0988b42d1..a68912ad2 100644 --- a/spot/twaalgos/stats.cc +++ b/spot/twaalgos/stats.cc @@ -343,7 +343,6 @@ namespace spot declare('g', &gen_acc_); declare('n', &nondetstates_); declare('p', &complete_); - declare('r', &run_time_); declare('s', &states_); declare('S', &scc_); // Historical. Deprecated. Use %c instead. declare('t', &trans_); @@ -353,11 +352,9 @@ namespace spot } std::ostream& - stat_printer::print(const const_twa_graph_ptr& aut, - formula f, double run_time) + stat_printer::print(const const_twa_graph_ptr& aut, formula f) { form_ = f; - run_time_ = run_time; if (has('t')) { diff --git a/spot/twaalgos/stats.hh b/spot/twaalgos/stats.hh index c9ec7cb0b..be67c66fc 100644 --- a/spot/twaalgos/stats.hh +++ b/spot/twaalgos/stats.hh @@ -103,8 +103,7 @@ namespace spot /// The \a f argument is not needed if the Formula does not need /// to be output, and so is \a run_time). std::ostream& - print(const const_twa_graph_ptr& aut, formula f = nullptr, - double run_time = -1.); + print(const const_twa_graph_ptr& aut, formula f = nullptr); private: const char* format_; @@ -118,7 +117,6 @@ namespace spot printable_value nondetstates_; printable_value deterministic_; printable_value complete_; - printable_value run_time_; printable_value gen_acc_; };