-Introducing non-determinism both in \verb+fetch_values+ and
-\verb+diffuse_values+ functions is necessary in our context. If the
-non-determinism would be used only in \verb+fetch_values+, then it would not be
-possible for instance to retrieve the value $X_i^{(t)}$ without taking into
-account the value $X_i^{(t-1)}$. On the other hand, if the non-determinism is
-only used in \verb+diffuse_values+, then each time a value is pushed into the
-channel, this value is immediately consumed, which contradicts the notion of
-delays.
-
-\subsection{Discussion}
-A coarse approach could consist in providing one process for each element.
-However, the distance with the mathematical model given in \Equ{eq:async} of
-such a translation would be larger than the method presented along these lines.
-It induces that it would be harder to prove the soundness and completeness of
-such a translation. For that reason we have developed a PROMELA model that is
-as close as possible to the mathematical one.
-
-Notice furthermore that PROMELA is an imperative language which
-often results in generating intermediate states
-(to execute a matrix assignment for
-instance).
-The use of the \verb+atomic+ keyword allows the grouping of
-instructions, making the PROMELA code and the DDN as closed as possible.
-
-\subsection{Universal Convergence Property}
-We are left to show how to formalize into the SPIN model-checker that iterations
-of a DDN with $n$ elements are universally convergent. We first recall that the
+L'introduction de l'indéterminisme à la fois dans les fonctions \verb+fetch_values+
+et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était
+présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer
+la valeur $X_i^{(t)}$ sans considérer la valeur $X_i^{(t-1)}$.
+De manière duale, si le non-determinism était uniquement
+utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait
+mise dans le cannal, elle serait immédiatement consommé, ce qui est contradictoire avec la notion de
+délai.
+
+% \subsection{Discussion}
+% A coarse approach could consist in providing one process for each element.
+% However, the distance with the mathematical model given in \Equ{eq:async} of
+% such a translation would be larger than the method presented along these lines.
+% It induces that it would be harder to prove the soundness and completeness of
+% such a translation. For that reason we have developed a PROMELA model that is
+% as close as possible to the mathematical one.
+
+% Notice furthermore that PROMELA is an imperative language which
+% often results in generating intermediate states
+% (to execute a matrix assignment for
+% instance).
+% The use of the \verb+atomic+ keyword allows the grouping of
+% instructions, making the PROMELA code and the DDN as closed as possible.
+
+\subsection{Propriéte de convergence universelle}
+Il reste à formaliser dans le model checker SPIN que les itérations d'un système
+dynamique à $n$ éléments est universellement convergent.
+
+We first recall that the
