9 May
2023
9 May
'23
10:48 a.m.
Hi Marcel,
Marcel Gerber <mgerber59(a)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