[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