investigate how ra_to_ba can be generalized
Can we write ra_to_ba()
for transition-based generalized Rabin automata? Generalizing the technique of Krishnan et al. (ISAAC'94)?
If that works, we can combine that with #174 (closed) and our determinization procedure to obtain a way to decide whether an automaton represents a recurrence property.