alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcheck: Record translation time.

Browse source 
* lib/gethrxtime.h, lib/xtime.h: Add extern "C".
* src/bin/Makefile.am (ltlcheck_LDADD): Use LIB_GETHRXTIME.
* src/bin/ltlcheck.cc: Use gethrxtime() to record translation time.
This commit is contained in:
Alexandre Duret-Lutz 2012-10-08 23:22:42 +02:00
parent 756319739b
commit 82babb9d38
4 changed files with 25 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

8
lib/gethrxtime.h
View file

@ -22,6 +22,10 @@
# include "xtime.h" # include "xtime.h"
#ifdef __cplusplus
extern "C" {
#endif
/* Get the current time, as a count of the number of nanoseconds since /* Get the current time, as a count of the number of nanoseconds since
an arbitrary epoch (e.g., the system boot time). Prefer a an arbitrary epoch (e.g., the system boot time). Prefer a
high-resolution clock that is not subject to resetting or high-resolution clock that is not subject to resetting or
@ -34,4 +38,8 @@ static inline xtime_t gethrxtime (void) { return gethrtime (); }
xtime_t gethrxtime (void); xtime_t gethrxtime (void);
# endif # endif
#ifdef __cplusplus
}
#endif
#endif #endif

8
lib/xtime.h
View file

@ -37,6 +37,10 @@ typedef long int xtime_t;
# endif # endif
# endif # endif
#ifdef __cplusplus
extern "C" {
#endif
/* Return an extended time value that contains S seconds and NS /* Return an extended time value that contains S seconds and NS
nanoseconds, without any overflow checking. */ nanoseconds, without any overflow checking. */
static inline xtime_t static inline xtime_t
@ -83,4 +87,8 @@ xtime_nsec (xtime_t t)
return ns; return ns;
} }
#ifdef __cplusplus
}
#endif
#endif #endif

1
src/bin/Makefile.am
View file

@ -49,3 +49,4 @@ randltl_SOURCES = randltl.cc
ltl2tgba_SOURCES = ltl2tgba.cc ltl2tgba_SOURCES = ltl2tgba.cc
ltl2tgta_SOURCES = ltl2tgta.cc ltl2tgta_SOURCES = ltl2tgta.cc
ltlcheck_SOURCES = ltlcheck.cc ltlcheck_SOURCES = ltlcheck.cc
ltlcheck_LDADD = $(LDADD) $(LIB_GETHRXTIME)

9
src/bin/ltlcheck.cc
View file

@ -28,7 +28,7 @@
#include <cstdio> #include <cstdio>
#include <argp.h> #include <argp.h>
#include "error.h" #include "error.h"
#include <sstream> #include "gethrxtime.h"
#include "common_setup.hh" #include "common_setup.hh"
#include "common_cout.hh" #include "common_cout.hh"
@ -113,6 +113,7 @@ struct statistics
unsigned scc; unsigned scc;
unsigned nondetstates; unsigned nondetstates;
bool nondeterministic; bool nondeterministic;
double time;
unsigned product_states; unsigned product_states;
unsigned product_transitions; unsigned product_transitions;
unsigned product_scc; unsigned product_scc;
@ -127,6 +128,7 @@ struct statistics
" \"scc\",\n" " \"scc\",\n"
" \"nondetstates\",\n" " \"nondetstates\",\n"
" \"nondeterministic\",\n" " \"nondeterministic\",\n"
" \"time\",\n"
" \"product_states\",\n" " \"product_states\",\n"
" \"product_transitions\",\n" " \"product_transitions\",\n"
" \"product_scc\""); " \"product_scc\"");
@ -142,6 +144,7 @@ struct statistics
<< scc << ", " << scc << ", "
<< nondetstates << ", " << nondetstates << ", "
<< nondeterministic << ", " << nondeterministic << ", "
<< time << ", "
<< product_states << ", " << product_states << ", "
<< product_transitions << ", " << product_transitions << ", "
<< product_scc; << product_scc;
@ -365,7 +368,9 @@ namespace
std::string cmd = command.str(); std::string cmd = command.str();
std::cerr << "Running [" << l << translator_num << "]: " std::cerr << "Running [" << l << translator_num << "]: "
<< cmd << std::endl; << cmd << std::endl;
xtime_t before = gethrxtime();
int es = system(cmd.c_str()); int es = system(cmd.c_str());
xtime_t after = gethrxtime();
const spot::tgba* res = 0; const spot::tgba* res = 0;
if (es) if (es)
@ -429,6 +434,8 @@ namespace
st->scc = m.scc_count(); st->scc = m.scc_count();
st->nondetstates = spot::count_nondet_states(res); st->nondetstates = spot::count_nondet_states(res);
st->nondeterministic = st->nondetstates != 0; st->nondeterministic = st->nondetstates != 0;
double prec = XTIME_PRECISION;
st->time = (after - before) / prec;
} }
return res; return res;
} }