[Termtools] certified - strange proofs

[Koprowski, A.]

  Ok, that indeed deserves explanation, which was already given by Frederic but let me try to be more explicit.

  So as far as I know TTT2 uses the same scripts (runme & checkme) as TPA for certification. Now, those problems come from the fact that while writing those scripts I had only TPA in mind and I made some assumptions that were not properly discussed with TTT2 team. Those assumptions are:
-) if the tool succeeds, it should print the XML certificate on standard output and exit with status 0
-) otherwise it should return with non-zero status and the output does not matter.

  Now what happens is:
1) TTT2 prints Maybe BUT exits with status 0
2) runme script thinks that the proof succeeded and gives the standard output (MAYBE) to Rainbow.
3) Rainbow finds out that this is not a valid proof and throws an exception "Not a valid proof"
4) the runme scripts fails to check whether Rainbow succeeded (all TPA produced proofs are correct "by definition") prints YES and outputs an empty proof.
5) Coq gets an empty file as input, which is a valid Coq file so it can "certify termination"

  The really bad outcome of the whole thing is that TTT2 gets points for systems for which it essentially fails. Of course this should be avoided and even more so in the certified competition!

  Best wishes,
   Adam

-----Original Message-----
From: termtools-bounces at lists.lri.fr on behalf of Christian Sternagel
Sent: Wed 6/6/2007 10:21
To: termtools at lri.fr
Subject: [Termtools] certified - strange proofs
 
It seems as there was a second missunderstanding between me and the
Rainbow(runscript)-authors. I assumed that everything except a
correct XML-file is interpreted as a wrong proof. But I saw
that everytime when ttt2-cert outputs `MAYBE' (instead of an XML-file)
there is a YES in the coq-proof output followed by an exception.
The real strange thing is, that Coq afterwards succeeds in certifying,
but there is no proof at all.

An example is: TRS/SK90/2.26.trs

cheers

christian
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools