Update documentation: syntax correction

doc/avatarmodelchecker/ttool_avatarmodelchecker.tex

@@ -503,7 +503,7 @@ The verification of internal action loops is then managed in the \textit{Specifi
 For instance, if a static loop contains the states \textit{Collect, Elaborate, Fail, Retry} the pragma created would be \textit{Collect || Elaborate || Fail || Retry --> !(Collect || Elaborate || Fail || Retry)}.
 
 \section{Verification traces}
-Verification traces are extracted using the class \textit{CounterexampleTrace}. For each state created during the model-checking a \textit{CounterexampleTraceState} is associated with it to save the current state pointer for each block and a pointer to a father.. All the "counter" states are inserted in the map \textit{traceStates}. The final verification state is extracted by the method \textit{evaluateSafetyOfProperty} or \textit{checkPropertyOnDeadlock}. That state represents a point of a loop, of a deadlock, or a reachability.
+Verification traces are extracted using the class \textit{CounterexampleTrace}. For each state created during the model-checking a \textit{CounterexampleTraceState} is associated with it to save the current state pointer for each block and a pointer to a father. All the "counter" states are inserted in the map \textit{traceStates}. The final verification state is extracted by the method \textit{evaluateSafetyOfProperty} or \textit{checkPropertyOnDeadlock}. That state represents a point of a loop, of a deadlock, or a reachability.
 \\\\
 The verification trace is constructed in the \textit{CounterexampleTrace} class using the method \textit{buildTrace}. The start point is the last state \textit{counterexampleState} which ended the verification. If the verification ends with a reachability or a deadlock, so it does not contain a loop, the trace is simply created visiting each father starting from \textit{counterexampleState} until \textit{state 0}. If instead, the verification ends with a loop, we have to eventually manipulate the data since the recorded trace using the fathers may not include a loop. If visiting each father from \textit{counterexampleState} a loop is detected, the trace is already well constructed. If instead, it does not contain a loop, a loop is searched using a deep first search starting from the loop point (the state with the same hash value of \textit{counterexampleState}). Then, the trace visiting each father starting from the loop point is appended to the previously detected cycle.
 \\\\