Closed adl closed 9 years ago
I like the suggestion. It makes the acceptance shorter and I can't see any disadvantages.
I agree, please change it.
I've made a patch on branch adl/42, but I would like Joachim's opinion before we merge it, as I think he is the only producer of Parity automata currently.
I'm also fine with your suggestion
Fine by me. Currently, jhoafparser does not check for the canonical Acceptance expression for parity, I'll add that.
Should we add the canonical expressions for 'min odd' and 'max even' to the format document as well, just to be extra clear what's expected?
I've added examples for parity min odd 6
and parity max even 5
. Can you double check and merge if you are happy with it?
I'm implementing some support for generating and recognizing parity acceptance conditions, and I don't like the encoding currently suggested in the specifications:
I would prefer this to be
The two formulas are logically equivalent, but the second
In particular, I have found the latter point to be important in several algorithms. I can think of at least three algorithms in Spot where either I have special cases to handle acceptance with sets that are both used as Inf and Fin, or the algorithm is simply requires disjoint Fin/Inf numbers as a prerequisite. (My typical simple "horror case" is
Acceptance: 2 (Fin(0)&Inf(1)) | (Inf(0)&Fin(1))
which basically encodesInf(0) xor Inf(1)
.)What do you think? Can I change the parity examples to use the irredundant encoding?