[Termtools] Termination Competition test run

[Johannes Waldmann]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Simon -

thanks for sending the information,
and for getting the competition up and running in the first place.


Just to be very clear about what's happening:
you are essentially repeating last year's competition
(old provers) on the new hardware and infrastructure, right?

So results should match those from last year.
Do you have some automated way of checking
whether this really is the case?


As the infrastructure seems to be working,
we could start making more concrete plans
towards the "real" thing (i.e., using updated provers
and new problems/categories perhaps).

I think there should be a competition steering committe meeting
sometime during RTA, assuming most prover authors are present.
But I don't see when, as the schedule is packed. Any suggestions?
(I'd skip the Pflasterspektakel trip on Thursday
but that's just me, I've see enough juggling already...
also, Thursday is rather late in the week.)

Would it be possible to accept (test) submissions
of new prover versions during RTA, and also do some test runs
(not the complete TPDB of course)? Assuming that Simon is
present to handle technical issues that might occur.


Still, we should separate discussion on
specification issues (how do we want to use the infrastructure)
from implementation issues (Simon will figure these out ...).
E.g. the committee should decide on categories (defining
problem selection, rules for scoring, time frame for
submissions/runs/reporting).

So, bring your proposals to Hagenberg,
and/or post them here on the list.
We can use the termination-portal wiki for keeping track
of the discussion (but not for discussions themselves).
You might want to re-check these notes:
http://termination-portal.org/wiki/WScT08-Minutes-Competition



PS: Here is some reading on a project with similar goals
(running several solvers on several problems)
and a similar design: http://www.smtexec.org/
(why didn't we just copy their source code)



Best regards, Johannes Waldmann.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.4-svn0 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFIciknDqiTJ5Q4dm8RApTRAJ9aymjN49iNof7xkGLJ6iCaijIuZACdHgRA
ZRmLH+4V2uXbUDQb7JR+5rY=
=UCrg
-----END PGP SIGNATURE-----