#593 Allow annotations on invariants

General notes

• Best to review per commit.
• Notes:
  • Invariants in locations require the annotation names with double at-signs (see below).
  • In the documentation, I switched from listing explicitly which elements have what kind of annotation names, to now using a table.
  • CifParserHooks now uses Collections.emptyList() instead of listc(0). This requires less memory (no array storage, all the same immutable list instance).

Regarding annotation names

I ran into an issue for annotations on elements within locations (invariants now, later also edges). I get shift/reduce conflicts when trying to add them.

The problem is that if there is an element in a location, and after that there is an annotation, it doesn't know whether to reduce the current location (if the annotation is for the next location) or to shift the annotation (if it is for a invariant or edge of the current location). For an LALR(1) parser, this can't be decided. Only once the full annotation has been parsed (could be a lot of tokens for all the arguments and their values), then it sees the next keyword (edge, invariant, location, etc).

I thought about whether there is a solution to this. Somehow, it needs more knowledge to distinguish between a next location element, or a next location. Most things in the CIF language, if they can have elements, end with and end keyword. Then it is clear where for instance an automaton ends, and thus whether the next thing is an element of the automaton, or a next thing in its parent. We don't have that for locations.

I therefore thought about allowing locations to also end with end (optionally). And to only allow annotations on a non-first location in an automaton if the previous location ended with end. But, then it gets reduce/reduce conflicts on end keywords, as it doesn't know whether to end the location or the automaton, on account of the end being optional for locations.

Then I thought of not distinguishing between the annotated elements, but the annotations themselves. We already do that for specifications vs all other annotations, using specification annotations for specifications instead of regular annotations. If we also use specifications annotations (renaming them to 'double at-sign annotations') for elements of locations, we can easily solve the issues. I went for this solution, as I think it is the most clean.

Addresses #593 (closed)