support for additional state/transition properties

[adl]

This was partly discussed in an email, and is also related to #3.

The question here is whether we want to support extra and optional properties for states or transitions. For instance it could be useful for a GUI to attach coordinates to states. Other tools might want to attach different kind of properties to states or transitions: for instance to partition the state into different SCCs, to add weights (cf. #3), to preserve the number of the original state in algorithms that transform automata, to add rendering information (like "draw in bold"), etc.

Currently, we only support such extra information with /* comments */. While this can be helpful for debugging, it is not a good way to carry information between tools.

We discussed a few options with Jan S and Fanda today. It seems clear that if this has to be extensible, the additional properties should be named somehow. E.g., if we need to attach a coordinate, we could write <x: 10, y: 20>. So the properties would be a list of key-value pairs. I suggest that the same rule that we have applied to headers be used here: properties that carry semantic information should be capitalized, so that tools may ignore only properties starting with a lowercase letter.

If we have such a key-value syntax for attaching properties to states and transitions, a natural question is whether we should not regard the guards [0&1] and membership to acceptance sets {0 1} as properties too, and use a uniform syntax for everything? We would have something like Label: 0&1, Acc: 0 1, etc. But then we have to decide how to properly represent properties that are not simple values (like 0&1, or 0 1) and repeating Label and Acc for every transltion appears to be bloat. We would rather keep the current structure, and add an optional <key:value...> if needed.

We suggest to get a first working version of the format without the additional properties, and then see if we need more and what. So far we have lived very well with less than we currently plan to support, and over-designing the format will just delay its implementation.

[kleinj]

Agreed.

[JanKretinsky]

Coordinates would be a very useful feature, but I agree that for now we have to do without, v2 should accommodate that