Annotation Correctness Help

       This property assumes that annotations in scenarios must be valid at corresponding states in any admissible scenarios execution. To check the annotation consistency symbolic simulation of MSC diagrams is used rather than execution with specific states. Each time when annotations are met they are checked to be the consequences from current conditions. In the case of loops annotations can be used as loop invariants.