relabel automata to reduce atomic propositions
Jérôme Dubois tells me that he is working with a benchmark of automata where the edges have complex Boolean formulas, but the automaton only uses a handful of different formulas. This is causing slowdowns in algorithms like simulation()
that are sensible to the BDD sizes. In his case it would make sense to first relabel the entire automaton with shorter formulas, apply the simulation, and then relabel the results. It's not clear how to do that in practice, but that would be a useful function, similar to what we do for Boolean subformulas during LTL translation.