[Termtools] Issues with StarExec/Script for the results

Tue Jun 16 09:14:38 CEST 2020

Hey Akihisa,

you are right, sorry for the inconveniences. I generated an anonymous
link to the job but it seems that this is somewhat useless to share the
details. I made the spaces public, they can be found in [1] and [2].

Thank you for the reference to the jobs of TermComp 2019. As far as we
can see, we chose the same settings, i.e., no pre-processing, execution
via runsolver, and post-processing by "CeTA-2.35 for runsolver". We used
the standard settings for memory and timeout of starexec.

[1] https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=417401

[2] https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=417407

Without any postprocessing we got identical results from AProVE.
However, when we enable post-processing via CeTA, our proofs do not get
certified but get the prefix "INVALID_CLAIM".

Best,

Marcel

Am 15.06.20 um 16:50 schrieb Yamada, Akihisa:
> Dear Marcel,
>
> I don't think you made the job details visible to us. Try "edit space
> permissions" -> "make public".
>
> Anyway, you'd better first reproduce the 2019 setting. Check 'job
> overview' of
> https://www.starexec.org/starexec/secure/details/job.jsp?id=33569.
>
> Best,
> Akihisa
>
> On 2020/06/15 20:26, Marcel Hark wrote:
>> 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
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>
-- 

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/20200616/cd23ad53/attachment-0001.htm>