[Termtools] Issues with StarExec/Script for the results

Marcel Hark marcel.hark at cs.rwth-aachen.de
Mon Jun 15 11:30:31 CEST 2020


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

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


More information about the Termtools mailing list