search

adl / hoaf

Hanoi Omega-Automata Format
13 stars 2 forks source link

reverse Streett and introduce generalized-Streett #66

Closed adl closed 7 years ago

adl commented 7 years ago

My suggestion for #62.

The change to acc-name: Streett n is backward incompatible, but 1) The fact that Rabin and Streett were not dual in v1 was a flaw 2) we also want to have generalized-Streett as a dual of generalized-Rabin (which is largely used now) and we want Streett to be a special case of generalized-Streett, 3) I'd rather do the change now that there are very few tools that need to be updated 4) like for #63 we are only changing the meaning of a lowercase header, so we could argue that is not a major semantic change that would require upgrading the version number...

My plan for Spot is to support both versions of the format, so the HOA printer will emit acc-name: Streett n iff the acceptance condition match the Streett specification of the selected HOA version. On input, Spot has always ignored acc-name: so this in not a problem. Spot currently has one algorithm specialized for Streett (in the HOA v1 sense), and I plan to generalize it to be able to work on any Streett-like automaton (i.e., pairs of Inf/Fin in any order).

I guess the only producer of Streett is ltl2dstar, so I won't push this without comments from Joachim.

kleinj commented 7 years ago

I agree that we should switch the order in the Streett pairs. Unfortunately, we already use the "old" Streett definition when parsing HOA files in a released version of PRISM, i.e., relying on the acc-name header to determine the semantics of the acceptance sets. As we didn't have clearly defined semantics for the version numbers, the parser there rejects anything that is not 'v1' in practice.

I guess the cleanest way would be to just do the v1.1 release with a version number bump to 2, with the added clarifications about the version number semantics which are then backwards compatible. As there is currently limited tool support, it should then be relatively easy to adapt the tools.

Another option would be to use an alternative name for the reversed Streett condition, e.g., xStreett or AltStreett. But that looks a bit weird and would probably lead to keeping both variants in the future as well...

Regarding the changeset: