constraints between acc-name and Acceptance

[adl]

Excerpt from the Acceptance Specifications section (emphasis is mine):

Even if acc-name: is used, the Acceptance: line is mandatory and should match exactly the patterns given in the following examples. This way the tools that ignore the acc-name: line have no suprise. [...] A generalized [Büchi] automaton with three acceptance sets can be defined with:

acc-name: generalized-Buchi 3
Acceptance: 3 Inf(0)&Inf(1)&Inf(2)

I don't remember why we decided to require an exact match. I don't see what could go wrong if the Acceptance: line uses a different, but logically equivalent formula:

acc-name: generalized-Buchi 3
Acceptance: 3 Inf(1)&Inf(2)&Inf(0)

I would like to suggest that we change "should match exactly" to "should be logically equivalent to".

A side-effect of this change is that we would accept any of those

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))

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

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

While currently only one of these three should be allowed to have acc-name: parity min even 5. (I would leave the last two examples in the specification, and not show the first one.)

The only drawback I see here is that it makes any validation of the correspondance between acc-name: and Acceptance: slightly harder. One way it can be done it is to convert acc-name: and Acceptance: as two separate BDDs, and then check them for equality. I'm currently implementing such a BDD-based check not for validation (currently Spot always ignore the acc-name: line) but to automatically name acceptance conditions in autfilt. If I detect some Acceptance: line is equivalent to parity min even 5, then I can add the corresponding acc-name: line, and depending on what we decide here, I can either leave the Acceptance: line as-is or I can standardize it so it become an exact match.

[adl]

Another example worth considering, as I fear you might not like it. I'm actually suggesting to accept this

acc-name: Rabin 2
Acceptance: (Fin(0)|Fin(2)) & (Fin(0) | Inf(3)) & (Fin(2) | Inf(1)) & (Inf(1) | Inf(3))

because this acceptance formula is just Rabin 2 in CNF.

[kleinj]

The only drawback I see here is that it makes any validation of the correspondance between acc-name: and Acceptance: slightly harder.

I would prefer to keep it as-is, exactly for the reason of very easy (syntactic) validation. It provides a consumer that relies on acc-name an extra level of assurance that the acceptance is correct and as intended. jhoafparser will routinely detect such mismatches and throw an error. I don't see the benefit of relaxing this requirement, if a producer commits to outputting the acc-name, then it surely knows how to output the canonical form...

Perhaps it would be worthwhile to code a small JavaScript form that can be used to output the canonical forms of the various acceptance types for given parameters? Might be helpful for users, especially for the corner-cases.

[adl]

My only motivation is that for parity acceptance there are two encodings which I think are legitimate. There is the quadratic encoding that we suggest in the specifications: an irredundant sum-of-product that makes the acceptance very Rabin-like. But there is also a linear encoding, like

Acceptance: 5 Inf(0) | Fin(1) & (Inf(2) | Fin(3) & Inf(4))

for parity min even 5. While it does not look like Rabin, this linear encoding has the advantage that when you complement it, you get another linear encoding:

Acceptance: 5 Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))

which actually is a linear encoding of parity min odd 5. While if you complement the quadratic encoding you get some horrible crap. I like this duality, and I'm sad I can't tag this linear acceptance with acc-name: parity ....

For all the other acceptance conditions, I agree there is little point in supporting alternate forms.

Perhaps it would be worthwhile to code a small JavaScript form that can be used to output the canonical forms of the various acceptance types for given parameters? Might be helpful for users, especially for the corner-cases.

FWIW, I already have some Python bindings to experiment with that (not yet merged, and not yet updated to account for #42 but that will be done soon):

>>> import spot
>>> spot.parse_acc_code('Rabin 2')
(Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
>>> spot.parse_acc_code('Rabin 2').to_cnf()
(Fin(0)|Fin(2)) & (Fin(0) | Inf(3)) & (Fin(2) | Inf(1)) & (Inf(1) | Inf(3))
>>> spot.parse_acc_code('parity max even 4')
(Fin(3) & Inf(2)) | (Fin(3) & Fin(2) & Fin(1) & Inf(0))
>>> spot.parse_acc_code('Fin(0) | Fin(1) & Fin(2)').complement()
(Inf(1) | Inf(2)) & Inf(0)

[kleinj]

But there is also a linear encoding, like Acceptance: 5 Inf(0) | Fin(1) & (Inf(2) | Fin(3) & Inf(4)) for parity min even 5.

I'd have no objection to changing the canonical acceptance conditions for parity to such linear ones.

FWIW, I already have some Python bindings to experiment with that

Nice!

[adl]

I wrote

Acceptance: 5 Fin(0) & (Inf(1) | (Fin(2) & (Inf(3) | Fin(4))))

which actually is a linear encoding of parity min odd 5.

but I think this is wrong, because the linear encoding of parity min odd 5 is just

Acceptance: 5 Fin(0) & (Inf(1) | (Fin(2) & Inf(3)))

The former acceptance will be satisfied by Fin(0)&Fin(2)&Fin(4) but that does not guarantee that an odd set will be visited infinitely often.

Of course in a real parity automaton the fact that a state always belongs to exactly one set ensures that Fin(0)&Fin(2)&Fin(4) is equivalent to Inf(1)|Inf(2), but in the general case we may not assume that. Maybe we should have a property like property: partitioned-sets (or partitioned-acc?) when the acceptance sets form a partition of the states (or of the transitions).

So the duality is slightly less nice than I first thought. Nonetheless, I still prefer the linear encoding.

I'd have no objection to changing the canonical acceptance conditions for parity to such linear ones.

I think that would be better.

Here is an updated version of the text to get a better feeling of these linear encodings. I choose the last two examples to be the dual of the first two ones, to better highlight that the dual is not exactly the complement. Maybe this calls for another paragraph discussing the fact that what people call a parity automaton is an automaton with parity acceptance and partitioned acceptance sets?

If the automaton should accept when the least identifier of acceptance sets visited infinitely often is even, we write:

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

If the greatest identifier has to be odd, we write:

acc-name: parity max odd 6
Acceptance: 6 Inf(5) | (Fin(4) & (Inf(3) | (Fin(2) & Inf(1))))

The dual combinations min odd or max even are also possible:

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

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

[adl]

Two points.

First, as far as the original issue is concerned (i.e., allowing or disallowing acc-name: on logically equivalent acceptance formulas), I agree with Joachim to keep it strict, and I've fixed Spot to follow that rule. autfilt is still trying to play it "smart" in the sense that if you input an automaton with Inf(3)&Fin(2) | Fin(0)&Inf(1) as acceptance, autfilt will reorder it as Fin(0)&Inf(1) | Fin(2)&Inf(3) in order be allowed to call it Rabin 2 in the output. (This is only done if the formula is already in CNF, and similar reordering occurs for Streett, generalized Büchi, and generalized co-Buchi as well.)

Second, for the encoding of parity acceptance, I see that Jan merged #45, but Joachim sent me some concerns by email this afternoon. This is what we get for discussing things privately... So I'll close this issue an open a new one dedicated to those strange parity questions.