chaos in labels

[strejcek]

The current document admits that one state of the automaton can be state-labeled, another one can have labels on outgoing transition, and another can have implicit labels (à la ltl2dstar). Is this what we want. I don't think so.

We should clearly state that the whole automaton is either state-labelled or explicit transition-labelled or implicit transition-labelled.

Do you agree?

[adl]

I'll admit that I allowed this deliberately. I don't think anybody needs it, but it just feels easier to implement. I prefer to have three different ways to parse one state rather than three different ways to parse one list of states. The latter option would require more code to be duplicated (in case the grammar is unfolded three times), or some additional checks (are all states defined using the same syntax?) to be performed.

That said, I could live with a parser that is more liberal (allowing mixed definitions) than our specification document (if we decide to disallow this), and I would definitely not mix these syntax in the output.

A secondary issue to this discussion is that I'm wondering if, for consistency with the way state-based acceptance could be considered as syntactic sugar for transition-based acceptance of all outgoing transitions (#5), we should not consider state labels in the same way. I mean that just like we have

State: 1 {1}
 (0) 2
 (!0) 3 {0}

equivalent to

State: 1
 (0) 2 {1}
 (!0) 3 {0 1}

We could also have

State: (1) 1 {1}
 (0) 2
 (!0) 3 {0}

equivalent to

State: 1
 (0&1) 2 {1}
 (!0&1) 3 {0 1}

I confess I don't really see any use for this (while I can imagine reasons to mix transition-based and state-based acceptance) I'm just mentioning it because it some way, it would feel natural.

[xblahoud]

We should clearly state that the whole automaton is either state-labelled or explicit transition-labelled or implicit transition-labelled.

It makes sense not to mix implicit trans-labelled with explicit labelling (note that label of state cannot be merged with the implicit-labelled transitions of the same state). In the case of mixing explicit state and trans. labels I have no strong opinion. What Alexandre suggested sounds OK for me.

But shall we admit to mix some states that have implicit labels on transitions with states that uses explicit? Like:

State: 2
 1
 1 {0}
 2
 2 {0}
State: 1
 (0&1) 2 {1}
 (!0&1) 3 {0 1}

That looks like a big mess for me.

[strejcek]

I was thinking about this half a day (when sitting in a state-exam committee today) and I do not see any problem in mixing the label styles. Again, we should be careful with the presentation.

In general, I suggest to make all examples reasonable, i.e. not mixing accepting states/transitions and not mixing label styles. But somewhere down in the document, we should explicitly mention that one can mix accepting states/transitions and/or label styles. We can emphasize that if one avoids mixing, the semantics of each automaton is very natural. Finally, we should explain that in the case of some mixing, accepting states and labels on states can be seen as syntactic sugar and we should provide the formal semantics as well.