GitLab

Just like we have autfilt --product-and and autfilt --product-or, we should have autfilt --sum-or and autfilt --sum-and that put the two automata side-by-side and play with the initial states to implement union (non-deterministic initial states) or intersection (universal initial state). See slide 17 of this for an example.

Note that Spot does not support multiple initial states, so we need fake it as already done in the HOA parser. Also another trap is that two two operations requires labeling the one automaton with a set of marks that does not satisfy the acceptance of the other automaton. If the acceptance is a tautology, the acceptance has to be changed (e.g., to Büchi, as done in the complete_here() function).