Distinguish usages of explanations
Currently the explanations are used by two completely different purposes:
- Display information in IDE for the user
- Stored in shapes for helping merging: preventing associated goals that were not of the same kind (pre, post, loop inv init, loop inv preserv, assert, etc.)
For usage 1, it is allowed to have several explanations, possible with different prefixes in the corresponding attributes. For usage 2, it is mandatory to have only one explanations. Usage 2 is potentially broken if a user adds other attributes prefixed with expl:
.