ltl2tgba --parity and autfilt --parity
Currently ltl2tgba -G -D
can return deterministic generalized Büchi or parity. For people who absolutely need parity automata, it would be nice to have a --parity
option.
This means adding parity output to spot::postprocessor
, and then of course we also want --parity
in autfilt
. So we cannot just assume the input will be generalized Büchi or parity.
It seems @max has some code for converting Rabin or Streett to parity, can this be adapted to generalized Rabin and generalized Streett? (It would be horrible if our conversion for arbitrary acceptance to parity had to go through NBA).
Ideally, I'd also like to be able to say that I want a special type of parity (like max even
, or that I don't care). @lxu wrote several functions to convert one type of parity to another, so this part would be just devising the spot::postprocessor
interface to specify those desires and the calling the right functions.