diff --git a/ChangeLog b/ChangeLog index a3938f8e2..0d556cb2e 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2004-11-29 Alexandre Duret-Lutz + + * src/misc/timer.hh, src/misc/timer.cc: New files. + * src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. + * src/tgbatest/randtgba.cc: Use time_map to measure the algorithms. + Add the -R option. + * src/sanity/style.sh: Let me use `for (.*;;)'. + 2004-11-29 Denis Poitrenaud * src/tgbaalgos/tau03opt.cc: Add a first version of the computation of diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 901de5f2c..718071e94 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -35,6 +35,7 @@ misc_HEADERS = \ minato.hh \ modgray.hh \ random.hh \ + timer.hh \ version.hh noinst_LTLIBRARIES = libmisc.la @@ -46,4 +47,5 @@ libmisc_la_SOURCES = \ minato.cc \ modgray.cc \ random.cc \ + timer.cc \ version.cc diff --git a/src/misc/timer.cc b/src/misc/timer.cc new file mode 100644 index 000000000..a3b4566c7 --- /dev/null +++ b/src/misc/timer.cc @@ -0,0 +1,84 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#include "timer.hh" +#include +#include + +namespace spot +{ + + std::ostream& + timer_map::print(std::ostream& os) const + { + time_info total; + for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i) + { + total.utime += i->second.first.utime(); + total.stime += i->second.first.stime(); + } + clock_t grand_total = total.utime + total.stime; + + os << std::setw(33) << "" + << "| user time | sys. time | total |" + << std::endl + << std::setw(33) << "name " + << "| ticks % | tics % | tics % | n" + << std::endl + << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl; + for (tm_type::const_iterator i = tm.begin(); i != tm.end(); ++i) + { + const spot::timer& t = i->second.first; + os << std::setw(32) << i->first << " |" + << std::setw(6) << t.utime() + << std::setw(5) << (total.utime ? + 100.0 * t.utime() / total.utime : 0) + << " |" + << std::setw(6) << t.stime() + << std::setw(5) << (total.stime ? + 100.0 * t.stime() / total.stime : 0) + << " |" + << std::setw(6) << t.utime() + t.stime() + << std::setw(5) << (grand_total ? + (100.0 * (t.utime() + t.stime()) / + grand_total) : 0) + << " |" + << std::setw(4) << i->second.second + << std::endl; + } + os << std::setw(79) << std::setfill('-') << "" << std::setfill(' ') + << std::endl + << std::setw(32) << "TOTAL" << " |" + << std::setw(6) << total.utime + << std::setw(5) << 100 + << " |" + << std::setw(6) << total.stime + << std::setw(5) << 100 + << " |" + << std::setw(6) << grand_total + << std::setw(5) << 100 + << " |" + << std::endl; + return os; + } + +} diff --git a/src/misc/timer.hh b/src/misc/timer.hh new file mode 100644 index 000000000..9f27383af --- /dev/null +++ b/src/misc/timer.hh @@ -0,0 +1,183 @@ +// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// département Systèmes Répartis Coopératifs (SRC), Université Pierre +// et Marie Curie. +// +// 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 2 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 Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_MISC_TIMER_HH +# define SPOT_MISC_TIMER_HH + +# include +# include +# include +# include + +namespace spot +{ + /// \addtogroup misc_tools + /// @{ + + /// A structure to record elapsed time in clock ticks. + struct time_info + { + time_info() + : utime(), stime(0) + { + } + clock_t utime; + clock_t stime; + }; + + /// A timekeeper that accumulate interval of time. + class timer + { + public: + + /// Start a time interval. + void + start() + { + struct tms tmp; + times(&tmp); + start_.utime = tmp.tms_utime; + start_.stime = tmp.tms_stime; + } + + /// Stop a time interval and update the sum of all intervals. + void + stop() + { + struct tms tmp; + times(&tmp); + total_.utime += tmp.tms_utime - start_.utime; + total_.stime += tmp.tms_stime - start_.stime; + } + + /// \brief Return the user time of all accumulated interval. + /// + /// Any time interval that has been start()ed but not stop()ed + /// will not be accounted for. + clock_t + utime() const + { + return total_.utime; + } + + /// \brief Return the system time of all accumulated interval. + /// + /// Any time interval that has been start()ed but not stop()ed + /// will not be accounted for. + clock_t + stime() const + { + return total_.stime; + } + + protected: + time_info start_; + time_info total_; + }; + + /// \brief A map of timer, where each timer has a name. + /// + /// Timer_map also keeps track of the number of measures each timer + /// has performed. + class timer_map + { + public: + + /// \brief Start a timer with name \a name. + /// + /// The timer is created if it did not exist already. + /// Once started, a timer should be either stop()ed or + /// cancel()ed. + void + start(const std::string& name) + { + item_type& it = tm[name]; + it.first.start(); + ++it.second; + } + + /// \brief Stop timer \a name. + /// + /// The timer must have been previously started with start(). + void + stop(const std::string& name) + { + tm[name].first.stop(); + } + + /// \brief Cancel timer \a name. + /// + /// The timer must have been previously started with start(). + /// + /// This cancel only the current measure. (Previous measures + /// recorded by the timer are preserved.) When a timer that has + /// not done any measure is canceled, it is removed from the map. + void + cancel(const std::string& name) + { + tm_type::iterator i = tm.find(name); + assert(i != tm.end()); + assert(0 < i->second.second); + if (0 == --i->second.second) + tm.erase(i); + } + + /// Return the timer \a name. + const spot::timer& + timer(const std::string& name) const + { + tm_type::const_iterator i = tm.find(name); + assert(i != tm.end()); + return i->second.first; + } + + /// Return the timer \a name. + spot::timer& + timer(const std::string& name) + { + return tm[name].first; + } + + /// \brief Whether there is no timer in the map. + /// + /// If empty() return true, then either no timer where ever + /// started, or all started timers were canceled without + /// completing any measure. + bool + empty() const + { + return tm.empty(); + } + + /// Format information about all timers in a table. + std::ostream& + print(std::ostream& os) const; + + protected: + typedef std::pair item_type; + typedef std::map tm_type; + tm_type tm; + }; + + /// @} +} + +#endif // SPOT_MISC_ESCAPE_HH diff --git a/src/sanity/style.test b/src/sanity/style.test index f771c4cb1..d1a677294 100755 --- a/src/sanity/style.test +++ b/src/sanity/style.test @@ -110,7 +110,7 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do grep '[ ];' $tmp && diag 'No space before semicolon.' - grep -v 'for (;;)' $tmp | grep ';[^ ")]' && + grep -v 'for (.*;;)' $tmp | grep ';[^ ")]' && diag 'Must have space or newline after semicolon.' grep '}.*}' $tmp && diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 8f8c8dfbc..20eb69398 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -33,6 +33,7 @@ #include "tgbaalgos/dotty.hh" #include "misc/random.hh" #include "tgba/tgbatba.hh" +#include "misc/timer.hh" #include "tgbaalgos/emptiness.hh" #include "tgbaalgos/emptiness_stats.hh" @@ -45,6 +46,65 @@ #include "tgbaalgos/tau03opt.hh" #include "tgbaalgos/replayrun.hh" + +spot::emptiness_check* +couvreur99_cons(const spot::tgba* a) +{ + return new spot::couvreur99_check(a); +} + +spot::emptiness_check* +couvreur99_shy_cons(const spot::tgba* a) +{ + return new spot::couvreur99_check_shy(a); +} + +spot::emptiness_check* +bsh_ms_cons(const spot::tgba* a) +{ + return spot::bit_state_hashing_magic_search(a, 4096); +} + +spot::emptiness_check* +bsh_se05_cons(const spot::tgba* a) +{ + return spot::bit_state_hashing_se05_search(a, 4096); +} + +struct ec_algo +{ + const char* name; + spot::emptiness_check* (*construct)(const spot::tgba*); + unsigned int min_acc; + unsigned int max_acc; + bool safe; +}; +ec_algo ec_algos[] = + { + { "couvreur99", couvreur99_cons, 0, -1U, true }, + { "couvreur99_shy", couvreur99_shy_cons, 0, -1U, true }, + { "explicit_magic_search", spot::explicit_magic_search, 0, 1, true }, + { "bit_state_hashing_magic_search", + bsh_ms_cons, 0, 1, false }, + { "explicit_se05", spot::explicit_se05_search, 0, 1, true }, + { "bit_state_hashing_se05", + bsh_se05_cons, 0, 1, false }, + { "explicit_gv04", spot::explicit_gv04_check, 0, 1, true }, + { "explicit_tau03", spot::explicit_tau03_search, 1, -1U, true }, + { "explicit_tau03_opt", spot::explicit_tau03_opt_search, 0, -1U, true }, + }; + +spot::emptiness_check* +cons_emptiness_check(int num, const spot::tgba* a, + const spot::tgba* degen, unsigned int n_acc) +{ + if (n_acc < ec_algos[num].min_acc || n_acc > ec_algos[num].max_acc) + a = degen; + if (a) + return ec_algos[num].construct(a); + return 0; +} + void syntax(char* prog) { @@ -66,6 +126,8 @@ syntax(char* prog) << " -n N number of nodes of the graph [20]" << std::endl << " -r compute and replay acceptance runs (implies -e)" << std::endl + << " -R N repeat each emptiness-check and accepting run " + << "computation N times" << std::endl << " -s N seed for the random number generator" << std::endl << " -t F probability of the atomic propositions to be true" << " [0.5]" << std::endl @@ -275,6 +337,8 @@ main(int argc, char** argv) bool opt_z = false; bool opt_Z = false; + int opt_R = 0; + bool opt_dot = false; int opt_ec = 0; int opt_ec_seed = 0; @@ -341,6 +405,12 @@ main(int argc, char** argv) if (!opt_ec) opt_ec = 1; } + else if (!strcmp(argv[argn], "-R")) + { + if (argc < argn + 2) + syntax(argv[0]); + opt_R = to_int(argv[++argn]); + } else if (!strcmp(argv[argn], "-s")) { if (argc < argn + 2) @@ -371,7 +441,8 @@ main(int argc, char** argv) spot::bdd_dict* dict = new spot::bdd_dict(); - + spot::timer_map tm_ec; + spot::timer_map tm_ar; std::set failed_seeds; do { @@ -397,69 +468,36 @@ main(int argc, char** argv) if (opt_degen && opt_n_acc != 1) degen = new spot::tgba_tba_proxy(a); - std::vector ec_obj; - std::vector ec_name; - std::vector ec_safe; - - ec_obj.push_back(new spot::couvreur99_check(a)); - ec_name.push_back("couvreur99"); - ec_safe.push_back(true); - - ec_obj.push_back(new spot::couvreur99_check_shy(a)); - ec_name.push_back("couvreur99_shy"); - ec_safe.push_back(true); - - if (opt_n_acc <= 1 || opt_degen) - { - spot::tgba* d = opt_n_acc > 1 ? degen : a; - - ec_obj.push_back(spot::explicit_magic_search(d)); - ec_name.push_back("explicit_magic_search"); - ec_safe.push_back(true); - - ec_obj.push_back(spot::bit_state_hashing_magic_search(d, 4096)); - ec_name.push_back("bit_state_hashing_magic_search"); - ec_safe.push_back(false); - - ec_obj.push_back(spot::explicit_se05_search(d)); - ec_name.push_back("explicit_se05"); - ec_safe.push_back(true); - - ec_obj.push_back(spot::bit_state_hashing_se05_search(d, 4096)); - ec_name.push_back("bit_state_hashing_se05"); - ec_safe.push_back(false); - - ec_obj.push_back(spot::explicit_gv04_check(d)); - ec_name.push_back("explicit_gv04"); - ec_safe.push_back(true); - } - - if (opt_n_acc >= 1 || opt_degen) - { - spot::tgba* d = opt_n_acc == 0 ? degen : a; - - ec_obj.push_back(spot::explicit_tau03_search(d)); - ec_name.push_back("explicit_tau03"); - ec_safe.push_back(true); - } - - ec_obj.push_back(spot::explicit_tau03_opt_search(a)); - ec_name.push_back("explicit_tau03_opt"); - ec_safe.push_back(true); - - int n_ec = ec_obj.size(); + int n_alg = sizeof(ec_algos) / sizeof(*ec_algos); + int n_ec = 0; int n_empty = 0; int n_non_empty = 0; int n_maybe_empty = 0; - for (int i = 0; i < n_ec; ++i) + for (int i = 0; i < n_alg; ++i) { - std::string algo = ec_name[i]; + spot::emptiness_check* ec; + spot::emptiness_check_result* res; + ec = cons_emptiness_check(i, a, degen, opt_n_acc); + if (!ec) + continue; + ++n_ec; + std::string algo = ec_algos[i].name; std::cout.width(32); std::cout << algo << ": "; - spot::emptiness_check_result* res = ec_obj[i]->check(); + tm_ec.start(algo); + for (int count = opt_R;;) + { + res = ec->check(); + if (count-- <= 0) + break; + delete res; + delete ec; + ec = cons_emptiness_check(i, a, degen, opt_n_acc); + } + tm_ec.stop(algo); const spot::ec_statistics* ecs = - dynamic_cast(ec_obj[i]); + dynamic_cast(ec); if (opt_z && ecs) ec_stats[algo].count(ecs); if (res) @@ -468,9 +506,23 @@ main(int argc, char** argv) ++n_non_empty; if (opt_replay) { - spot::tgba_run* run = res->accepting_run(); - if (run) + spot::tgba_run* run; + tm_ar.start(algo); + for (int count = opt_R;;) { + run = res->accepting_run(); + if (count-- <= 0 || !run) + break; + delete run; + } + if (!run) + { + tm_ar.cancel(algo); + std::cout << " exists, not computed"; + } + else + { + tm_ar.stop(algo); std::ostringstream s; if (!spot::replay_tgba_run(s, res->automaton(), run)) { @@ -515,17 +567,13 @@ main(int argc, char** argv) } delete run; } - else - { - std::cout << " exists, not computed"; - } } std::cout << std::endl; delete res; } else { - if (ec_safe[i]) + if (ec_algos[i].safe) { std::cout << "empty language" << std::endl; ++n_empty; @@ -539,8 +587,8 @@ main(int argc, char** argv) } if (opt_Z) - ec_obj[i]->print_stats(std::cout); - delete ec_obj[i]; + ec->print_stats(std::cout); + delete ec; } assert(n_empty + n_non_empty + n_maybe_empty == n_ec); @@ -632,6 +680,22 @@ main(int argc, char** argv) print_ar_stats(mar_stats); } + if (opt_z) + { + if (!tm_ec.empty()) + { + std::cout << std::endl + << "emptiness checks cumulated timings:" << std::endl; + tm_ec.print(std::cout); + } + if (!tm_ar.empty()) + { + std::cout << std::endl + << "accepting runs cumulated timings:" << std::endl; + tm_ar.print(std::cout); + } + } + if (!failed_seeds.empty()) { exit_code = 1;