Hi Marcel, Marcel Gerber <mgerber59@gmail.com> writes:

I notice that `product_or` necessarily runs `complete` on both input automata [...] If my thinking is correct, this would not be necessary if both input automata are Büchi automata, correct?

I don't think so. E.g., imagine the product_or of an automaton for G(a) and an automaton for G(!a). If you don't complete the two automata, the resulting product would be incorrect.

Right now, running `product_or`, even on small input automata, produces absolutely unwieldy automata that are impossible to interpret. This is mostly due to my use case, where I'm using letters of an alphabet more akin to a standard DFA model, and encoding a symbol of `a` into the preposition formula `a & !b & !c` etc. This works well with single automata and with intersections, but not with unions sadly.

It is unfortunate that Spot only supports 2^AP alphabets. If you use an encoding of letters that has gaps (i.e., the union U of the boolean formulas representing each letter is not bddtrue) maybe it also makes sense to intersect all edge labels with U before displaying them. My personal preference would would to encode the letters in such a way that their union is bddtrue. For instance if I have three letters a, b, c, encode 'a' as '!p0&!p1', 'b' as '!p0&p1', and 'c' as 'p0'. To help with graphical interpretation of the automaton, you could try to play with aliases: https://spot.lre.epita.fr/ipynb/aliases.html