[Termtools] Issues with StarExec/Script for the results

Yamada, Akihisa akihisa.yamada at aist.go.jp
Mon Jun 15 11:54:14 CEST 2020


Dear Marcel,

could you share the failing starexec job?

Best,
Akihisa

On 2020/06/15 18:30, Marcel Hark wrote:
> Dear Akihisa,
> 
> thank you for the quick fix. I have another question regarding testing 
> for certified categories. The most recent version of CeTA in the 
> post-processor menu is CeTA 2.35 for runsolver. The most recent version 
> of CeTA seems to be 2.39. Is this the version we should choose for 
> testing? We tried this but got "INVALID_CLAIM" as prefix in every entry 
> of the column "results". Please let me know if I can provide further 
> information or help you in adapting the settings.
> 
> Best,
> 
> Marcel
> 
> Am 12.06.20 um 10:04 schrieb Yamada, Akihisa:
>> 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 
>>>>
>>>>
>>>
>>
> -- 
> 
> 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
> 

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



More information about the Termtools mailing list