better encoding for parity acceptance #42

Closed
adl opened this Issue May 19, 2015 · 6 comments

Comments

Projects
None yet
5 participants
@adl
Owner

adl commented May 19, 2015

I'm implementing some support for generating and recognizing parity acceptance conditions, and I don't like the encoding currently suggested in the specifications:

acc-name: parity min even 5
Acceptance: 5 Inf(0) | (Fin(0)&Fin(1)&Inf(2)) | (Fin(0)&Fin(1)&Fin(2)&Fin(3)&Inf(4))

I would prefer this to be

acc-name: parity min even 5
Acceptance: 5 Inf(0) | (Fin(1)&Inf(2)) | (Fin(1)&Fin(3)&Inf(4))

The two formulas are logically equivalent, but the second

  • is an irredundant sum of products,
  • does not use the same set number in both Fin and Inf primitves.

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 encodes Inf(0) xor Inf(1).)

What do you think? Can I change the parity examples to use the irredundant encoding?

@adl adl added the enhancement label May 19, 2015

@xblahoud

This comment has been minimized.

Show comment
Hide comment
@xblahoud

xblahoud May 20, 2015

Collaborator

I like the suggestion. It makes the acceptance shorter and I can't see any disadvantages.

Collaborator

xblahoud commented May 20, 2015

I like the suggestion. It makes the acceptance shorter and I can't see any disadvantages.

@strejcek

This comment has been minimized.

Show comment
Hide comment
@strejcek

strejcek May 20, 2015

Collaborator

I agree, please change it.

Collaborator

strejcek commented May 20, 2015

I agree, please change it.

@adl

This comment has been minimized.

Show comment
Hide comment
@adl

adl May 20, 2015

Owner

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.

Owner

adl commented May 20, 2015

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.

@JanKretinsky

This comment has been minimized.

Show comment
Hide comment
@JanKretinsky

JanKretinsky May 20, 2015

Collaborator

I'm also fine with your suggestion

Collaborator

JanKretinsky commented May 20, 2015

I'm also fine with your suggestion

@kleinj

This comment has been minimized.

Show comment
Hide comment
@kleinj

kleinj May 20, 2015

Collaborator

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?

Collaborator

kleinj commented May 20, 2015

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?

adl added a commit that referenced this issue May 20, 2015

@adl

This comment has been minimized.

Show comment
Hide comment
@adl

adl May 20, 2015

Owner

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?

Owner

adl commented May 20, 2015

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?

@adl adl closed this in 663a6d4 May 20, 2015

kleinj added a commit that referenced this issue May 20, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment