X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/e3c2188521eaa2c6e2c6eee2da43b0f42fc47a89..b3411a22f651c0dbca34dca87df92f8d3d130e1a:/modelchecking.tex?ds=inline

diff --git a/modelchecking.tex b/modelchecking.tex
index dd804c2..1b8843d 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,4 +1,64 @@
-\JFC{donner dans les rappels les dÃ©lais et les propriÃ©tÃ©s de convergence uniforme}
+\JFC{donner dans les rappels les dÃ©lais et les propriÃ©tÃ©s de convergence universelle}
+
+\JFC{Statuer sur la taille des exemples traitables par la dÃ©marche, cf donnÃ©es pratiques}
+
+\section{Exemple jouet}
+
+\begin{xpl}
+  On considÃ¨re dans ce chapitre l'exemple oÃ¹ trois Ã©lÃ©ments dans $\Bool$. 
+  Chaque configuration est ainsi un Ã©lement de $\{0,1\}^3$, \textit{i.e.}, 
+  un nombre entre 0 et 7. 
+  La \Fig{fig:map} prÃ©cise la fonction $f$ considÃ©rÃ©e et 
+  la \Fig{fig:xplgraph} donne son graphe d'intÃ©raction.
+  
+\begin{figure}[ht]
+  \centering
+  \begin{minipage}%[h]
+    {.6\linewidth}
+    \begin{center}
+      $ F(x)= \left \{
+        \begin{array}{rcl}
+          f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3  \\
+          f_2(x_1,x_2,x_3) & = & x_1 + \overline{x_3} \\
+          f_3(x_1,x_2,x_3) & = & x_2.x_3
+        \end{array}
+      \right.
+      $        
+    \end{center}
+    \caption{Fonction Ã  itÃ©rer}    \label{fig:map}
+  \end{minipage}
+  \begin{minipage}%[h]
+    {.35\linewidth}
+    \begin{center}
+      \includegraphics[width=4cm]{images/xplCnxMc.eps}
+    \end{center}
+    \caption{Graphe d'intÃ©raction}
+    \label{fig:xplgraph}
+    \end{minipage}
+  \caption{Exemple pour SDD $\approx$ SPIN.}
+\end{figure}
+
+
+
+
+
+
+On peut facilement vÃ©rifier que toutes les itÃ©rations parallÃ¨les initialisÃ©es 
+avec $x^0 \neq 7$ soit $(111)$ 
+convergent vers $2$ soit $(010)$; celles initialisÃ©es avec 
+$x^0=7$ restent en 7.
+Pour les autres modes synchrones avec  une 
+stratÃ©gie pseudo pÃ©riodique, les comportements selon la configuration initiale:
+\begin{itemize}
+\item initialisÃ©e avec 7, les itÃ©rations restent en 7;
+\item initialisÃ©e avec 0, 2, 4 ou 6 les itÃ©rations convergent vers 2;
+\item initialisÃ©es avec 1, 3 ou 5, les itÃ©rations convergent vers un des 
+deux points fixes 2 ou 7.
+\end{itemize}   
+\end{xpl}
+
+
+
 
 
 \section{Rappels sur le langage PROMELA}
@@ -11,7 +71,7 @@ On peut trouver davantage de dÃ©tails dans~\cite{Hol03,Wei97}.
 
 
 \begin{figure}[ht]
-\begin{scriptsize}
+\begin{tiny}
 \begin{lstlisting}
 #define N 3
 #define d_0 5
@@ -26,7 +86,7 @@ a_send channels [N];
 chan unlock_elements_update=[1] of {bool};
 chan sync_mutex=[1] of {bool};
 \end{lstlisting}
-\end{scriptsize}
+\end{tiny}
 \caption{Declaration des types de la traduction.}
 \label{fig:arrayofchannels}
 \end{figure}
@@ -34,74 +94,74 @@ chan sync_mutex=[1] of {bool};
 
 Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
 \texttt{short} et  \texttt{int}. Comme dans le langage C par exemple,
-on peut declarer des tableaux Ã  une dimension de taille constante 
+on peut dÃ©clarer des tableaux Ã  une dimension de taille constante 
 ou des nouveaux types de donnÃ©es (introduites par le mot clef 
 \verb+typedef+). Ces derniers sont utilisÃ©s pour dÃ©finir des tableaux Ã  deux
-dimension.
+dimensions.
 
 \begin{xpl}
 Le programme donnÃ© Ã  la {\sc Figure}~\ref{fig:arrayofchannels} correspond Ã  des 
 dÃ©clarations de variables qui serviront dans l'exemple jouet de ce chapitre. 
 Il dÃ©finit tout d'abord:
 \begin{itemize}
-\item les constantes \verb+N+ et \verb+d_0+ qui prÃ©cisent respectivement le numbre
+\item les constantes \verb+N+ et \verb+d_0+ qui prÃ©cisent respectivement le nombre
  $n$ d'Ã©lÃ©ments et le dÃ©lais maximum $\delta_0$;
 \item les deux tableaux  (\verb+X+ et \verb+Xp+) de \verb+N+ variables boolÃ©ennes; 
-les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associÃ©es Ã  la variables $X_{i+1}$
-d'un systÃ¨ne dynamique discret 
-(le dÃ©callage d'un entier est dÃ» Ã  l'indexation Ã  partir de zÃ©ro des cellules d'un tableau);
-Elles  memorisent les  valeurs de $X_{i+1}$ respectivement avant et aprÃ¨s sa mise Ã  jour; 
-il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $X$ Ã  changÃ© ou pas;
-\item le tableau \verb+mods+ contient les Ã©lÃ©ments qui doivent Ãªtre modifiÃ©s lors de l'iteration 
-en cours; cela correspond naturellement Ã  l'ensemble des Ã©lÃ©ments $S^t$;
+les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associÃ©es Ã  la variables $x_{i+1}$
+d'un systÃ¨me dynamique discret 
+(le dÃ©calages d'un entier est dÃ» Ã  l'indexation Ã  partir de zÃ©ro des cellules d'un tableau);
+Elles  mÃ©morisent les  valeurs de $X_{i+1}$ respectivement avant et aprÃ¨s sa mise Ã  jour; 
+il suffit ainsi de comparer  \verb+X+ et \verb+Xp+ pour constater si $x$ Ã  changÃ© ou pas;
+\item le tableau \verb+mods+ contient les Ã©lÃ©ments qui doivent Ãªtre modifiÃ©s lors de l'itÃ©ration 
+en cours; cela correspond naturellement Ã  l'ensemble des Ã©lÃ©ments $s^t$;
 \item le type de donnÃ©es structurÃ©es \verb+vals+ et le tableau de tableaux 
- \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise Ã  mÃ©moriser $X_{j+1}^{D^{t-1}_{i+1j+1}}$
- pour l'itÃ©ration au temps $t$ (en d'autres termes, utile lors du calcul de $X^{t}$).
+ \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise Ã  mÃ©moriser $x_{j+1}^{D^{t-1}_{i+1j+1}}$
+ pour l'itÃ©ration au temps $t$ (en d'autres termes, utile lors du calcul de $x^{t}$).
 \end{itemize}
 
 
-Puisque le dÃ©callage d'un indices ne change pas fondamentalement 
+Puisque le dÃ©calage d'un indices ne change pas fondamentalement 
 le comportement de la version PROMELA par rapport au modÃ¨le initial
-et pour des raisons de claretÃ©, on utilisera par la suite la mÃªme 
-lettre d'indice entre les deux niveaux (pour le modÃ¨le: $X_i$ et pour  PROMELA: 
-\texttt{X[i]}). Cependant, ce dÃ©callage devra Ãªtre conservÃ© mÃ©moire.
+et pour des raisons de clartÃ©, on utilisera par la suite la mÃªme 
+lettre d'indice entre les deux niveaux (pour le modÃ¨le: $x_i$ et pour  PROMELA: 
+\texttt{X[i]}). Cependant, ce dÃ©calage devra Ãªtre conservÃ© mÃ©moire.
 
 Une donnÃ©e de type \texttt{channel} permet le 
 transfert de messages entre processus dans un ordre FIFO.
 Elles serait dÃ©clarÃ©e avec le mot clef \verb+chan+ suivi par sa capacitÃ© 
-(qui est constante), son nom et le type des messages qui sont stockÃ©s dans ce cannal.
+(qui est constante), son nom et le type des messages qui sont stockÃ©s dans ce canal.
 Dans l'exemple prÃ©cÃ©dent, on dÃ©clare successivement:
 \begin{itemize}
-\item un cannal \verb+sent+ qui vise Ã  mÃ©moriser\verb+d_0+ messages de type
+\item un canal \verb+sent+ qui vise Ã  mÃ©moriser\verb+d_0+ messages de type
  \verb+bool+; le tableau nommÃ© \verb+channels+ de \verb+N+*\verb+N+
- Ã©lÃ©ments de type \verb+a_send+ est utilisÃ© pour mÃ©moriser les valeurs intermÃ©diaires $X_j$;
+ Ã©lÃ©ments de type \verb+a_send+ est utilisÃ© pour mÃ©moriser les valeurs intermÃ©diaires $x_j$;
  Il permet donc de temporiser leur emploi par d'autres elements $i$.
-\item les deux cannaux  \verb+unlock_elements_update+ et  \verb+sync_mutex+ contenant 
+\item les deux canaux  \verb+unlock_elements_update+ et  \verb+sync_mutex+ contenant 
 chacun un message boolÃ©en et utilisÃ© ensuite comme des sÃ©maphores.
 \end{itemize}
 \end{xpl}
 
 %\subsection{PROMELA Processes} 
-Le langage PROMELA exploite la notion de \emph{process} pour modÃ©liser la concurence
-au sein de systÃ¨mes. Un process est dÃ©clarÃ©avec le mot-clef
-\verb+proctype+  et est  instanciÃ© soit imÃ©diatement (lorsque sa dÃ©claration est prÃ©fixÃ©e 
+Le langage PROMELA exploite la notion de \emph{process} pour modÃ©liser la concurrence
+au sein de systÃ¨mes. Un process est dÃ©clarÃ© avec le mot-clÃ©
+\verb+proctype+  et est  instanciÃ© soit immÃ©diatement (lorsque sa dÃ©claration est prÃ©fixÃ©e 
  par le mot-clef  \verb+active+) ou bien au moment de l'exÃ©cution de l'instruction 
 \texttt{run}.
 Parmi tous les process,  \verb+init+ est le process  initial qui permet 
-d'initialiser les variables, lancer d'autres processes\ldots
+d'initialiser les variables, lancer d'autres process\ldots
 
 
-Les instructions d'affecatation sont interprÃ©tÃ©es usuellement.
-Les cannaux sont cernÃ©s par des instructions particuliÃ¨res d'envoi et de
-rÃ©ception de messages. Pour un cannal  
-\verb+ch+,  ces instruction sont respectivement notÃ©es
-\verb+ch  !  m+ et \verb+ch  ?  m+.
-L'instruction de rÃ©ception consomme la valeur en tÃªte du cannal \verb+ch+
+Les instructions d'affectation sont interprÃ©tÃ©es usuellement.
+Les canaux sont concernÃ©s par des instructions particuliÃ¨res d'envoi et de
+rÃ©ception de messages. Pour un canal  
+\verb+ch+,  ces instructions sont respectivement notÃ©es
+\verb+ch ! m+ et \verb+ch ? m+.
+L'instruction de rÃ©ception consomme la valeur en tÃªte du canal \verb+ch+
 et l'affecte Ã  la variable \verb+m+ (pour peu que  \verb+ch+ soit initialisÃ© et non vide).
-De maniÃ¨re similaire,l'instruction d'envoi ajoute la valeur de \verb+m+ Ã  la queue du canal
+De maniÃ¨re similaire, l'instruction d'envoi ajoute la valeur de \verb+m+ Ã  la queue du canal
 \verb+ch+ (pour peu que celui-ci soit initialisÃ© et non rempli).
-Dans les cas problÃ©matiques, canal non initialisÃ© et vide pour une reception ou bien rempli pour un envoi,
-le processus est blockÃ© jusqu'Ã  ce que les  conditions soient  remplies.
+Dans les cas problÃ©matiques, canal non initialisÃ© et vide pour une rÃ©ception ou bien rempli pour un envoi,
+le processus est bloquÃ© jusqu'Ã  ce que les  conditions soient  remplies.
 
 La structures de contrÃ´le   \verb+if+   (resp.   \verb+do+)   dÃ©finit un choix non dÃ©terministe 
  (resp.  une boucle non dÃ©terministe). Que ce soit pour la conditionnelle ou la boucle, 
@@ -110,28 +170,27 @@ sera choisi alÃ©atoirement puis exÃ©cutÃ©.
 
 Dans le process \verb+init+ dÃ©taillÃ© Ã  la {\sc Figure}~\ref{fig:spin:init}, 
 une boucle de taille $N$ initialise alÃ©atoirement la variable  globale de type tableau \verb+Xp+.
-Ceci permet par la suite de verifier si les itÃ©rations sont  convergentes pour n'importe  
-quelle configuration initiale $X^{(0)}$.
+Ceci permet par la suite de vÃ©rifier si les itÃ©rations sont  convergentes pour n'importe  
+quelle configuration initiale $x^{(0)}$.
 
 
 
 Pour chaque  Ã©lÃ©ment $i$, si les itÃ©rations sont asynchrones
 \begin{itemize}
 \item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+ 
-puisque la matrice $S^0$ est Ã©gale Ã  $(0)$,
+puisque la matrice $s^0$ est Ã©gale Ã  $(0)$,
 \item puis, la valeur  de $i$ (reprÃ©sentÃ©e par  \verb+Xp[i]+) devrait Ãªtre transmise 
   Ã  $j$  s'il y a un arc de $i$ Ã    $j$ dans le graphe d'incidence. Dans ce cas,
-  c'est la fonction  \verb+hasnext+ (non dÃ©taillÃ©e ici)  
-  \JFC{la dÃ©tailler}
-  qui   memorise ce graphe
+  c'est la fonction  \verb+hasnext+ (dÃ©taillÃ©e Ã  la~\Fig{fig:spin:hasnext})  
+  qui   mÃ©morise ce graphe
   en fixant Ã   \texttt{true} la variable \verb+is_succ+, naturellement et Ã  
   \texttt{false} dans le cas contraire. 
   Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+.
 \end{itemize}
 
 \begin{figure}[t]
- \begin{minipage}[h]{.52\linewidth}
-\begin{scriptsize}
+  \begin{minipage}[h]{.32\linewidth}
+\begin{tiny}
 \begin{lstlisting}
 init{
  int i=0; int j=0; bool is_succ=0;
@@ -164,11 +223,11 @@ init{
  sync_mutex ! 1;
 }
 \end{lstlisting}
-\end{scriptsize}
+\end{tiny}
 \caption{Process init.}\label{fig:spin:init} 
 \end{minipage}\hfill
- \begin{minipage}[h]{.42\linewidth}
-\begin{scriptsize}
+ \begin{minipage}[h]{.32\linewidth}
+\begin{tiny}
 \begin{lstlisting}
 active proctype scheduler(){ 
  do
@@ -189,10 +248,32 @@ active proctype scheduler(){
  od
 }
 \end{lstlisting}
-\end{scriptsize}
-\caption{Process scheduler pour la stratÃ©gie pseudo-periodique.
+\end{tiny}
+\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©rodique.
  \label{fig:scheduler}}
 \end{minipage}
+\begin{minipage}[h]{.30\linewidth}
+\begin{tiny}
+\begin{lstlisting}
+inline hasnext(i,j){
+  if
+    :: i==0 && j ==0 -> is_succ = 1
+    :: i==0 && j ==1 -> is_succ = 1
+    :: i==0 && j ==2 -> is_succ = 0
+    :: i==1 && j ==0 -> is_succ = 1
+    :: i==1 && j ==1 -> is_succ = 0
+    :: i==1 && j ==2 -> is_succ = 1
+    :: i==2 && j ==0 -> is_succ = 1	
+    :: i==2 && j ==1 -> is_succ = 1
+    :: i==2 && j ==2 -> is_succ = 1
+  fi
+}
+\end{lstlisting}
+\end{tiny}
+\caption{Codage du graphe d'intÃ©raction de $f$.
+ \label{fig:spin:hasnext}}
+\end{minipage}
+
 \end{figure}
 
 
@@ -206,48 +287,47 @@ ces notions est traduite vers un modÃ¨le PROMELA.
 
 
 \subsection{La stratÃ©gie}\label{sub:spin:strat}
-Regardons comment une stratÃ©gie pseudo-pÃ©riodique peut Ãªtre reprÃ©sentÃ©e en PROMELA.
+Regardons comment une stratÃ©gie pseudo pÃ©riodique peut Ãªtre reprÃ©sentÃ©e en PROMELA.
 Intuitivement, un process \verb+scheduler+ (comme reprÃ©sentÃ© Ã  la {\sc Figure}~\ref{fig:scheduler}) 
-est itÃ©rativement appelÃ© pour construire chaque $S^t$ reprÃ©sentant 
+est iterrativement appelÃ© pour construire chaque $s^t$ reprÃ©sentant 
 les Ã©lÃ©ments possiblement mis Ã  jour Ã  l'itÃ©ration $t$.
 
 Basiquement, le process est une boucle qui est dÃ©bloquÃ©e lorsque la valeur du sÃ©maphore
 \verb+sync_mutex+ est 1. Dans ce cas, les Ã©lÃ©ments Ã  modifier sont choisis
 alÃ©atoirement  (grÃ¢ce Ã   $n$ choix successifs) et sont mÃ©morisÃ©s dans le tableau
 \verb+mods+,  dont la taille est  \verb+ar_len+.   
-Dans la sÃ©quence d'Ã©xÃ©cution, le choix d'un Ã©lÃ©ment mis Ã  jour est directement
-suivi par des mis Ã jour: ceci est rÃ©alisÃ© grace Ã  la modification de la valeur du sÃ©maphore
+Dans la sÃ©quence d'exÃ©cution, le choix d'un Ã©lÃ©ment mis Ã  jour est directement
+suivi par des mises Ã  jour: ceci est rÃ©alisÃ© grÃ¢ce Ã  la modification de la valeur du sÃ©maphore
  \verb+unlock_elements_updates+.
 
-\subsection{ItÃ©rer la fonction $F$}\label{sub:spin:update}
-La mise Ã  jour de l'ensemble  $S^t=\{s_1,\ldots, s_m\}$  des Ã©lÃ©ments qui constituent la stratÃ©gie
-$(S^t)^{t \in \Nats}$ est implantÃ© Ã  l'aide du process  \verb+update_elems+ fourni Ã  la 
+\subsection{ItÃ©rer la fonction $f$}\label{sub:spin:update}
+La mise Ã  jour de l'ensemble  $s^t=\{s_1,\ldots, s_m\}$  des Ã©lÃ©ments qui constituent la stratÃ©gie
+$(s^t)^{t \in \Nats}$ est implantÃ©e Ã  l'aide du process  \verb+update_elems+ fourni Ã  la 
 {\sc Figure}~\ref{fig:proc}.  
-Ce process actif attend jusqu'Ã  ce qu'il soit dÃ©blocquÃ© par le process
+Ce process actif attend jusqu'Ã  ce qu'il soit dÃ©bloquÃ© par le process
 \verb+scheduler+  Ã  l'aide du sÃ©maphore \verb+unlock_elements_update+.
-L'implantation contient donc cinq Ã©tapes:
-
-\begin{enumerate}
-\item elle commence en mettant Ã  jour la variable \texttt{X} avec les valeurs de \texttt{Xp}
-  dans la fonction \texttt{update\_X} (non dÃ©taillÃ©e ici);
-\item elle mÃ©morise dans  \texttt{Xd} la valeurs disponibles des  Ã©lÃ©ments grÃ¢ce Ã  
-  la function \texttt{fetch\_values} (cf. \Sec{sub:spin:vt});
-\item  une boucle sur les  \texttt{ar\_len} Ã©lÃ©ments qui peuvent Ãªtre modifiÃ©s
-  met Ã  jour itÃ©rativement la valeur de $j$ (grace Ã  l'appel de fonction \texttt{F(j)})
-  pour peu que celui-ci doive Ãªtre modifiÃ©,  \textit{i.e.},   pour peu qu'il soit renseignÃ© dans
-  \texttt{mods[count]}; le code source de \texttt{F} est donnÃ© en {\sc Figure}~\ref{fig:p} et est une 
-  traduction directe de l'application $F$;
-\item les nouvelles valeurs des Ã©lÃ©ments \texttt{Xp} sont symbolicallement envoyÃ©s aux 
-  autres Ã©lÃ©ments qui en dÃ©pendent grÃ¢ce Ã  la fonction 
-  \texttt{diffuse\_values(Xp)} (cf. \Sec{sub:spin:vt});
-\item finallement, le process informe le scheduler de la fin de la tÃ¢che 
-  (au travers  du semaphore \texttt{sync\_mutex}).
-\end{enumerate}
-
+L'implantation se dÃ©roule en cinq Ã©tapes:
 
 \begin{figure}[t]
-  \begin{minipage}[h]{.475\linewidth}
-\begin{scriptsize}
+\begin{minipage}[b]{.32\linewidth}
+\begin{tiny}
+\begin{lstlisting}
+inline update_X(){ 	
+  int countu;
+  countu = 0;
+  do
+    :: countu == N -> break ;
+    :: countu != N ->
+       X[countu] = Xp[countu];
+       countu ++ ;
+  od
+}
+\end{lstlisting}
+\end{tiny}
+\caption{Sauvegarde de l'Ã©tat courant}\label{fig:spin:sauve}
+\end{minipage}\hfill%
+\begin{minipage}[b]{.32\linewidth}
+\begin{tiny}
 \begin{lstlisting}
 active proctype update_elems(){
  do
@@ -273,13 +353,13 @@ active proctype update_elems(){
  od
 }
 \end{lstlisting}
-\end{scriptsize}
+\end{tiny}
 \caption{Mise Ã  jour des Ã©lÃ©ments.}\label{fig:proc}
   \end{minipage}\hfill%
 %\end{figure}
 %\begin{figure}
-  \begin{minipage}[h]{.45\linewidth}
-\begin{scriptsize}
+  \begin{minipage}[b]{.33\linewidth}
+\begin{tiny}
 \begin{lstlisting}
 inline F(){
  if
@@ -293,14 +373,38 @@ inline F(){
  fi
 }
 \end{lstlisting}
-\end{scriptsize}
-\caption{Application de la fonction $F$.}\label{fig:p}
+\end{tiny}
+\caption{Application de la fonction $f$.}\label{fig:p}
   \end{minipage}
 \end{figure}
 
 
+\begin{enumerate}
+\item elle commence en mettant Ã  jour la variable \texttt{X} avec les valeurs de \texttt{Xp} dans la fonction \texttt{update\_X},~\Fig{fig:spin:sauve}
+\item elle mÃ©morise dans  \texttt{Xd} la valeurs disponible pour chaque Ã©lÃ©ment  grÃ¢ce Ã   la fonction \texttt{fetch\_values}; cette fonction est dÃ©taillÃ©e 
+dans la section suivante;
+\item  une boucle %sur les  \texttt{ar\_len} Ã©lÃ©ments qui peuvent Ãªtre modifiÃ©s
+  met Ã  jour iterrativement la valeur de $j$ (grÃ¢ce Ã  l'appel de fonction \texttt{f(j)})
+  pour peu que celui-ci doive Ãªtre modifiÃ©,  \textit{i.e.},   pour peu qu'il soit renseignÃ© dans
+  \texttt{mods[count]}; le code source de \texttt{F} est donnÃ© en {\sc Figure}~\ref{fig:p} et est une 
+  traduction directe de l'application $f$;
+\item les nouvelles valeurs des Ã©lÃ©ments \texttt{Xp} sont symboliquement
+  envoyÃ©s aux autres Ã©lÃ©ments qui en dÃ©pendent grÃ¢ce Ã  la fonction 
+  \texttt{diffuse\_values(Xp)}; cette derniÃ¨re fonction est aussi dÃ©taillÃ©e 
+  dans la section suivante; 
+\item finalement, le process informe le scheduler de la fin de la tÃ¢che 
+  (au travers  du sÃ©maphore \texttt{sync\_mutex}).
+\end{enumerate}
+
+
+
+
+
+
+
+
 \subsection{Gestion des dÃ©lais}\label{sub:spin:vt}
-Cette  section montre comment les dÃ©lais inÃ©rents au mode asynchrone sont 
+Cette  section montre comment les dÃ©lais inhÃ©rents au mode asynchrone sont 
 traduits dans le modÃ¨le  PROMELA  grÃ¢ce Ã  deux 
 fonctions \verb+fetch_values+  et   \verb+diffuse_values+.   
 Celles-ci sont donnÃ©es en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast}, 
@@ -308,7 +412,7 @@ qui rÃ©cupÃ¨rent et diffusent respectivement les valeurs des elements.
 
 \begin{figure}[t]
   \begin{minipage}[h]{.475\linewidth}
-\begin{scriptsize}
+\begin{tiny}
 \begin{lstlisting}
 inline fetch_values(){
  int countv = 0;
@@ -337,11 +441,11 @@ inline fetch_values(){
  od
 }
 \end{lstlisting}
-\end{scriptsize}
+\end{tiny}
 \caption{RÃ©cupÃ©rer les valeurs des elements\label{fig:val}}
   \end{minipage}\hfill%
   \begin{minipage}[h]{.475\linewidth}
-\begin{scriptsize}
+\begin{tiny}
 \begin{lstlisting}
 inline diffuse_values(values){   
  int countb=0;
@@ -368,54 +472,53 @@ inline diffuse_values(values){
  od
 }	
 \end{lstlisting}
-\end{scriptsize}
+\end{tiny}
 \caption{Diffuser les valeurs des elements}\label{fig:broadcast}
   \end{minipage}
 \end{figure}
 
-La premiÃ¨re fonction met Ã  jour le tableau array \verb+Xd+ recquis pour les Ã©lÃ©ments
+La premiÃ¨re fonction met Ã  jour le tableau   \verb+Xd+ requis pour les Ã©lÃ©ments
 qui doivent Ãªtre modifiÃ©s.
 Pour chaque Ã©lÃ©ment dans  \verb+mods+, identifiÃ© par la variable 
-$j$, la fonction rÃ©cupÃ¨re les valeurs  des autres Ã©lÃ©ments  (dont le libÃ©lÃ© est $i$)
-dont $j$ dÃ©pend. \JFC{vÃ©rifier si c'est ce sens ici}
+$j$, la fonction rÃ©cupÃ¨re les valeurs  des autres Ã©lÃ©ments  (dont le libellÃ© est $i$)
+dont $j$ dÃ©pend. 
 Il y a deux cas.
 \begin{itemize}
 \item puisque $i$ connaÃ®t sa derniÃ¨re valeur (\textit{i.e.},  $D^t_{ii}$ est toujours $t$)
   \verb+Xd[i].v[i]+ est donc  \verb+Xp[i]+;
-\item sinon, il y a deux sous-cas qui peuvent peuvent potentiellement modifier la valeur 
-  que $j$ a de $i$ (et qui peuvent Ãªtre choisies de maniÃ¨re allÃ©atoire):
+\item sinon, il y a deux sous cas qui peuvent peuvent potentiellement modifier la valeur 
+  que $j$ a de $i$ (et qui peuvent Ãªtre choisies de maniÃ¨re alÃ©atoire):
   \begin{itemize}
   \item  depuis la perspective de $j$ la valeur de  $i$ peut ne pas avoir changÃ©  (
     c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaÃ®t 
-    lorsqu'il n'y a pas d'arce de  $i$ Ã  $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
-    la valeur de \verb+is_succ+ qui est calculÃ©e par  \verb+hasnext(i,j)+  is 0;
+    lorsqu'il n'y a pas d'arc de  $i$ Ã  $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
+    la valeur de \verb+is_succ+ qui est calculÃ©e par  \verb+hasnext(i,j)+ est 0;
     dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiÃ©e;
   \item sinon,  on affecte Ã  \verb+Xd[j].v[i]+ la valeur mÃ©morisÃ©e
-    dansle cannal \verb+channels[i].sent[j]+  (pour peu que celui-ci ne soit pas vide).
-    Les valeurs des Ã©lÃ©ments sont ajoutÃ©es dans ce cannal au travers de la fonction  \verb+diffuse_values+
-    donnÃ©e juste aprÃ¨s.
+    dans le canal \verb+channels[i].sent[j]+  (pour peu que celui-ci ne soit pas vide).
   \end{itemize}
 \end{itemize}
 
-L'objectif de la fonction \verb+diffuse_values+  est de stocker les valeurs de $X$  reprÃ©sentÃ©
-dans le modÃ¨le par \verb+Xp+ dans le cannal  \verb+channels+.
+Les valeurs des Ã©lÃ©ments sont ajoutÃ©es dans ce canal au travers de la fonction  \verb+diffuse_values+. L'objectif de cette fonction 
+est de stocker les valeurs de $x$  (reprÃ©sentÃ©
+dans le modÃ¨le par \verb+Xp+) dans le canal  \verb+channels+.
 Il permet au modÃ¨le-checker SPIN  d'exÃ©cuter 
-le modÃ¨le PROMELA model comme s'il pouvait y avoir des dÃ©lais entre processus
+le modÃ¨le PROMELA   comme s'il pouvait y avoir des dÃ©lais entre processus
 Il y a deux cas diffÃ©rents pour la valeur de $X_{j}$:
 \begin{itemize}
 \item soit elle est \og perdue\fg{}, \og oubliÃ©e\fg{} pour permettre Ã  $i$ de ne pas tenir compte d'une 
 des valeurs de  $j$; ce cas a lieu soit lors de l'instruction  \verb+skip+ ou lorsqu'il 
 n'y a pas d'arc de $j$ Ã  $i$ dans le graphe d'incidence;
-\item soit elle est mÃ©morisÃ©e dans le cannal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein).
+\item soit elle est mÃ©morisÃ©e dans le canal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein).
 \end{itemize}
 
 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
+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 dÃ©terminisme  Ã©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 
+mise dans le canal, elle serait immÃ©diatement consommÃ©e, ce qui est contradictoire avec la notion de 
 dÃ©lai.
 
 % \subsection{Discussion}
@@ -433,527 +536,265 @@ dÃ©lai.
 % 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 
+\subsection{PropriÃ©tÃ© de convergence universelle}
+Il reste Ã  formaliser dans le model checker SPIN le fait que les 
+itÃ©rations d'un systÃ¨me 
 dynamique Ã  $n$ Ã©lÃ©ments est universellement convergent.
 
-We first recall that the
-variables \verb+X+  and \verb+Xp+ respectively  contain the value of  $X$ before
-and after  an update.  Then,  by applying a non-deterministic  initialization of
-\verb+Xp+  and  applying  a   pseudo-periodic  strategy,  it  is  necessary  and
-sufficient to establish the following Linear Temporal Logic (LTL) formula:
+Rappelons tout d'abord que les variables \verb+X+  et \verb+Xp+ 
+contiennent respectivement la valeur de $x$ avant et aprÃ¨s la mise Ã  jour. 
+Ainsi, si l'on effectue une initialisation  non dÃ©terministe de 
+\verb+Xp+  et si l'on applique une stratÃ©gie pseudo pÃ©riodique,  
+il est nÃ©cessaire et suffisant
+de prouver la formule temporelle linÃ©aire (LTL) suivante:
 \begin{equation}
 \diamond  (\Box  \verb+Xp+ = \verb+X+)
 \label{eq:ltl:conv}
 \end{equation}
-where $\diamond$  and $\Box$ have the usual  meaning \textit{i.e.}, respectively
-{\em eventually} and {\em always} in  the subsequent path.  It is worth noticing
-that this property only ensures the stabilization of the system, but it does not
-provide any information  over the way the system  converges. In particular, some
-indeterminism  may still  be present  under the  form of  multiple  fixed points
-accessible from some initial states.
-
-
-
-\section{Proof of Translation Correctness}\label{sec:spin:proof}
-\JFC{DÃ©placer les preuves en annexes}
-
-This  section  establishes  the  soundness  and  completeness  of  the  approach
-(Theorems~\ref{Theo:sound}  and ~\ref{Theo:completeness}). Technical  lemmas are
-first shown to ease the proof of the two theorems.
-   
-
-% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock}
-%   Let $\phi$ be a DDN model and $\psi$ be its translation.  There is no deadlock
-%   in any execution of $\psi$.
-% \end{Lemma}
-% \begin{Proof}
-%   In current  translation, deadlocks of  PROMELA may only be  introduced through
-%   sending  or  receiving messages  in  channels.   Sending  (resp. receiving)  a
-%   message in the  \verb+diffuse_values+ (resp.  \verb+fetch_values+) function is
-%   executed  only if  the  channel is  not full  (resp.  is not  empty).  In  the
-%   \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value
-%   in     any     semaphore     channel    (\verb+unlock_elements_update+     and
-%   \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the
-%   way.
-% \end{Proof}
-
-
-\begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
-  Let $\phi$  be a  DDN with strategy  $(S^t)^{t \in  \Nats}$ and $\psi$  be its
-  translation.  There exists an execution of $\psi$ with weak fairness s.t.  the
-  scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$.
-\end{lemma}
-\begin{Proof}
-  The proof is direct  for $t=0$. Let us suppose it is  established until $t$ is
-  some $t_0$.  Let  us consider pseudo-periodic strategies.  Thanks  to the weak
-  fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at
-  iteration $t$.
-\end{Proof}
-
-In     what     follows,     let     $Xd^t_{ji}$     be     the     value     of
-\verb+Xd[+$j$\verb+].v[+$i$\verb+]+  after  the   $t^{\text{th}}$  call  to  the
-function  \verb+fetch_values+.  Furthermore,  let $Y^k_{ij}$  be the  element at
-index  $k$  in  the  channel  \verb+channels[i].sent[j]+ of  size  $m$,  $m  \le
-\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are  respectively the head and the tail
-of the  channel.  Secondly, let $(M_{ij}^t)^{t \in  \{1, 1.5, 2, 2.5,\ldots\}}$ be a
-sequence such  that $M_{ij}^t$ is the  partial function that  associates to each
-$k$, $0 \le k \le  m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering
-into the \verb+update_elems+ at iteration $t$ where
-% \begin{itemize}
-% \item
- $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+
-  at index $k$,
-%\item 
-$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and
-%\item 
-$c^k_{ij}$ is the  first date at which the value is  available on $j$. So,
-  the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$.
-%\end{itemize}
-$M_{ij}^t$ has the following signature:
-\begin{equation*}
-\begin{array}{rrcl}
-M_{ij}^t: & 
-\{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\
-& k  \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}).
-\end{array}  
-\end{equation*}
-
-Intuitively,  $M_{ij}^t$  is  the  memory  of  \verb+channels[i].sent[j]+  while
-starting the iteration $t$.  Notice that the domain of any $M_{ij}^1$ is $\{0\}$
-and   $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    indeed,   the   \verb+init+   process
-initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+.
-
-Let us  show how  to make the  indeterminism inside the  two functions\linebreak
-\verb+fetch_values+  and  \verb+diffuse_values+  compliant with  \Equ{eq:async}.
-The  function   $M_{ij}^{t+1}$  is  obtained   by  the  successive   updates  of
-$M_{ij}^{t}$  through   the  two  functions\linebreak   \verb+fetch_values+  and
-\verb+diffuse_values+.   Abusively,   let  $M_{ij}^{t+1/2}$  be   the  value  of
-$M_{ij}^{t}$ after the former function during iteration $t$.
-
-In  what follows, we  consider elements  $i$ and  $j$ both  in $\llbracket  1, n
-\rrbracket$   that  are   updated.   At   iteration   $t$,  $t   \geq  1$,   let
-$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of
-\verb+fetch_values+.   If $t$  is  equal  to $c^0_{ij}+1$  then  we execute  the
-instruction    that   assigns    $Y^0_{ij}$   (\textit{i.e.},     the   head    value   of
-\verb+channels[i].sent[j]+)  to   $Xd_{ji}^t$.   In  that   case,  the  function
-$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each
-$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$.
-Otherwise (\textit{i.e.}, when  $t < c^0_{ij}+1$ or when  the domain of $M_{ij}$
-is  empty)   the  \verb+skip+  statement  is  executed   and  $M_{ij}^{t+1/2}  =
-M_{ij}^{t}$.
-
-In the function \verb+diffuse_values+, if  there exists some $\tau$, $\tau\ge t$
-such that \mbox{$D^{\tau}_{ji} = t$}, let  $c_{ij}$ be defined by $ \min\{l \mid
-D^{l}_{ji} =  t \} $.  In  that case, we  execute the instruction that  adds the
-value   \verb+Xp[i]+   to  the   tail   of  \verb+channels[i].sent[j]+.    Then,
-$M_{ij}^{t+1}$ is defined  as an extension of $M_{ij}^{t+1/2}$  in $m$ such that
-$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$.  Otherwise (\textit{i.e.}, when $\forall l
-\, .  \, l \ge t  \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+
-statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
-
-
-\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution}
-  For any sequences $(S^t)^{t  \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for
-  any map $F$ there exists a SPIN  execution such that for any iteration $t$, $t
-  \ge  1$, for  any $i$ and $j$ in  $\llbracket 1, n \rrbracket$  we  have the
-  following properties:
-   
-\noindent If the domain of $M_{ij}^t$ is not empty, then
-\begin{equation}
-  \left\{
-    \begin{array}{rcl}
-      M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
-      \textrm{if $t \geq 2$ then }M_{ij}^t(0) & = &
-      \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
-      c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
-    \end{array}
-  \right.
-  \label{eq:Mij0}
-\end{equation}
-\noindent Secondly we have:
-\begin{equation}
-  \forall t'\, .\,   1 \le t' \le t  \Rightarrow   Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
-  \label{eq:correct_retrieve}
-\end{equation}
-\noindent Thirdly, for any $k\in S^t$.  Then, the value of the computed variable
-\verb+Xp[k]+  at  the  end  of  the  \verb+update_elems+  process  is  equal  to
-$X_k^{t}$          \textit{i.e.},          $F_{k}\left(         X_1^{D_{k\,1}^{t-1}},\ldots,
-  X_{n}^{D_{k\,{n}}^{t-1}}\right)$ at the end of the $t^{\text{th}}$ iteration.
-\end{lemma}
-\begin{Proof}
-The proof is done by induction on the number of iterations.
-
-\paragraph{Initial case:}
-
-For the first  item, by definition of $M_{ij}^t$, we  have $M_{ij}^1(0) = \left(
-  \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}},
-  0,0 \right)$.
-
-Next, the first call to  the function \verb+fetch_value+ either assigns the head
-of   \verb+channels[i].sent[j]+  to   \verb+Xd[j].v[i]+  or   does   not  modify
-\verb+Xd[j].v[i]+.  Thanks to  the \verb+init+ process, both cases  are equal to
-\verb+Xp[i]+,  \textit{i.e.}, $X_i^0$.  The  equation (\ref{eq:correct_retrieve})  is then
-established.
-
-
-For  the last  item, let  $k$, $0  \le  k \le  n-1$.  At  the end  of the  first
-execution\linebreak   of   the  \verb+update_elems+   process,   the  value   of
-\verb+Xp[k]+       is\linebreak       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
-\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.  Thus,  by definition of $Xd$,  it is equal
-to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$.  Thanks to \Equ{eq:correct_retrieve},
-we can conclude the proof.
-
-
-
-\paragraph{Inductive case:}
-
-Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
-
-First,  if domain  of definition  of the  function $M_{ij}^l$  is not  empty, by
-induction  hypothesis $M_{ij}^{l}(0)$  is  $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
-\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-At iteration $l$, if  $l < c + 1$ then the  \verb+skip+ statement is executed in
-the   \verb+fetch_values+  function.   Thus,   $M_{ij}^{l+1}(0)$  is   equal  to
-$M_{ij}^{l}(0)$.  Since $c > l-1$  then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
-is $\min\{k  | D_{ji}^k  > D_{ji}^{l-1} \}$.  Obviously, this implies  also that
-$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-We now consider that at iteration $l$, $l$ is $c + 1$.  In other words, $M_{ij}$
-is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$:
-\begin{itemize}
-\item  if $\dom(M_{ij}^{l})=\{0\}$  and $\forall  k\,  . \,  k\ge l  \Rightarrow
-  D^{k}_{ji} \neq l$  is established then $\dom(M_{ij}^{l+1})$ is  empty and the
-  first item of the lemma  is established; 
-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists  k\, . \, k\ge l \land D^{k}_{ji}
-  = l$  is established then $M_{ij}^{l+1}(0)$  is $(\verb+Xp[i]+,l,c_{ij})$ that
-  is  added  in  the  \verb+diffuse_values+ function  s.t.\linebreak  $c_{ij}  =
-  \min\{k  \mid  D^{k}_{ji}  = l  \}  $.   Let  us  prove  that we  can  express
-  $M_{ij}^{l+1}(0)$  as  $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$  where
-  $c'$ is  $\min\{k |  D_{ji}^k > D_{ji}^{l-1}  \}$.  First,  it is not  hard to
-  establish that  $D_{ji}^{c_{ij}}= l \geq  D_{ji}^{l} > D_{ji}^{l-1}$  and thus
-  $c_{ij}  \geq   c'$.   Next,  since   $\dom(M_{ij}^{l})=\{0\}$,  then  between
-  iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
-  not updated $M_{ij}$.  Formally we have
-$$
-\forall t,k  \, .\, D_{ji}^c <  t < l \land  k \geq t  \Rightarrow D_{ji}^k \neq
-t.$$
-
-Particularly, $D_{ji}^{c'} \not  \in \{D_{ji}^{c}+1,\ldots,l-1\}$.  We can apply
-the     third    item     of    the     induction    hypothesis     to    deduce
-$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude.
-
-\item  if   $\{0,1\}  \subseteq  \dom(M_{ij}^{l})$   then  $M_{ij}^{l+1}(0)$  is
-  $M_{ij}^{l}(1)$.   Let  $M_{ij}^{l}(1)=  \left(\verb+Xp[i]+, a_{ij}  ,  c_{ij}
-  \right)$.   By  construction $a_{ij}$  is  $\min\{t'  |  t' >  D_{ji}^c  \land
-  (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k |
-  D_{ji}^k = a_{ij}\}$.  Let us show  $c_{ij}$ is equal to $\min\{k | D_{ji}^k >
-  D_{ji}^{l-1} \}$ further  referred as $c'$.  First we  have $D_{ji}^{c_{ij}} =
-  a_{ij} >  D_{ji}^c$. Since $c$  by definition is  greater or equal to  $l-1$ ,
-  then $D_{ji}^{c_{ij}}>  D_{ji}^{l-1}$ and then $c_{ij} \geq  c'$.  Next, since
-  $c$ is  $l-1$, $c'$ is $\min\{k |  D_{ji}^k > D_{ji}^{c} \}$  and then $a_{ij}
-  \leq  D_{ji}^{c'}$. Thus,  $c_{ij} \leq  c'$  and we  can conclude  as in  the
-  previous part.
-\end{itemize}
-
-
-The case where  the domain $\dom(M^l_{ij})$ is empty but  the formula $\exists k
-\, .\, k \geq  l \land D_{ji}^k = l$ is established  is equivalent to the second
-case given above and then is omitted.
-
-
-Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}).  At iteration
-$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.  Two cases
-have to be  considered depending on whether $D_{ji}^{l}$  and $D_{ji}^{l-1}$ are
-equal or not.
-\begin{itemize}
-\item If  $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'}  > D_{ji}^{l-1}$, then
-  $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$  is distinct from $l$. Thus, the SPIN
-  execution detailed  above does not  modify $Xd_{ji}^{l+1}$.  It is  obvious to
-  establish   that   $Xd_{ji}^{l+1}  =   Xd_{ji}^{l}   =  X_i^{D_{ji}^{l-1}}   =
-  X_i^{D_{ji}^{l}}$.
-\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$.
-  According     to     \Equ{eq:Mij0}     we     have    proved,     we     have
-  $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$.   Then  the SPIN  execution
-  detailed above  assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$,  which ends the
-  proof of (\ref{eq:correct_retrieve}).
-\end{itemize}
+oÃ¹ les opÃ©rateur  $\diamond$ et  $\Box$ ont
+la sÃ©mantique usuelle, Ã  savoir
+respectivement {\em Ã©ventuellement} et {\em toujours} dans les chemins suivants.
+On note que cette propriÃ©tÃ©, si elle est Ã©tablie, garantit
+la stabilisation du systÃ¨me.
+Cependant elle ne donne aucune mÃ©trique quant Ã 
+la maniÃ¨re dont celle-ci est obtenue.
+En particulier, on peut converger trÃ¨s lentement ou le systÃ¨me peut mÃªme 
+disposer de plusieurs points fixes.
 
-We are left to prove the induction of  the third part of the lemma.  Let $k$, $k
-\in S^{l+1}$. % and $\verb+k'+ = k-1$.
-At the  end of the first  execution of the \verb+update_elems+  process, we have
-$\verb+Xp[+k\verb+]+=                                   F(\verb+Xd[+k\verb+][0]+,
-\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.  By  definition of $Xd$,  it is equal
-to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
-\Equ{eq:correct_retrieve} we have proved, we can conclude the proof.
-\end{Proof}
 
 
-\begin{lemma}
-  Bounding the size of channels  to $\textit{max} = \delta_0$ is sufficient when
-  simulating a DDN where delays are bounded by $\delta_0$.
-\end{lemma}
+\section{Correction et complÃ©tude de la dÃ©marche}\label{sec:spin:proof}
 
-\begin{Proof}
-  For  any $i$,  $j$, at  each  iteration $t+1$,  thanks to  bounded delays  (by
-  $\delta_0$),  element $i$  has to  know at  worst $\delta_0$  values  that are
-  $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$.  They  can be stored into any channel
-  of size $\delta_0$.
-\end{Proof}
+Cette section prÃ©sente les thÃ©orÃ¨mes
+de correction et de  complÃ©tude de l'approche.
+(ThÃ©orÃ¨mes~\ref{Theo:sound} et~\ref{Theo:completeness}). 
+Toutes les preuves sont dÃ©placÃ©es en 
+annexes~\ref{anx:promela}.
 
 
-\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound}
-  Let $\phi$ be  a DDN model and $\psi$ be its  translation.  If $\psi$ verifies
-  the  LTL  property  (\ref{eq:ltl:conv})  under weak  fairness  property,  then
-  iterations of $\phi$ are universally convergent.
-\end{theorem}
-\begin{Proof}
-%   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
-%   verification  is achieved  under  weak fairness  property.  Instructions  that
-%   write or read into \verb+channels[j].sent[i]+ are continuously enabled leading
-%   to  convenient  available  dates  $D_{ji}$.   It is  then  easy  to  construct
-%   corresponding iterations of the DDN that are convergent.
-% \ANNOT{quel sens donnes-tu a \emph{convenient} ici ?}
-
-  Let us show the contraposition of the theorem.  The previous lemmas have shown
-  that for any  sequence of iterations of the DDN, there  exists an execution of
-  the PROMELA  model that  simulates them.   If some iterations  of the  DDN are
-  divergent, then  they prevent  the PROMELA model  from stabilizing,  \textit{i.e.},  not
-  verifying the LTL property (\ref{eq:ltl:conv}).
-\end{Proof}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
+  Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction PROMELA.  
+  Si $\psi$ vÃ©rifie
+  la propriÃ©tÃ©  LTL  (\ref{eq:ltl:conv})  sous hypothÃ¨se d'Ã©quitÃ© faible,  alors
+  les itÃ©rations de $\phi$ sont universellement convergentes.
+\end{restatable}
 
 
-% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
-% Let $\phi$ be a DDN model where strategy, $X^(0)$ 
-% are only constrained to be pseudo-periodic and
-% in $E$ respectively.
-% Let $\psi$ be its translation.
-% If all the executions of $\psi$ converge, 
-% then  iterations of $\phi$ are universally convergent.
-% \end{Corol}
+\begin{restatable}[ComplÃ©tude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
+  Soit $\phi$ un modÃ¨le de systÃ¨me dynamique discret et $\psi$ sa traduction.  Si $\psi$ ne vÃ©rifie pas 
+  la propriÃ©tÃ© LTL (\ref{eq:ltl:conv}) sous hypothÃ¨se d'Ã©quitÃ© faible,
+  alors les itÃ©rations de  $\phi$ ne sont pas universellement convergentes.
+\end{restatable}
 
 
 
-\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness}
-  Let $\phi$ be a  DDN model and $\psi$ be its translation.   If $\psi$ does not
-  verify the LTL property  (\ref{eq:ltl:conv}) under weak fairness property then
-  the iterations of $\phi$ are divergent.
-\end{theorem}
-\begin{Proof}
-  For models $\psi$  that do not verify the  LTL property (\ref{eq:ltl:conv}) it
-  is easy  to construct corresponding iterations  of the DDN,  whose strategy is
-  pseudo-periodic since weak fairness property is taken into account.
-
-%   i.e. iterations that  are divergent.   Executions are
-%   performed under weak  fairness property; we then detail  what are continuously
-%   enabled:
-% \begin{itemize}
-% \item if the strategy is not  defined as periodic, elements $0$, \ldots, $n$ are
-%   infinitely often updated leading to pseudo-periodic strategy;
-% \item  instructions  that  write  or read  into  \verb+channels[j].sent[i]+  are
-%   continuously enabled leading to convenient available dates $D_{ji}$.
-% \end{itemize}
-% The simulated DDN does not stabilize and its iterations are divergent.
- \end{Proof}
 
 
 
-\section{Practical Issues}
+\section{DonnÃ©es pratiques}
 \label{sec:spin:practical}
-This  section  first  gives  some  notes about  complexity  and  later  presents
-experiments.
-%\subsection{Complexity Analysis}
-%\label{sub:spin:complexity}
-\begin{theorem}[Number of states]
-  Let $\phi$ be a DDN model with  $n$ elements, $m$ edges in the incidence graph
-  and $\psi$ be  its translation into PROMELA.  The  number of configurations of
-  the $\psi$ SPIN execution is bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
+Cette section donne tout d'abord quelques mesures de complexitÃ© de l'approche 
+puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
+
+\begin{theorem}[Nombre d'Ã©tats ]
+  Soit  $\phi$  un modÃ¨le de systÃ¨me dynamique discret Ã   $n$ Ã©lÃ©ments, $m$ 
+  arcs dans le graphe d'incidence
+  et $\psi$ sa traduction en PROMELA.  Le nombre de configurations 
+  de l'exÃ©cution en SPIN de $\psi$ est bornÃ©e par $2^{m(\delta_0+1)+n(n+2)}$.
 \end{theorem}
 \begin{Proof}
-  A configuration is a valuation  of global variables. Their number only depends
-  on those that are not constant.
-
-  The  variables  \verb+Xp+ \verb+X+  lead  to  $2^{2n}$  states.  The  variable
-  \verb+Xs+ leads to $2^{n^2}$ states.  Each channel of \verb+array_of_channels+
-  may  yield $1+2^1+\ldots+2^{\delta_0}=  2^{\delta_0+1}-1$  states.  Since  the
-  number of  edges in  the incidence  graph is $m$,  there are  $m$ non-constant
-  channels,  leading  to  approximately $2^{m\times(\delta_0+1)}$  states.   The
-  number of configurations is then bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
-  Notice that  this bound is tractable  by SPIN for  small values of $n$, 
-  $m$ and $\delta_0$.
+  Une configuration est une valuation des variables globales.
+  Leur nombre ne dÃ©pend que de celles qui ne sont pas constantes.
+
+  Les  variables  \verb+Xp+ et \verb+X+ engendrent  $2^{2n}$ Ã©tats.
+  La variable
+  \verb+Xs+ gÃ©nÃ¨re $2^{n^2}$ Ã©tats.  
+  Chaque canal de \verb+array_of_channels+
+  peut engendrer $1+2^1+\ldots+2^{\delta_0}=  2^{\delta_0+1}-1$  Ã©tats. 
+  Puisque le nombre d'arÃªtes du graphe d'incidence  est $m$,  
+  il y a  $m$ canaux non constants,  ce qui gÃ©nÃ¨re approximativement $2^{m(\delta_0+1)}$ Ã©tats. 
+  Le nombre de configurations est donc bornÃ© par $2^{m(\delta_0+1)+n(n+2)}$.
+  On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de  $n$, 
+  $m$ et $\delta_0$.
+  \JFC{Donner un ordre de grandeur de cet ordre de grandeur}
+  
 \end{Proof}
 
+La mÃ©thode dÃ©taillÃ©e ici a pu Ãªtre appliquÃ©e sur l'exemple jouet
+pour prouver formellement sa convergence universelle.
 
-
-The  method detailed along  the line  of this  article has  been applied  on the
-running example to formally prove its universally convergence.
-
-First  of all,  SPIN only  considers  weak fairness  property between  processes
-whereas  above  proofs need  such  a  behavior to  be  established  each time  a
-non-deterministic choice is done.
-
-
-A first attempt has consisted in building the following formula
-each time an undeterministic choice between $k$ elements 
-respectively labeled $l1$, \ldots $lk$ occurs:  
+On peut remarquer que SPIN n'impose l'Ã©quitÃ© faible qu'entre les process
+alors que les preuves des deux thÃ©orÃ¨mes prÃ©cÃ©dentes reposent sur le fait que 
+celle-ci est Ã©tablie dÃ¨s qu'un choix indÃ©terministe est effectuÃ©.
+NaÃ¯vement, on pourrait considÃ©rer comme hypothÃ¨se la formule suivante 
+chaque fois qu'un choix indÃ©terministe se produit entre $k$ Ã©vÃ©nements
+respectivement notÃ©s $l_1$, \ldots $l_k$:  
 $$
-[] <> (l == l0) \Rightarrow 
-(([] <> (l== l1)) \land  \ldots \land ([] <> (l == lk)))
+\Box \diamond (l == l_0) \Rightarrow 
+((\Box \diamond (l== l_1)) \land  \ldots \land (\Box \diamond (l == l_k)))
 $$
-where label $l0$ denotes the line before the choice.
-This formula exactly translates the fairness property.
-The negation of such a LTL formula may then be efficiently translated  
-into a BÃ¼chi automata  with the tool ltl2ba~\cite{GO01}.
-However due to an explosion of the size of the product 
-between this automata and the automata issued from the PROMELA program 
-SPIN did not success to verify whether the property is established or not. 
-
-This problem has been practically tackled by leaving spin generating all the (not necessarily fair) computations and verifying convergence property on them.
-We are then left to interpret its output with two issues.
-If property is established for all the computations, 
-it is particularly established for fair ones and iterations are convergent. 
-In the opposite case, when facing to a counter example, an analysis of the SPIN 
-output is achieved. 
-\begin{xpl}
-Experiments have shown that all the iterations of the running example are 
-convergent for a delay equal to 1 in less than 10 min.
-The example presented in~\cite{abcvs05} with five elements taking boolean 
-values has been verified with method presented in this article.   
-Immediately, SPIN computes a counter example, that unfortunately does not
-fulfill fairness properties. Fair counter example is obtained
-after few minutes.
-All the experimentation have been realized in a classic desktop computer.
-\end{xpl}
-
-
-
 
+oÃ¹ le libellÃ© $l_0$ dÃ©note le libellÃ© de la ligne prÃ©cÃ©dent 
+le choix indÃ©terministe.
+Cette formule traduit exactement l'Ã©quitÃ© faible.
+Cependant en raison de l'explosion de la taille du produit entre 
+l'automate de BÃ¼chi issu de cette formule et celui issu du programme  PROMELA,
+SPIN n'arrive pas Ã  vÃ©rifier si la convergence universelle est Ã©tablie 
+ou non sur des exemples 
+simples\JFC{faire rÃ©fÃ©rence Ã  un tel exemple}. 
+
+Ce problÃ¨me a Ã©tÃ© pratiquement rÃ©solu en laissant SPIN 
+gÃ©nÃ©rer toutes les traces d'exÃ©cution,
+mÃªme celles qui ne sont pas Ã©quitables, 
+puis ensuite vÃ©rifier la propriÃ©tÃ© de convergence sur toutes celles-ci. 
+Il reste alors Ã  interprÃ©ter les rÃ©sultats qui peuvent Ãªtre de deux types. Si la convergence est 
+Ã©tablie pour toutes les traces, elle le reste en particulier pour les traces Ã©quitables.
+Dans le cas contraire on doit analyser le contre exemple produit par SPIN.
+
+% \begin{xpl}
+% \JFC{Reprendre ce qui suit}
+% Experiments have shown that all the iterations of the running example are 
+% convergent for a delay equal to 1 in less than 10 min.
+% The example presented in~\cite{abcvs05} with five elements taking boolean 
+% values has been verified with method presented in this article.   
+% Immediately, SPIN computes a counter example, that unfortunately does not
+% fulfill fairness properties. Fair counter example is obtained
+% after few minutes.
+% All the experimentation have been realized in a classic desktop computer.
+% \end{xpl}
+
+
+La mÃ©thode dÃ©taillÃ©e ici a Ã©tÃ© appliquÃ©e sur des exemples pour prouver formellement 
+leur convergence ou leur divergence (\Fig{fig:async:exp}).
+Dans ces expÃ©riences, les dÃ©lais ont Ã©tÃ© bornÃ©s par $\delta_0=10$.
+Dans ce tableau,  $P$ est vrai ($\top$) si et seulement si la convergence 
+universelle 
+est Ã©tablie et faux ($\bot$) sinon. Le nombre $M$ est 
+la taille de la  mÃ©moire consommÃ©e (en MB) et 
+$T$ est le temps d'exÃ©cution sur un  Intel Centrino Dual Core 2 Duo @1.8GHz avec 2GB de mÃ©moire vive
+pour Ã©tablir un verdict.
+
+
+\begin{figure}
+\begin{center}
+\begin{tiny}
+\begin{tabular}{|*{7}{c|}}
+\cline{2-7}
+\multicolumn{1}{c|}{ }
+&\multicolumn{3}{|c|}{ParallÃ¨les} & \multicolumn{3}{|c|}{Chaotiques} \\
+\cline{2-7}
+\multicolumn{1}{c|}{ }& 
+P & M & T&
+P & M & T \\
+\hline %\cline{2-7}
+\textit{RE}  &
+$\top$ & 2.7 & 0.01s & 
+$\bot$ & 369.371 & 0.509s \\ 
+\hline %\cline{2-7}
+\cite{RC07} &
+$\bot$ & 2.5 & 0.001s & % RC07_sync.spin
+$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
+\hline
+\cite{BM99} &
+$\top$ & 36.7 & 12s & % BM99_sync_para.spin
+$\top$ &  &  \\ % BM99_sync_chao.spin
+\hline
+\end{tabular}
+\end{tiny}
+\end{center}
+\caption{ExpÃ©rimentations avec des itÃ©rations synchrones}\label{fig:sync:exp}
+\end{figure} 
+
+
+
+\begin{figure}
+\begin{center}
+\tiny
+\begin{tabular}{|*{13}{c|}}
+\cline{2-13}
+\multicolumn{1}{c|}{ }
+&\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
+\cline{2-13}
+\multicolumn{1}{c|}{ }
+&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
+\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
+\cline{2-13}
+\multicolumn{1}{c|}{ }
+&P & M & T &
+P & M & T &
+P & M & T&
+P & M & T \\
+\hline %cline{2-13}
+\textit{RE} & 
+$\top$ & 409 & 1m11s&
+$\bot$ & 370 & 0.54 &
+$\bot$ & 374 & 7.7s&
+$\bot$ & 370 & 0.51s \\
+\hline %\cline{2-13}
+AC2D 
+&$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
+&$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
+&$\bot$ & 2.5 & 0.01s   % RC07_async.spin
+&$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
+\hline %\cline{2-13}
+\cite{BM99}
+&$\top$ &  &   %BM99_mixed_para.spin 
+&$\top$ &  &    % RC07_async_mixed_all.spin
+&$\bot$ &  &    % RC07_async.spin
+&$\bot$ &  &   \\ % RC07_async_all.spin 
+\hline %\cline{2-13}
+\end{tabular}
+\end{center}
+\caption{ExpÃ©rimentations avec des itÃ©rations asynchrones}\label{fig:async:exp}
+\end{figure} 
+
+
+
+L'exemple \textit{RE} est l'exemple jouet de ce chapitre,
+\cite{RC07} concerne un rÃ©seau composÃ© de deux gÃ¨nes
+Ã  valeur dans $\{0,1,2\}$,
+AC2D est un automate cellulaire  avec 9 elements prenant des
+valeurs boolÃ©ennes en fonction de 
+de 4 voisins et
+\cite{BM99} consiste en  10 process
+qui modifient leur valeur boolÃ©ennes dans un graphe d'adjacence proche 
+du graphe complet.
+
+
+L'exemple jouet \textit{RE} a Ã©tÃ© prouvÃ© comme universellement convergent.
+\JFC{statuer sur AC2D}
+Comme la convergence n'est dÃ©jÃ  pas Ã©tablie pour les itÃ©rations parallÃ¨les
+de~\cite{RC07}, il en est donc 
+de mÃªme pour les itÃ©rations asynchrones.
+La {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant Ã  la violation 
+de la convergence. Celle-ci correspond Ã  une stratÃ©gie pÃ©riodique qui rÃ©pÃ¨te
+$\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et dÃ©bute avec $x=(0,0)$.
+En raison de la dÃ©pendance forte entre les Ã©lÃ©ments
+de~\cite{BM99}, 
+$\delta_0$ est rÃ©duit Ã  1. Cela aboutit cependant Ã  $2^{100}$ 
+configurations dans le mode des itÃ©rations asynchrones.
+
+\JFC{Quid de ceci?}
+La convergence des itÃ©rations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas Ã©tablie 
+lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
+
+\begin{figure}
+\centering
+\includegraphics[scale=0.6]{images/RC07ce.eps}   
+\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
+\end{figure}
 
-%However preliminary experiments have shown the interest of the approach.  
-
-
-
-% The method detailed along the line of this article has been 
-% applied on some examples to formally prove their convergence
-% (Fig.~\ref{fig:async:exp}).
-% In these experiments, Delays are supposed to be bounded by $\delta_0$ set to 10.
-% In these arrays, 
-% $P$ is true ($\top$) provided the  uniform convergence property is established, false ($\bot$) otherwise,  
-% $M$ is the amount of memory usage (in MB) and 
-% $T$ is the time needed on a Intel Centrino Dual Core 2 Duo @1.8GHz  with 2GB of memory, both  
-% to establish or refute the property.
-
-% RE is the running example of this article, 
-% AC2D is a cellular automata with 9 elements taking boolean values
-% according their four neighbors 
-% and BM99 is has been proposed in~\cite{BM99} and consists of 10 process
-% modifying their boolean values, but with many connected connection graph. 
-
-
-
-
-
-% \begin{figure}
-% \begin{center}
-% \scriptsize
-% \begin{tabular}{|*{13}{c|}}
-% \cline{2-13}
-% \multicolumn{1}{c|}{ }
-% &\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
-% \cline{2-13}
-% \multicolumn{1}{c|}{ }
-% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
-% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-% \cline{2-13}
-% \multicolumn{1}{c|}{ }
-% &P & M & T &
-% P & M & T &
-% P & M & T&
-% P & M & T \\
-% \hline %cline{2-13}
-% Running Example & 
-% $\top$ & 409 & 1m11s&
-% $\bot$ & 370 & 0.54 &
-% $\bot$ & 374 & 7.7s&
-% $\bot$ & 370 & 0.51s \\
-% \hline %\cline{2-13}
-% AC2D 
-% &$\bot$ & 2.5 & 0.001s  % RC07_async_mixed.spin
-% &$\bot$ & 2.5 & 0.01s   % RC07_async_mixed_all.spin
-% &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
-% &$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
-% \hline %\cline{2-13}
-% BM99 
-% &$\top$ &  &   %BM99_mixed_para.spin 
-% &$\top$ &  &    % RC07_async_mixed_all.spin
-% &$\bot$ &  &    % RC07_async.spin
-% &$\bot$ &  &   \\ % RC07_async_all.spin 
-% \hline %\cline{2-13}
-% \end{tabular}
-% \end{center}
-% \caption{Experimentations with Asynchronous Iterations}\label{fig:async:exp}
-% \end{figure} 
-
-
-
-% The example~\cite{RC07} deals with a network composed of two genes taking their 
-% values into $\{0,1,2\}$. Since parallel iterations is already diverging, 
-% the same behavior is observed for all other modes.
-% The Figure~\ref{fig:RC07CE} gives the trace leading to convergence property 
-% violation output by SPIN.
-% It corresponds to peridic strategy that repeats $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ and starts with $X=(0,0)$.
-   
-  
-% In the example extracted from~\cite{BM99},
-% we have 10 processors computing a binary value.
-% Due to the huge number of  dependencies between these calculus, 
-% $\delta_0$ is reduced to 1. It nevertheless leads to about $2^{100}$ 
-% configurations in asynchronous iterations.
-
-% Let us focus on checking universal convergence of asynchronous iterations 
-% of example~\cite{BCVC10:ir}. 
-% With a $\delta_0$ set to 5, SPIN generates an out of memory error.  
-% However, it succeed to prove that the property is not established even
-% with $\delta_0$ set to 1 which is then sufficient.
-
-
-% \begin{figure}
-% \begin{center}
-% \begin{tiny}
-% \begin{tabular}{|*{7}{c|}}
-% \cline{2-7}
-% \multicolumn{1}{c|}{ }
-% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-% \cline{2-7}
-% \multicolumn{1}{c|}{ }& 
-% P & M & T&
-% P & M & T \\
-% \hline %\cline{2-7}
-% Running  &
-% $\top$ & 2.7 & 0.01s & 
-% $\bot$ & 369.371 & 0.509s \\ 
-% \hline %\cline{2-7}
-% \cite{RC07} example &
-% $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
-% $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
-% \hline
-% \cite{BM99} example &
-% $\top$ & 36.7 & 12s & % BM99_sync_para.spin
-% $\top$ &  &  \\ % BM99_sync_chao.spin
-% \hline
-% \end{tabular}
-% \end{tiny}
-% \end{center}
-% \caption{Experimentations with Synchronous Iterations}\label{fig:sync:exp}
-% \end{figure} 
 
 
 
 
 
 
-% \begin{tabular}{|*{}{c|}}
+% \begin{tabular}{|*{19}{c|}}
 % % \hline 
 % % e \\
 % % 
@@ -971,42 +812,30 @@ All the experimentation have been realized in a classic desktop computer.
 % \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\
 
 
-% \end{tabular}
+%  \end{tabular}
 
  
-\section{Conclusion and Future Work}
+\section{Conclusion}
 \label{sec:spin:concl}
-Stochastic based prototypes have been implemented to generate both 
-strategies and delays for asynchronous iterations in first in~\cite{BM99,BCV02}.
-However, since these research softwares are not exhaustive, they really give an 
-formal answer when they found a counterexample. When facing convergence, they only convince 
-the user about this behavior  without exhibiting a proof. 
- 
-As far as we know, no implemented formal method tackles the problem of
-proving asynchronous iterations convergence. 
-In the theoretical work~\cite{Cha06} Chandrasekaran shows that asynchronous iterations
-are convergent iff we can build a decreasing Lyaponov function, 
-but does not gives any automated method to compute it.  
-
-In this work, we  have shown how convergence proof for any asynchronous
-iterations of  discrete dynamical networks  with bounded delays
-can be automatically achieved.
-The key idea is to translate the network (map, strategy) into PROMELA and 
-to leave the SPIN model checker establishing the validity 
-of the temporal property corresponding to the convergence.
-The correctness and completeness of the approach have been proved, notably 
-by computing a SPIN execution of the PROMELA model that have the same
-behaviors than initial network.
-The complexity of the problem is addressed. It shows that non trivial example 
-may be addressed by this technique.
-
+Des mÃ©thodes de simulation basÃ©es sur des stratÃ©gies et des dÃ©lais gÃ©nÃ©rÃ©s alÃ©atoirement 
+ont dÃ©jÃ  Ã©tÃ© prÃ©sentÃ©es~\cite{BM99,BCV02}.
+Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un rÃ©sultat 
+formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,  
+cela ne permet que donner une intuition de convergence, pas  une preuve.
+Autant que nous sachions, aucune dÃ©marche de preuve formelle automatique 
+de convergence n'a jamais Ã©tÃ© Ã©tablie. 
+Dans le travail thÃ©orique~\cite{Cha06}, Chandrasekaran a montrÃ© que les itÃ©rations asynchrones sont convergentes 
+si et seulement si on peut construire une fonction de Lyaponov dÃ©croissante, mais il ne donne pas de mÃ©thode 
+automatique pour construire cette fonction.
+
+\JFC{DÃ©placer ceci dans les perspective}
 Among drawbacks of the method,  one can argue that bounded delays is only 
 realistic in practice for close systems. 
 However, in real large scale distributed systems where bandwidth is weak, 
 this restriction is too strong. In that case, one should only consider that 
-matrix $S^{t}$ follows the  iterations of the system, \textit{i.e.},
+matrix $s^{t}$ follows the  iterations of the system, \textit{i.e.},
 for all $i$, $j$, $1 \le i \le j \le n$,  we have$
-\lim\limits_{t \to \infty} S_{ij}^t = + \infty$. 
+\lim\limits_{t \to \infty} s_{ij}^t = + \infty$. 
 One challenge of this work should consist in weakening this constraint. 
 We plan as future work to take into account other automatic approaches 
 to discharge proofs notably by deductive analysis~\cite{CGK05}. 
