Improvements to TADL language

[vsimko]

We identified few cases that require extension to the current TADL langauge.

support for "mode switching" that is automatically verified, e.g. two modes A,B should always switch either A->B or B->A, but not A->A nor B->B
Here is a proposal, how the new TADL language could look like:

# Annotation group: modeA-modeB
## no multi-modeA
CTL AG(modeA -> AX(A[!modeA U modeB]))

## no multi-modeB
CTL AG(modeB -> AX(!E[!modeA U (modeB & !modeA)]))

## if there is "modeB" there must have been a "modeA" before
LTL G(modeB -> O(modeA))

# these are rules for adding new annotations to the specification
modeA -> mark:modeA; unmark:modeB
modeB -> mark:modeB; unmark:modeA

Another example could be the "abort" annotation which should automatically add "mark" annotation.

# Annotation group: abort
abort -> mark:abort

Finally, we could extend the TADL language to automatically add context information, such as use-case ID or step ID.

# Annotation group: create-use
create -> mark:create_$ucId_$stepNumber

... which would allow for guards like this: guard:create_UC1_5a4