[Spot] Re: [BUG] Bug translate LTL formula into automata

Hi Vincenzo, (Sorry for the delay, I just found your email in the middle of hundreds of spams that were waiting to be moderated...) Vincenzo Tramo <vv.tramo(a)gmail.com> writes: The above looks like an LTL formula generated from LTLf, so a deterministic BA will always exist for that. Building this DBA is reasonably fast: % ltl2tgba -D -F input1.ltl --stats="%s st., %e ed., %r sec." 381 st., 7269 ed., 0.67422 sec. If I drop option -D, it becomes slow because Spot will try to simplify the non-deterministic Büchi automaton using simulation-based reductions. I've found that if we activate only direct-simulation, the translation is efficient: % ltl2tgba -x simul=1 -F input1.ltl --stats="%s st., %e ed., %r sec." 395 st., 6290 ed., 0.601192 sec. However, the reverse simulation is very slow: with ~390 equivalence classes and some state having a up to 250 incoming edges, building the BDD signature of some of these states is very expensive, and BuDDy spends a lot of time running its garbage collector and allocating more memory. At this point, it's not clear to me how we could improve that. Switching to the matrix-based implementation of simulation-based reduction was successful too, but the size reduction is inferior: % ltl2tgba -x simul-method=2 -F input1.ltl --stats="%s st., %e ed., %r sec." 420 st., 6356 ed., 1.2033 sec. I've created an issue to track any progress on that https://gitlab.lre.epita.fr/spot/spot/-/issues/599 That second formula has 80 atomic propositions and looks highly random to me. Since we are dealing with algorithms that have 2^AP worst cases, do we have any to reason to believe it show be translated efficiently? Alexandre