timer: also consider the time spent in child processes
* src/misc/timer.hh: Fix. * NEWS: Mention the bug.
This commit is contained in:
parent
55ee18b96a
commit
20824b96b9
2 changed files with 15 additions and 6 deletions
9
NEWS
9
NEWS
|
|
@ -11,6 +11,15 @@ New in spot 1.2.2a (not yet released)
|
||||||
- randltl had trouble generating formulas when all unary, or
|
- randltl had trouble generating formulas when all unary, or
|
||||||
all binary/n-ary operators were disabled.
|
all binary/n-ary operators were disabled.
|
||||||
- Fix spurious testsuite failure when using Pandas 0.13.
|
- Fix spurious testsuite failure when using Pandas 0.13.
|
||||||
|
- Add the time spent in child processes when measuring time
|
||||||
|
with the timer class.
|
||||||
|
- Fix determinism of the SAT-based minimization encoding.
|
||||||
|
(It would sometimes produce different equivalent automata,
|
||||||
|
because of a different encoding order.)
|
||||||
|
- A the SAT-based minimization is asked for a 10-state automaton
|
||||||
|
and return a 6-state automaton, do not ask for a 9-state
|
||||||
|
automaton in the next iteration...
|
||||||
|
|
||||||
|
|
||||||
New in spot 1.2.2 (2014-01-24)
|
New in spot 1.2.2 (2014-01-24)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,6 +1,6 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2009, 2011, 2012, 2013 Laboratoire de Recherche et
|
// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche
|
||||||
// Développement de l'Epita (LRDE).
|
// et Développement de l'Epita (LRDE).
|
||||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
// et Marie Curie.
|
// et Marie Curie.
|
||||||
|
|
@ -69,8 +69,8 @@ namespace spot
|
||||||
#ifdef SPOT_HAVE_TIMES
|
#ifdef SPOT_HAVE_TIMES
|
||||||
struct tms tmp;
|
struct tms tmp;
|
||||||
times(&tmp);
|
times(&tmp);
|
||||||
start_.utime = tmp.tms_utime;
|
start_.utime = tmp.tms_utime + tmp.tms_cutime;
|
||||||
start_.stime = tmp.tms_stime;
|
start_.stime = tmp.tms_stime + tmp.tms_cstime;
|
||||||
#else
|
#else
|
||||||
start_.utime = clock();
|
start_.utime = clock();
|
||||||
#endif
|
#endif
|
||||||
|
|
@ -83,8 +83,8 @@ namespace spot
|
||||||
#ifdef SPOT_HAVE_TIMES
|
#ifdef SPOT_HAVE_TIMES
|
||||||
struct tms tmp;
|
struct tms tmp;
|
||||||
times(&tmp);
|
times(&tmp);
|
||||||
total_.utime += tmp.tms_utime - start_.utime;
|
total_.utime += tmp.tms_utime + tmp.tms_cutime - start_.utime;
|
||||||
total_.stime += tmp.tms_stime - start_.stime;
|
total_.stime += tmp.tms_stime + tmp.tms_cstime - start_.stime;
|
||||||
#else
|
#else
|
||||||
total_.utime += clock() - start_.utime;
|
total_.utime += clock() - start_.utime;
|
||||||
#endif
|
#endif
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue