Dear Akihisa,

I updated the runscript so that if AProVE fails to (dis)prove Termination, it outputs "MAYBE". I will add the new configuration id via pull-request.

Additionally, we found a bug in our complexity_its setting (Complexity_ITS just runs as a demonstration). Thus, we would like to add another version of AProVE which just runs for the complexity_its demonstration (and thus does not affect any of the other tested categories). Are we allowed to do this?

Best,

Marcel

Dear Marcel,

I see, but according to the rule, tools should output MAYBE rather than nothing. I think disabling the custom timeout will be the easiest.

Best,
Akihisa

On 2021/07/05 16:55, Marcel Hark wrote:

Dear Akihisa,

I checked this example. The configuration "certified" of AProVE was chosen in such a way, that as many interruptions of benchexec or the postprocessor as possible can be avoided. Thus, if the run of AProVE does not lead to "YES + Proof", "NO + Proof" or "WORST_CASE + Proof" the underlying starexec runscript does not output anything at all.

In the given example, the following happens: We set the timeout of AProVE to the timeout of starexec /minus 10s/ (to have some time for printing the proof etc.). Thus, AProVE internally kills the process after 290s. Without our runscript for the certified categories it outputs "KILLED" as it cannot (dis)prove termination within 90s.

The configuration "standard" of AProVE does not call AProVE with a timeout, i.e., here it can indeed happen that benchexec kills AProVE and notes a timeout.

Best,

Marcel

Am 05.07.21 um 04:45 schrieb YAMADA, Akihisa:

- AProVE certified: https://www.starexec.org/starexec/secure/details/pair.jsp?id=516304215
No idea, but time is almost up. Is there some pre-timeout process that doesn't write even "TIMEOUT"?

-- 

Marcel Hark
Research Group Computer Science 2
RWTH Aachen University
Ahornstr. 55
52074 Aachen
Germany

E-Mail: marcel.hark@cs.rwth-aachen.de"
Phone: +49-241/80-21218
Fax: +49-241/80-22217
Room: 4208