[Termtools] certification failures

[Carsten Otto]

On Wed, Nov 12, 2008 at 03:14:33PM +0100, olivier.pons at cnam.fr wrote:
> Maybe we can also implement an intelligent timeout to avoid that.

Yes. Some proofs are quite huge (>100 MByte HTML) and constructing this
information based on some complicated tree structure (containing branches
that did not provide parts of the "winning" proof) takes some time.

In principle a second timeout (starting after YES/NO was delivered) is only
needed to avoid bugs in tools where the proof output is too slow (or maybe
non-terminating? :)
A very safe way to avoid these problems, but still allow for a complete
proof output, would be to use the same timeout again. If it was possible to
create the proof in this time, it should be possible to output it in the
same time. No matter how generous this second timeout is, the impact on the
total time needed to run the competition is quite small (since the vast
majority of tools manages to create and output the proof before the first
timeout is hit) - and even if not, only a few additional seconds will be
needed in most cases.

PS: This problem is not as simple as it sounds. We experienced strange
problems with very huge proofs, slow/heavy Java garbage collection and
saturated network links to the databse in the past.

Best regards,
-- 
Carsten Otto           otto at informatik.rwth-aachen.de
LuFG Informatik 2      http://verify.rwth-aachen.de/otto/
RWTH Aachen            phone: +49 241 80-21241
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: Digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081112/b3d2f4f8/attachment.pgp