Hello,
I notice that `product_or` necessarily runs `complete` on both input automata [see this line in spot/twaalgos/product.cc https://gitlab.lre.epita.fr/spot/spot/-/blob/b487ff4190cdec4094154486bb8c04e90e0e741a/spot/twaalgos/product.cc#L462-469]. 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
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
-
Alexandre Duret-Lutz -
Marcel Gerber