Streett changes for HOA 1.1
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:
-
we have nothing to change on input, because currently we ignore the acc-name:
line. -
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.) -
we should change the output order of to_generalized_streett()
-
parse_acc()
is tricky, because it does not know what HOA format it is reading so it does not know whatStreett n
means. Should we add an optional argument? -
we should change print_hoa()
to detect the favor of Streett that is compatible with the selected HOA version before we outputacc-name: Streett n
. -
we should also change print_hoa()
to recognizegeneralized 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.