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