search

jwaldmann / ceta-postproc

GNU Lesser General Public License v3.0
0 stars 0 forks source link

expecting "<", but found: 'MAYBE #23

Open jwaldmann opened 4 years ago

jwaldmann commented 4 years ago

example:

output contains

WORST_CASE(?,O(n^1))
MAYBE
<?xml version="1.0" encoding="UTF-8"?>
<?xml-stylesheet type="text/xsl" href="cpfHTML.xsl"?>

this MAYBE is expected?

dio4ev commented 4 years ago

I cannot see the job details as I have no permission.

Yes, it is expected as this would show the BEST_CASE if it was found (solver is TcT?). Is that a Problem? I thought that only the first line matters.

jwaldmann commented 4 years ago

So what should ceta do in this case?

dio4ev commented 4 years ago

Normally, CeTA expects the certificate without an/a answer/result of the prover. For TTT2 the first line says either "YES", "NO" or "MAYBE".

So maybe I have to adjust TcT that it only outputs the WORST_CASE to be consistent with the certifiable output (and especially the number of lines which have to be removed by the postprocessor?) of other tools?

jwaldmann commented 4 years ago

Also, while we're discussing the output of one specific tool here, we should really be looking at the specification for the certified complexity categories.

It (should be at http://www.termination-portal.org/wiki/Complexity but it) is at http://cbr.uibk.ac.at/competition/rules.php but that does not mention where the certificate goes?

jwaldmann commented 4 years ago

Can you point at specific examples (per category) from last year's termcomp - so we can make the postprocessor behave identical to that.

dio4ev commented 4 years ago

Also, while we're discussing the output of one specific tool here, we should really be looking at the specification for the certified complexity categories.

It (should be at http://www.termination-portal.org/wiki/Complexity but it) is at http://cbr.uibk.ac.at/competition/rules.php but that does not mention where the certificate goes?

So as far as I can see we are not allowed to give the BEST_CASE...I will adapt that

dio4ev commented 4 years ago

Can you point at specific examples (per category) from last year's termcomp - so we can make the postprocessor behave identical to that.

As far as I can see, last year the output of AProVE was some complexity followed by a proof 0. (and this also applies for the certified categories of all other tools, e.g. where TTT2 participates) So I think that I just have to remove the BEST_CASE ouput. Then we should have the same output scheme as last year.

dio4ev commented 4 years ago

@jwaldmann: I have uploaded a new TcT solver "tct-trs_v3.2.0_2020-06-28" on my StarExec space. This solver omits the BEST_CASE output and should have the same output format as other solvers.

jwaldmann commented 4 years ago

OK. You can run the tests youself, pick "ceta-postproc-2.39.0 (654)" as post-processor.

The semantics of output should really be

I will try to fix/update ceta-postproc (please report issues here or on the mailing list), but the termcomp organizer will decide about its usage.

dio4ev commented 4 years ago

Thank you for all the help!

I have started a test run and will report on it tomorrow.

Am 28. Juni 2020 22:30:26 MESZ schrieb jwaldmann notifications@github.com:

OK. You can run the tests youself, pick "ceta-postproc-2.39.0 (654)" as post-processor.

The semantics of output should really be

  • discussed by the participants of the category (I am not),
  • and be decided, and written down, by the SC (I am not).

I will try to fix/update ceta-postproc (please report issues here or on the mailing list), but the termcomp organizer will decide about its usage.

-- You are receiving this because you commented. Reply to this email directly or view it on GitHub: https://github.com/jwaldmann/ceta-postproc/issues/23#issuecomment-650817611

--

dio4ev commented 4 years ago

After adapting the output, I would say that the postprocessor works:

https://www.starexec.org/starexec/secure/details/job.jsp?id=41408