randaut should learn to generate paralllel transitions
The random-automaton generator we use will output at most one edge between any pair of states. (This includes at most one self-loop as well.)
This is fine when the automaton is used to generate "state-spaces" (or should I say "transition-spaces"), as in ltlcross. In fact, the algorithm we use originates from lbtt.
However just sticking colors on top of such transitions does not cover the full ranges of ω-automata we may handle. We need to allow multiple transitions (with different colors) between states.
More generally, given a number of states, number of atomic proposition, and number of sets, could we ensure some kind of uniform generation of the random automata?