[Termtools] Issues with StarExec/Script for the results

[Marcel Hark]

Dear Akihisa,

I hope you are fine and not so much affected by the current pandemic.

We are benchmarking and testing our tool AProVE on StarExec at the
moment and encountered two issues.

 1. The runscript "BenchExec", which is superior to runsolver in
    measuring used time and space, still seems to be not working:
    whatever job we start, it fails with 100% runscript errors. Could
    you as a representative of the termination community report this to
    the StarExec developers or shall we just report it ourselves?
 2. There seems to be an error in the script calculating the results for
    the complexity categories. For example, in [1], both CoFloCo and
    AProVE proved the complexity "O(1)" for
    "Brockschmidt_16/T2/array.koat" but in the table of the results this
    is not reflected: The stated upper bound is "infinity" for both
    tools. This occurs whenever a constant upper bound was proven.

Thanks for your help. Please let us know if we can provide any further
information or help you.

Best,

Marcel

[1]
http://group-mmm.org/termination/competitions/Y2019/caches/complexity_33014.html

-- 

Marcel Hark
Research Group Computer Science 2
RWTH Aachen University
52056 Aachen
Germany

E-Mail: marcel.hark at cs.rwth-aachen.de"
Phone: +49-241/80-21214
Fax: +49-241/80-22217
Room: 4208, Ahornstr. 55

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20200608/e74a2482/attachment.htm>