[Termination tools] web-interface for termination tools

[H. Zantema]

On Thu, 26 May 2005, Aart Middeldorp wrote:

> I don't see any point in embedding the competition version of TTT (which
> isn't designed to produce nice output) in the AProVE facility.

My idea was not to consider this as an AProVE facility but as a neutral
facility, just like the competition page is a neutral facility and
not a CiME facility, although sharing the author and a prefix of 
the corresponding url. For sure (as a reaction on another email) this 
should be clear from the presentation and the lay-out. In my view Peter 
is the most natural person to develop this facility, and if you like 
he can be installed as a sub-committee of the competition organization,
by which he will do this on behalf of this sub-committee, and not as a
member of the AProVE team. 

I propose the format to be consistent with the competition page: when 
entering a TRS/SRS all corresponding tools should be applied and the 
output should be like a row in the results page of the competition: for 
every tool a red, yellow or green box with the time in it (or "time-out"), 
and by clicking on the box the tool output should appear. I think this 
facility would be very useful, even if some of the tools have their own 
web interface. If I want to know whether termination of a particular 
system can be proved by any tool, I want to enter this system only once, 
and not in several separate interfaces. Moreover, I hope this facility to 
be more stable than the separate interfaces. In particular, in the past 
often the TTT interface was not available.

Aart: do you still want to outplace TTT by not participating in this 
facility?

About the format I think we should use only TPDB format; why otherwise we
defined a common format? I propose that the area in which the TRS/SRS 
should be entered is initially not empty, but shows up a simple example 
in TPDB format. Then crucial details like declaration of variables for TRSs
and using comma's between rule in SRSs are obvious from the example. In 
this way also people not aware of the TPDB format or XML or whatever can 
use it by simply editing this initial system.

		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+