[Termtools] Termination Competition 2017: how to test your solvers on starexec

[Johannes Waldmann]

Dear colleagues,


here is some detail on this year's competition.
It will be the same as in previous years:
* submit and test solver on https://www.starexec.org/
* register participation with me (instructions follow soon)
* run on starexec, display on https://termcomp.imn.htwk-leipzig.de/

There will be two changes in technicalities.
None should require any change in participants' code,
but it is, of course, advised to test your solvers early.


1. Star-Exec now uses Bench-Exec instead of Runsolver.
This should give more accurate memory bounds,
especially for Java programs. Bench-Exec is now the default
"benchmarking framework" for Termination on Star-Exec.
https://github.com/jwaldmann/star-exec-presenter/issues/128

2. CeTA has two arguments now! (implemented by Akihisa Yamada - thanks!)
The conformance check between the TRS in the benchmark file
and the TRS in the proof file is now done inside CeTA, and is certified.
Still open ("CeTA needs three arguments") :
https://github.com/jwaldmann/ceta-postproc/issues/13


For testing in un-certified categories, use the "plain.5"
post-processor (which is the default). Example output:
https://termcomp.imn.htwk-leipzig.de/results/standard/noquery/22430

For testing in certified categories, use the "ceta-2.30-1"
post-processor (or higher version, as they become available),
example output:
https://termcomp.imn.htwk-leipzig.de/results/standard/noquery/22474


If you notice anything strange, then please report. Preferred methods:
* this mailing list (termtools)
  (for questions that need community attention and discussion)
* issue trackers (linked above)
  (for technical matters that just need fixing)
(Un-preferred: private email to me.)


Best regards, Johannes.