[Termtools] termination competition changes

[Aart Middeldorp]

Dear all,

This message contains important information about forthcoming
changes to the termination competition: (a) XML format, (b)
execution environment, and (c) competition schedule.

(a) Based on the original discussion in Leipzig in May 2008,
we have developed an XML format to replace the TPDB format.
The XML format offers the following advantages:

- structured representation of the TRS format
- easily extensible for future applications (current support
   for complexity and termination)
- meta-information can more easily be included
- input can be easily verified for syntactical correctness

The XML format can be used as storage format for the database
as well as input format for termination provers. We have created
a converter from the TPDB format to the new XML format as well
as an XSLT stylesheet which will generate the TPDB format from a
given XML file. See

http://termination-portal.org/wiki/XTC_Format_Specification

for details. In the next few days more explanation will be added.

(b) Following the SMT competition, we will provide a termination
execution platform (termexec in the following) which enables tool
authors to run experiments independent from the competition but
on the same hardware. Tool authors will be able to compare different
tools (including tools from previous competitions) on selected
categories, including secret problems. We aim to have termexec up
and running by May 1. A document describing the functionality in
more detail will be placed on the termination wiki later this month.

(c) Termexec will alleviate the need for ongoing competitions. We
plan to have quarterly competitions (January 1, April 1, and so on)
instead. The start date can be fixed at the forthcoming workshop on
termination in Leipzig (June 3-5, 2009).

-- TC organisation