X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/e3c2188521eaa2c6e2c6eee2da43b0f42fc47a89..fd3c8d84472bbc887a48fc8e441bd3fafedf96a7:/modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index dd804c2..1919416 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,4 +1,112 @@
-\JFC{donner dans les rappels les dÃ©lais et les propriÃ©tÃ©s de convergence uniforme}
+
+
+
+L'Ã©tude de convergence de systÃ¨mes dynamiques discrets est simple Ã  vÃ©rifier 
+pratiquement pour le mode synchrone. Lorsqu'on introduit des stratÃ©gies 
+pseudo pÃ©riodiques pour les modes unaires et gÃ©nÃ©ralisÃ©es, le problÃ¨me 
+se complexifie. C'est pire encore lorsqu'on traite des itÃ©rations asynchrones 
+et mixes prenant de plus en compte les dÃ©lais. 
+
+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.
+
+Un outil qui construirait automatiquement toutes 
+les transitons serait le bienvenu. 
+Pour peu qu'on Ã©tablisse la preuve de correction et de complÃ©tude de la 
+dÃ©marche, la convergence du rÃ©seau discret ne repose alors que sur le verdict 
+donnÃ© par l'outil. 
+Cependant, mÃªme pour des rÃ©seaux discrets Ã  peu d'Ã©lÃ©ments, 
+le nombre de configurations induites explose rapidement.
+Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}  
+sont des classes d'outils qui adressent le problÃ¨me de vÃ©rifier automatiquement
+qu'un modÃ¨le vÃ©rifie une propriÃ©tÃ© donnÃ©e. Pour traiter le problÃ¨me d'explosion 
+combinatoire, ces outils appliquent des mÃ©thodes d'ordre partiel, d'abstraction,
+de quotientage selon une relation d'Ã©quivalence.
+
+Ce chapitre montre comment nous simulons 
+des rÃ©seaux discrets selon toutes les sortes d'itÃ©rations pour Ã©tablir 
+formellement leur convergence (ou pas).
+Nous dÃ©butons par un exemple et faisons quelques rappels sur 
+le langage PROMELA qui est le langage du model-checker 
+SPIN~\cite{Hol03} (\Sec{sec:spin:promela}).
+Nous prÃ©sentons ensuite la dÃ©marche de traduction 
+de rÃ©seaux discrets dans PROMELA (\Sec{sec:spin:translation}).   
+Les thÃ©orÃ¨mes de correction et de complÃ©tude de la dÃ©marche
+sont ensuite donnÃ©s Ã  la (\Sec{sec:spin:proof}). 
+Des donnÃ©es pratiques comme la complexitÃ© et des synthÃ¨ses d'expÃ©rimentation
+sont ensuite fournies (\Sec{sec:spin:practical}). 
+
+
+
+
+
+
+
+%\section{Exemple jouet}
+
+
+\begin{figure}[ht]
+  \begin{center}
+    \subfigure[Fonction Ã  itÃ©rer]{
+      $ 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.
+      $        
+      \label{fig:map}
+    }
+    \hfill
+    \subfigure[Graphe d'intÃ©raction]{
+      \includegraphics[width=4cm]{images/xplCnxMc.eps}
+      \label{fig:xplgraph:inter:mc}
+    }
+  \end{center}
+  \caption{Exemple pour SDD $\approx$ SPIN.}
+\end{figure}
+
+
+
+\begin{xpl}
+  On considÃ¨re un exemple Ã  trois Ã©lÃ©ments dans $\Bool$. 
+  Chaque configuration est ainsi un Ã©lÃ©ment de $\Bool^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:inter:mc} donne son graphe d'intÃ©raction.
+  
+
+
+
+
+
+
+On peut facilement vÃ©rifier que toutes les itÃ©rations synchrones 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  mode unaires ou gÃ©nÃ©ralisÃ©s  avec  une 
+stratÃ©gie pseudo pÃ©riodique, on a des comportements qui dÃ©pendent 
+de 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 +119,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,82 +134,85 @@ 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}
 
 
-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 
+% Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
+% \texttt{short} et  \texttt{int}.
+Comme en C,
+on peut dÃ©clarer des tableaux Ã  une dimension 
 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.
+\verb+typedef+). % Ces derniers sont utilisÃ©s
+% pour dÃ©finir des tableaux Ã  deux
+% 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:
+dÃ©clarations de variables qui servent dans l'exemple de ce chapitre. 
+Il dÃ©finit:
 \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;
+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 
-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.
+% 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 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 
+DÃ©clarÃ©e avec le mot clef \verb+chan+, 
+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.
+% Elles serait  suivi par sa capacitÃ© 
+% (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  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 +221,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 +274,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 +299,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Ã©riodique.
  \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 +338,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 itÃ©rativement 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 processus 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 +404,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 +424,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 itÃ©rativement 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 +463,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 +492,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 +523,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+.
-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
+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 model-checker SPIN  d'exÃ©cuter 
+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
+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 +587,264 @@ 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}
+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.
 
-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.
+\section{Correction et complÃ©tude de la dÃ©marche}\label{sec:spin: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}.
 
-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.
 
+\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}
 
 
-\paragraph{Inductive case:}
+\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}
 
-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}
-
-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}
-
-\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}
-
-
-\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{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{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
+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:exp:promela}) 
+avec ou sans dÃ©lais.
+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}[ht]
+  \begin{center}
+    \begin{tiny}
+      \subfigure[Sans dÃ©lais]{
+        \begin{tabular}{|*{7}{c|}}
+          \cline{2-7}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{GÃ©nÃ©ralisÃ©es} \\
+          \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}
+        \label{fig:sync:exp}  
+      }
+    
+      \subfigure[Avec dÃ©lais]{
+        \begin{tabular}{|*{13}{c|}}
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{6}{|c|}{Mode Mixe} & \multicolumn{6}{|c|}{Seulement bornÃ©} \\
+          \cline{2-13}
+          \multicolumn{1}{c|}{ }
+          &\multicolumn{3}{|c|}{Synchrones} & \multicolumn{3}{|c|}{Pseudo-PÃ©riodique} &
+          \multicolumn{3}{|c|} {Synchrones} & \multicolumn{3}{|c|}{Pseudo-PÃ©riodique} \\
+          \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}
+        \label{fig:async:exp}
+      }
+    \end{tiny}
+  \end{center}
+  \caption{RÃ©sultats des simulations Promela des SDDs}\label{fig:exp:promela}
+\end{figure} 
+
+
+
+L'exemple \textit{RE} est l'exemple 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 leurs valeurs boolÃ©ennes dans un graphe d'adjacence proche 
+du graphe complet.
+
+
+L'exemple  \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 synchrones
+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,45 +862,12 @@ 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.
-
-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.},
-for all $i$, $j$, $1 \le i \le j \le n$,  we have$
-\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}. 
+
 
 
 
