GitLab

As discussed in HOA issue #62 and its associated pull request there are plan to reverse the current definition of Streett, from

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

to

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

this is so that Streett becomes the dual of Rabin, and so that we can introduce generalized Streett in a way that is both a generalization of Streett and the dual of generalized Rabin.

This change has not been accepted yet.

We have very few Streett-specific code in Spot so far, so here is what I think we should change:

1. we have nothing to change on input, because currently we ignore the acc-name: line.
2. we should change streett_to_generalized_buchi() to work with any Streett-like acceptance condition, by this I mean that we should accept each Streett pairs to list Fin and Inf in both orders. (BTW, can we generalize this algorithm to generalize Streett acceptance ? Think about it.)
3. we should change the output order of to_generalized_streett()
4. parse_acc() is tricky, because it does not know what HOA format it is reading so it does not know what Streett n means. Should we add an optional argument?
5. we should change print_hoa() to detect the favor of Streett that is compatible with the selected HOA version before we output acc-name: Streett n.
6. we should also change print_hoa() to recognize generalized Streett (I would use the definition from HOA 1.1 in HOA 1.0 as well since it is not defined there).

I think points 2 & 3 can be done right away, and that 4­–6 should not be merged before the aforementioned HOA issue is resolved.