generalized Streett? about hoaf HOT 4 OPEN

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

from hoaf.

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.

from hoaf.

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

from hoaf.

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

from hoaf.