[Termtools] timing

[Martin Johann Korp]

Dear all,

> Johannes Waldmann wrote:
> Matchbox is being cautious and assumes wall clock time
> internally. I think Jambox also does (e. g. we both use
> the "timeout" command to kill SAT solvers and this uses the wall clock).
> What does TTTbox do? (It seems to know very exactly what time it is,
> so it can print DONTKNOW at the very last moment :-)

Sorry for answering that late. TTTbox uses wall clock time too. That's the
reason why it can print in genereal DONT KNOW a few ms before the timout is
reached :-). In the program a SIGALARM signal is thrown, 60 (resp. 300) seconds
after the start.

> Claude Marché wrote:
> So if some tool is starting another process, but do not kill this second
> process properly, my engine do not see the time spent in the second
> process. I do not know how to fix this problem...

Maybe the intervall timer "ITIMER_PROF" can be used to calculate the process
time. As I know, this timer decrease whenever the system is running on behalf
of the process. If this does not work than an other possibility would be to use
the Linux function "time". For instance, execute the programa with the prefix
"time", write time-results in a file and read the informations.

Best regards,
      Martin Korp

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools