AdditionalSuggestions

chapters/annotations.tex

@@ -461,7 +461,7 @@ \section{Annotations for Code Generation}\label{annotations-for-code-generation}
 \end{annotationdefinition}
 
 \section{Annotations for Simulations}\label{annotations-for-simulations}
-These annotations define how models can be simulated.
+These annotations define how models can be checked, translated, and simulated.
 \subsection{Annotations for Simulation Experiments}\label{annotations-for-simulation-experiments}
 \begin{lstlisting}[language=grammar]
 experiment-annotation:
@@ -483,7 +483,7 @@ \subsection{Annotation for Test Cases}\label{annotation-for-test-cases}
    annotation "(" "TestCase" "(" "shouldPass" "=" ( false | true ) ")" ")"
 \end{lstlisting}
 If \lstinline!shouldPass! is \lstinline!false! it indicates that the translation or the simulation of the model should fail.
-If a tools checks a package where classes have \lstinline!shouldPass=false! they should not generate errors, and may even be skipped.
+If a tools checks a package where classes have \lstinline!shouldPass=false! they should not generate errors, and checking may even be skipped.
 On the other hand, models with \lstinline!shouldPass=false! may be useful for creation of negative tests in tool-specific ways.
 Similarly as a class with obsolete-annotation, a class with \lstinline!TestCase! annotation (regardless of the value of \lstinline!shouldPass!) shall not be used in other models, unless those models also have a \lstinline!TestCase! annotation.
 \begin{nonnormative}