generalized Streett?

[adl]

I'm currently implementing a conversion from arbitrary acceptance to generalized Rabin and generalized Streett (with the goal of implementing an emptiness check of the latter). However I just realized that HOA defines generalized-Rabin but not generalized-Streett.

Turns out that the definition of generalized-Streett is not necessarily natural, because of what I (now) think is a design mistake in the format: in generalized-Rabin, Rabin, and Streett: Fin sets always come before Inf sets in clauses. As a consequence complementing Rabin 1 acceptance (Fin(0)&Inf(1)) gives Inf(0)|Fin(1) which is different from Streett 1 (= Fin(0)|Inf(1)): one additionally needs to rename the acceptance sets to obtain a Streett automaton when complementing an Rabin automaton.

So for generalized-Streett, one option is to propagate this flaw, and use

acc-name: generalized-Streett 3 2 1 0
Acceptance: 6 (Fin(0)|Fin(1)|Inf(2))&(Fin(3)|Inf(4))&Inf(5)

or we can use a proper dual of generalized Rabin:

acc-name: generalized-Streett 3 2 1 0
Acceptance: 6 (Inf(0)|Fin(1)|Fin(2))&(Inf(3)|Fin(4))&Inf(5)

This second option makes the code more elegant. For instance with this option I could implement to_generalized_streett(aut) as complement_acceptance(to_generalized_rabin(complement_acceptance(aut))).

However with this second option, it hurts that generalized-Streett 3 0 0 0 is not equal to Streett 3 :-(

[xblahoud]

I agree with Alexandre, that the current situation is a flaw and I would prefer to have the dual conditions to be defined as duals. So I suggest to define generalized-Streett as dual to generalized-Rabin. One reason for that is the consistency of the notation for the number of accepting sets, i.e. 3 2 1 0 from acc-name: generalized-Streett 3 2 1 0. For generalized-Rabin we have that the numbers 2 1 0 specify the numbers of sets in the second components of the pairs.

How painful would it be to change the definition of Streett?

(Btw. generalized-Streett 3 0 0 0 should be equivalent to generalized-Buchi 3. The one we would like to agree to Streett 3 is generalized-Streett 3 1 1 1.)

[strejcek]

I also vote for the second option: generalized-Streett 3 2 1 0 should stand for Acceptance: 6 (Inf(0)|Fin(1)|Fin(2))&(Inf(3)|Fin(4))&Inf(5). Further, I suggest to change the definition of Streett accordingly.

The question is when to fix the definition of Streett. I see two options:

1. Consider the current state as a bug and fix it immediately.
2. Fix it at the next major release (2.0).

The second option is politically (more) correct, but it could also bring more damage. I think that now the option Streett is used by very few third-party tools (or maybe none), but if we wait with the fix until the next major release, more tools may start to use the buggy version of Streett. Hence I vote for the first option.

[adl]

I'm voting to change this now too.

Currently the Spot's autfilt --generalized-streett generates the first form (i.e., the generalization of the "flawed" Streett), but does not output acc-name: generalized-streett. I don't think anybody is using this option, so I'm not afraid to reorder the generalized Streett acceptance.

Regarding Streett, at least ltl2dstar is one producer of Streett automata that would need to be changed. Spot can read those and has some dedicated Streett->TGBA conversion algorithm that currently only detect Streett acceptance if it is given as in the HOA spec. I'd be happy to adjust this algorithm to support both style of Streett acceptance (I'll need to support both style anyway if Spot has to read/write both versions of the format).

[strejcek]

To make some progress, I've merged the Alexandre's pull request #66 (we all agreed on) and corrected the bugs detected by Joachim ($L_1$ -> $F_1$ and "generic" -> "Generalized").

I'm almost sure that the option with two alternative names for Streett acceptance (with different order of Fins and Infs) would not get serious support.

What remains to be decided is the new version number: Do we want to switch to v2 or release it as v1.1?

I have no strong opinion here: I tend to slightly prefer v1.1 as the changes are not very big. On the other hand, the current description of version numbers says:

The major version number should be updated in case of changes that invalidate the syntax or semantic of earlier versions.

I'm afraid that this is a strong reason to switch to v2 (or change the description of version number semantics such that the changes of header entries starting with lowercase is not the reason to change major version number).