adl/hoaf — pull request #2 by adl (2014-01-22 22:47:00+00:00)
Title: Add support for alternating automata.

This is a first attempt at specifying alternating automata for discussion.

The addition of disjunct destinations also enables, even on non-alternating automata, some syntactic fusion of edges that have the same source, label, and acceptance sets (but different destination). It's not clear to me if this is welcome, or if this is just some additional burden on the authors of the parsers. Should authors of tools that do not care about alternating automata really bother about supporting disjunct destinations?

One feature I have left out is the notion of "empty" destination, usually represented by "true" in the state-formula representing the destination. I can see that this helpful when handling states of alternating automata algorithmically (because "true & x" simplifies to "x"), but on the other hand:
- it's not very difficult to detect a "true" state when it has been represented explicitly.
- one problem with implicit states is that their membership to the various acceptance sets is then unclear (this implicit state obviously has to be accepting, but imagine a complex acceptance condition with disjunctions, and hence multiple ways to be satisfied).
- if we change `state-formula` to allow `t`, then the following automaton becomes another way to accept any word.

HOA: v1
States: 0
Start: t
Acceptance: 1 I0