[Termtools] Issues with StarExec/Script for the results

[Akihisa Yamada]

Dear Marcel,

thank you for the report! About 2. I'm very sorry, it looks like my 
fault. I'll find time later this this week to fix it.

About BenchExec, I guess you forget to chose a right postprocessor 
(plain.5 or 6). In general, a link to a failing StarExec job will help.

However, BenchExec is known not to work properly (cf. 
https://github.com/StarExec/StarExec/issues/232). Unless the issue is 
fixed, we should use the working runsolver (with plain.4).

Best regards,
Akihisa

On 2020/06/09 0:12, Marcel Hark wrote:
> 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
> 
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
このEメールはアバスト アンチウイルスによりウイルススキャンされています。
https://www.avast.com/antivirus