[Termtools] [Termcomp] Fwd: Re: [color] Termination Competition 2009: Call for Participation

[Frederic Blanqui]

Johannes Waldmann a écrit :
>> Another question: if we provide a "checkme" command, what can be the 
>> arguments? Is it possible to take as argument both the problem file and 
>> the proof file as follows:
>>
>> checkme xtc_file cpf_file?
> 
> As I understand, that would be redundant.
> The proof contains the problem.
> http://cl-informatik.uibk.ac.at/software/cpf/
> root element: certificationProblem, child elements: input, proof

It is redundant if the proof really contains the same problem...

> BTW, what has happened to the names:
> XTC meant "xml format for Termination Certificates" (at WScT08)?
> Now XTC denotes the input format only?

It seems so.

> Is there any synchronisation between XTC and CPF?
> It seems that XTC:trs (what version?)
> is copied into CPF:trs but they are not identical
> (e.g., signature and relrules are missing from CPF:trs?)
> In fact CPF should just refer to XTC here?

I agree. This also means that giving the problem as argument is not 
completely redundant currently...

> Oh, and while we're at it - I think a naming like
> "z001.xml" (as in current tpdb)  is wrong - it should be "z001.xtc"
 >
> Compare the naming conventions for source codes:
> you don't say "quicksort.text" but "quicksort.java" (etc.)
> because you then see that you need a Java compiler.
> text (or xml) just denotes the visual represenation.

I agree.