I notice that `product_or` necessarily runs `complete` on both input automata [see this line in spot/twaalgos/product.cc]. In contrast, this is not the case for the "normal" `product`.

If my thinking is correct, this would not be necessary if both input automata are Büchi automata, correct? Because the union of two incomplete Büchi automata is an incomplete Büchi automaton again, and the product automaton construction applies as normal as far as I can tell.

Would it be possible to allow for this, potentially by introducing another method or exposing the `product_aux` function (incl. from Python)?

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.

Your help would be very much appreciated,

Marcel