timer: add a stopwatch for timing a simple operation
* src/misc/timer.hh (stopwatch): New class, implemented on top of C++11's std::chrono::high_resolution_clock. * src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/bin/ltlcross.cc: Use it in lieu of gethrxtime(), so we do not need to distribute gethrxtime anymore.
This commit is contained in:
parent
8d947a8782
commit
a4f951facc
4 changed files with 41 additions and 17 deletions
|
|
@ -24,7 +24,6 @@
|
|||
|
||||
#include <argp.h>
|
||||
#include "error.h"
|
||||
#include "gethrxtime.h"
|
||||
|
||||
#include "common_setup.hh"
|
||||
#include "common_finput.hh"
|
||||
|
|
@ -40,6 +39,7 @@
|
|||
#include "tgbaalgos/stats.hh"
|
||||
#include "tgba/bddprint.hh"
|
||||
#include "misc/optionmap.hh"
|
||||
#include "misc/timer.hh"
|
||||
#include "dstarparse/public.hh"
|
||||
#include "tgbaalgos/sccinfo.hh"
|
||||
|
||||
|
|
@ -305,14 +305,11 @@ namespace
|
|||
if (!daut)
|
||||
error(2, 0, "failed to read automaton from %s", filename);
|
||||
|
||||
const xtime_t before = gethrxtime();
|
||||
|
||||
spot::stopwatch sw;
|
||||
sw.start();
|
||||
auto nba = spot::dstar_to_tgba(daut);
|
||||
auto aut = post.run(nba, 0);
|
||||
|
||||
const xtime_t after = gethrxtime();
|
||||
const double prec = XTIME_PRECISION;
|
||||
const double conversion_time = (after - before) / prec;
|
||||
const double conversion_time = sw.stop();
|
||||
|
||||
switch (format)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -24,7 +24,6 @@
|
|||
|
||||
#include <argp.h>
|
||||
#include "error.h"
|
||||
#include "gethrxtime.h"
|
||||
|
||||
#include "common_setup.hh"
|
||||
#include "common_r.hh"
|
||||
|
|
@ -44,6 +43,7 @@
|
|||
#include "tgbaalgos/translate.hh"
|
||||
#include "tgba/bddprint.hh"
|
||||
#include "misc/optionmap.hh"
|
||||
#include "misc/timer.hh"
|
||||
|
||||
const char argp_program_doc[] ="\
|
||||
Translate linear-time formulas (LTL/PSL) into Büchi automata.\n\n\
|
||||
|
|
@ -223,11 +223,10 @@ namespace
|
|||
process_formula(const spot::ltl::formula* f,
|
||||
const char* filename = 0, int linenum = 0)
|
||||
{
|
||||
const xtime_t before = gethrxtime();
|
||||
spot::stopwatch sw;
|
||||
sw.start();
|
||||
auto aut = trans.run(&f);
|
||||
const xtime_t after = gethrxtime();
|
||||
const double prec = XTIME_PRECISION;
|
||||
const double translation_time = (after - before) / prec;
|
||||
const double translation_time = sw.stop();
|
||||
|
||||
// This should not happen, because the parser we use can only
|
||||
// read PSL/LTL formula, but since our ltl::formula* type can
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@
|
|||
#include <unistd.h>
|
||||
#include <sys/wait.h>
|
||||
#include "error.h"
|
||||
#include "gethrxtime.h"
|
||||
#include "argmatch.h"
|
||||
|
||||
#include "common_setup.hh"
|
||||
|
|
@ -61,6 +60,7 @@
|
|||
#include "misc/hash.hh"
|
||||
#include "misc/random.hh"
|
||||
#include "misc/tmpfile.hh"
|
||||
#include "misc/timer.hh"
|
||||
|
||||
// Disable handling of timeout on systems that miss kill() or alarm().
|
||||
// For instance MinGW.
|
||||
|
|
@ -892,9 +892,10 @@ namespace
|
|||
std::string cmd = command.str();
|
||||
std::cerr << "Running [" << l << translator_num << "]: "
|
||||
<< cmd << std::endl;
|
||||
xtime_t before = gethrxtime();
|
||||
spot::stopwatch sw;
|
||||
sw.start();
|
||||
int es = exec_with_timeout(cmd.c_str());
|
||||
xtime_t after = gethrxtime();
|
||||
double duration = sw.stop();
|
||||
|
||||
const char* status_str = 0;
|
||||
|
||||
|
|
@ -1043,8 +1044,7 @@ namespace
|
|||
statistics* st = &(*fstats)[translator_num];
|
||||
st->status_str = status_str;
|
||||
st->status_code = es;
|
||||
double prec = XTIME_PRECISION;
|
||||
st->time = (after - before) / prec;
|
||||
st->time = duration;
|
||||
|
||||
// Compute statistics.
|
||||
if (res)
|
||||
|
|
|
|||
|
|
@ -29,6 +29,7 @@
|
|||
# include <iosfwd>
|
||||
# include <string>
|
||||
# include <map>
|
||||
# include <chrono>
|
||||
# if SPOT_HAVE_SYS_TIMES_H
|
||||
# include <sys/times.h>
|
||||
# endif
|
||||
|
|
@ -40,6 +41,33 @@ namespace spot
|
|||
/// \addtogroup misc_tools
|
||||
/// @{
|
||||
|
||||
|
||||
/// \brief A simple stopwatch
|
||||
struct stopwatch
|
||||
{
|
||||
protected:
|
||||
typedef std::chrono::high_resolution_clock clock;
|
||||
clock::time_point start_;
|
||||
public:
|
||||
/// Marks the start if the measurement
|
||||
void start()
|
||||
{
|
||||
start_ = clock::now();
|
||||
}
|
||||
|
||||
/// \brief Returns the elapsed duration in seconds.
|
||||
///
|
||||
/// May be called multiple times, and will always return the
|
||||
/// duration since the last call to start().
|
||||
double stop()
|
||||
{
|
||||
auto t = clock::now();
|
||||
typedef std::chrono::duration<double> seconds;
|
||||
return std::chrono::duration_cast<seconds>(t - start_).count();
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
/// A structure to record elapsed time in clock ticks.
|
||||
struct time_info
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue