[Termination tools] Several issues

[Claude Marche]

>>>>> "Juergen" == Juergen Giesl <giesl at informatik.rwth-aachen.de> writes:

    >> Also, the timeout needs not to be necessarily the same for each
    >> problem. One could imagine a way to enlarge the timeout, for all the
    >> problems that have not been solved this year. It could even be done
    >> automatically : if a problem is not solved by any tool, then we rerun
    >> the tools with a larger timeout. Imagine we do that
    >> first with 1 second, then 10, then 1 minute, then 5 minutes : I guess
    >> TTT will be pleased with that !

    Juergen> I think that even if there is a system
    Juergen> that can solve a problem in 1 second, it is still interesting to know
    Juergen> whether other systems can probably solve it in 10 seconds. But I agree

I expected this answer from you, of course. But my proposal could be
made less strict. For example :

1) first run each tool with a timeout of 5 seconds
2) if no tool solved the pb within 1 second (not 5), rerun the tools which
were unsuccessfull with a timeout of 1 minute.
3) if no tool solves the pb within 30 seconds, rerun the tools which
were unsuccesfull with a timeout of 5 minutes.

We simply have to adjust the values in order to make Juergen and Aart
equally satisfied.

    Juergen> that raising the timeout from 1 minute to something higher should only
    Juergen> be done for systems where no tool was successful within 1 minute (since
    Juergen> otherwise, the competition will take too long).



-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |