search

adl / hoaf

Hanoi Omega-Automata Format
13 stars 2 forks source link

Add Alphabet header for specifying an alphabet not based on atomic propositions #54

Closed kleinj closed 8 years ago

kleinj commented 8 years ago

To support use cases where the alphabet of the automaton is not defined over a set of atomic propositions, it would make sense to allow an alternative way of specifying the alphabet:

header-item ::= ...
             | "Alphabet:" INT STRING*

Example:

Alphabet: 3 "a" "b" "c"

This header would be mutually exclusive to the AP header.

In such an automaton, the integer indizes would refer to the individual letters:

[0]     successor // letter a
[1 | 2] successor // letter b or c

t would be "any letter", f and conjunctions would lead to ignored transitions.

Areas that would need adaptions:

Adding such an Alphabet header would not cause existing tools to misinterpret the automaton, as they should reject unknown headers with semantic implications (capitalized A).

kleinj commented 8 years ago

I pushed a proposal to the issue/54 branch (fb750ba15dcc52e043868bc7a3cd6c5dbdaa639b). Feedback very welcome.

The main changes:

kleinj commented 8 years ago

I forgot to mention: There's currently no example using the Alphabet header.

xblahoud commented 8 years ago

I will provide one during the weekend or in the next week.

strejcek commented 8 years ago

Regarding the explicit/implicit labels: I think that it makes sense to use implicit edge labelling even with Alphabet: we simply assume that the edges are labelled with the letters in the order given in the Alphabet specification header.

If you do not have anything against, I will propose a modification in the next days.

kleinj commented 8 years ago

Thanks, yes, I missed that, it makes sense to allow implicit edge labelling as well.

strejcek commented 8 years ago

I think that this is now done (including implicit transition labels for directly defined alphabet).