[Termtools] Issues with StarExec/Script for the results

Marcel Hark marcel.hark at cs.rwth-aachen.de
Mon Jun 15 13:26:59 CEST 2020


Dear Akihisa,

The jobs can be found in [1] and [2]. The information/output files are
available at [3].

Best,

Marcel

[1]
https://www.starexec.org/starexec/secure/details/job.jsp?anonId=f4609732-05e3-4ee2-8207-fae3cc857827

[2]
https://www.starexec.org/starexec/secure/details/job.jsp?anonId=001f44b1-333a-4bd9-a61c-2e5b6f6fa92a

[3] https://rwth-aachen.sciebo.de/s/bA2pVynCBTLxRLl

Am 15.06.20 um 11:54 schrieb Yamada, Akihisa:
> 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
>>
>
-- 

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/b9eaebbc/attachment.htm>


More information about the Termtools mailing list