Dear all,
there seems no conflict this year :) But there are some errors.
- Ulitmate: https://www.starexec.org/starexec/secure/details/pair.jsp?id=516407978 It seems to fail to write a file. I think it should not write to the current directory but to the output directory, $2.
- 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"?
- TTT2 certified: https://www.starexec.org/starexec/secure/details/pair.jsp?id=516330503 A garbage is present before CPF output.
- NaTT certified: https://www.starexec.org/starexec/secure/details/pair.jsp?id=516331340 Hmm I must debug...
Best, Akihisa
Zeige Antworten nach Diskussionsstrang
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"?
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
Dear Akihisha,
going through some of the test outputs, I see that one feature of MnM was accidentally switched off in the current strategy that I'd like to turn on again. This is just to announce that a slightly revised version will probably be submitted by July 10.
Best regards Dieter
On Mon, 2021-07-05 at 11:45 +0900, YAMADA, Akihisa wrote:
Dear all, there seems no conflict this year :) But there are some errors.
--
Dieter Hofbauer dieter_hofbauer@web.de Mühlengasse 16, D-34125 Kassel, Germany phone (+49) 561 739 29 54
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
Am 05.07.21 um 11:20 schrieb YAMADA, Akihisa:
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
Dear Marcel,
sure!
Akihisa
On 2021/07/05 19:17, Marcel Hark wrote:
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
Am 05.07.21 um 11:20 schrieb YAMADA, Akihisa:
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
--
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
termtools@lists.rwth-aachen.de
-
Dieter Hofbauer -
Marcel Hark -
YAMADA, Akihisa