[Termtools] Issues with StarExec/Script for the results
Yamada, Akihisa
akihisa.yamada at aist.go.jp
Fri Jun 12 10:04:59 CEST 2020
Dear complexity people,
as pointed out by Marcel, last years' scoring was wrong. I've fixed it
now here. Fortunately the ranking was not affected.
http://group-mmm.org/termination/competitions/Y2019/
Best regards,
Akihisa
On 2020/06/09 14:25, Akihisa Yamada wrote:
> 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://jpn01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FStarExec%2FStarExec%2Fissues%2F232&data=02%7C01%7Cakihisa.yamada%40aist.go.jp%7C2e54c43055014cb37e2408d80c358aa8%7C18a7fec8652f409b8369272d9ce80620%7C0%7C0%7C637272771380318734&sdata=OrzPHiiDihaPenP503ltyP7fZyr7m6%2Bf6bqMzbMlerw%3D&reserved=0).
> 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]
>> https://jpn01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fgroup-mmm.org%2Ftermination%2Fcompetitions%2FY2019%2Fcaches%2Fcomplexity_33014.html&data=02%7C01%7Cakihisa.yamada%40aist.go.jp%7C2e54c43055014cb37e2408d80c358aa8%7C18a7fec8652f409b8369272d9ce80620%7C0%7C0%7C637272771380318734&sdata=eKe7yyYdHyDbHNqDquMYxOvnZ5cIh5Z%2BnA01tWTy3Hc%3D&reserved=0
>>
>>
>> --
>>
>> 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
>> https://jpn01.safelinks.protection.outlook.com/?url=http%3A%2F%2Flists.lri.fr%2Fcgi-bin%2Fmailman%2Flistinfo%2Ftermtools&data=02%7C01%7Cakihisa.yamada%40aist.go.jp%7C2e54c43055014cb37e2408d80c358aa8%7C18a7fec8652f409b8369272d9ce80620%7C0%7C0%7C637272771380318734&sdata=AhsUFlmQOypcerbToc2UdX4KsIjYiBfyhnZqAtjJWHY%3D&reserved=0
>>
>>
>
--
このEメールはアバスト アンチウイルスによりウイルススキャンされています。
https://www.avast.com/antivirus
More information about the Termtools
mailing list