From 12daa0571dbb8c7f4011eb8e88c5ec58966907da Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Wed, 29 Jul 2020 11:04:31 +0200
Subject: [PATCH] Update documentation: syntax correction

---
 doc/avatarmodelchecker/ttool_avatarmodelchecker.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex b/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
index 1f625c29c2..f427cd3a63 100644
--- a/doc/avatarmodelchecker/ttool_avatarmodelchecker.tex
+++ b/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.
 \\\\
-- 
GitLab