Dear Akihisa,
for SRS-Standard (certified), for several benchmarks, example ICFP_2010/4991.xml, these results are displayed:
- matchbox: "YES (without \checkmark)" https://www.starexec.org/starexec/services/jobs/pairs/567222906/stdout/1?lim...
- ttt2: "post-processor error" (post processor timeout after 15 min) https://www.starexec.org/starexec/services/jobs/pairs/567222903/log
these are logically the same thing? (both did produce a certificate?)
Ah - noh, for matchbox, the certifier did not time-out, but "certification-err Stack space overflow: current size 8388608..."
Locally, I am not getting this error (certification succeeds in 50 seconds for matchbox' certificate, 55 seconds for ttt2's) I am using ceta-postproc (contains CeTA-2.42) compiled with ghc-9.0.2
- Johannes.
Dear Johannes, René,
interesting. The postproc should be using the ceta binary release. Can compilation option/environment make such a difference?
Best, Akihisa
On 7/27/2022 8:15 PM, Johannes Waldmann wrote:
Dear Akihisa,
for SRS-Standard (certified), for several benchmarks, example ICFP_2010/4991.xml, these results are displayed:
- matchbox: "YES (without \checkmark)"
https://www.starexec.org/starexec/services/jobs/pairs/567222906/stdout/1?lim...
- ttt2: "post-processor error" (post processor timeout after 15 min)
https://www.starexec.org/starexec/services/jobs/pairs/567222903/log
these are logically the same thing? (both did produce a certificate?)
Ah - noh, for matchbox, the certifier did not time-out, but "certification-err Stack space overflow: current size 8388608..."
Locally, I am not getting this error (certification succeeds in 50 seconds for matchbox' certificate, 55 seconds for ttt2's) I am using ceta-postproc (contains CeTA-2.42) compiled with ghc-9.0.2
- Johannes.
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Can compilation option/environment make such a difference?
Oh, certainly. GHC RTS (default) settings and implementation might change with each release.
I am trying to reproduce the error locally. What ghc did you use? (8.10.7 seems fine.)
- J.
Dear all,
(just a short status message, since Akihisa is busy right now)
René, Akihisa and I have investigated the time-outs and stack-overflows of CeTA. We understand what's happening (it's nothing about the source code, but about compilation) and we have an improvement (locally, for now). It takes some time to install on starexec.
Best regards, Johannes.
Dear all,
ttt2 still has time-outs in the certifier, even though we compiled CeTA with recent GHC, and -O2, and Akihisa increased the time limit considerably (to 45 min)
I made this analysis - and sort-of partial work-around https://github.com/jwaldmann/ceta-postproc/issues/25#issuecomment-1208128726
So, matchbox was lucky to not use matchbounds (for srs std cert) ...
- Johannes.
Dear Johannes,
thank you for your report and investigation.
Today I found time to implemented the following approach for all tree-automata based techniques such as matchbounds, roofbounds, …: before a tree automata with n states is given to the checker, all states are renamed to integers 0 .. n-1. (CeTA internally is flexible in what the type of states are, only CPF uses “string”).
However, for me (running ghc -O2) there is no big difference between this new version and CeTA 2.42, in particular on example 3633.cpf.ttt2
All of you that are interested can access this intermediate version of CeTA under
http://cl-informatik.uibk.ac.at/users/thiemann/ceta_states_integer.tgz
Best, René
Am 08.08.2022 um 15:37 schrieb Johannes Waldmann johannes.waldmann@htwk-leipzig.de:
Dear all,
ttt2 still has time-outs in the certifier, even though we compiled CeTA with recent GHC, and -O2, and Akihisa increased the time limit considerably (to 45 min)
I made this analysis - and sort-of partial work-around https://github.com/jwaldmann/ceta-postproc/issues/25#issuecomment-1208128726
So, matchbox was lucky to not use matchbounds (for srs std cert) ...
- Johannes.
Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Dear René
... all states are renamed to integers 0 .. n-1.
Thank you for working on this.
I updated my timing and profiling data
https://github.com/jwaldmann/ceta-postproc/issues/25#issuecomment-1219982858
it's down 15 percent, and now red-black tree operations dominate everything. So, perhaps
- use a better implementation of sets (like containers:Data.IntMap - but I understand you want that certified first ... perhaps it can be imported with "sorry", just to get an idea of the run-time)
- remove sets altogether from (the hot code of) checking bounds (what do they represent? why are they needed? the automaton is non-deterministic, because it can have epsilon transitions? )
well, clearly that work should be sponsored by the authors of tools that use match-bounds...
Best regards, Johannes.
termtools@lists.rwth-aachen.de
-
Johannes Waldmann -
Thiemann, René -
YAMADA, Akihisa