X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/251b65007a909068d3344bd82b7c5ec0ffb0a21a..322d0e3286e2bc9cae4178aa7488b5631c57a8ba:/modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index f69df76..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}
@@ -32,49 +140,52 @@ chan sync_mutex=[1] of {bool};
 \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 dÃ©clarer 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 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Ã¨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;
+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$;
+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Ã©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.
+% 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 canal.
+% 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 canal \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 canaux  \verb+unlock_elements_update+ et  \verb+sync_mutex+ contenant 
 chacun un message boolÃ©en et utilisÃ© ensuite comme des sÃ©maphores.
@@ -83,8 +194,8 @@ chacun un message boolÃ©en et utilisÃ© ensuite comme des sÃ©maphores.
 
 %\subsection{PROMELA Processes} 
 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 
+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 
@@ -92,13 +203,13 @@ d'initialiser les variables, lancer d'autres process\ldots
 
 
 Les instructions d'affectation sont interprÃ©tÃ©es usuellement.
-Les canaux sont cernÃ©s par des instructions particuliÃ¨res d'envoi et de
+Les canaux sont concernÃ©s par des instructions particuliÃ¨res d'envoi et de
 rÃ©ception de messages. Pour un canal  
-\verb+ch+,  ces instruction sont respectivement notÃ©es
-\verb+ch  !  m+ et \verb+ch  ?  m+.
+\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 rÃ©ception ou bien rempli pour un envoi,
 le processus est bloquÃ© jusqu'Ã  ce que les  conditions soient  remplies.
@@ -111,18 +222,17 @@ 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 vÃ©rifier si les itÃ©rations sont  convergentes pour n'importe  
-quelle configuration initiale $X^{(0)}$.
+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}
+  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. 
@@ -130,7 +240,7 @@ puisque la matrice $S^0$ est Ã©gale Ã  $(0)$,
 \end{itemize}
 
 \begin{figure}[t]
- \begin{minipage}[h]{.52\linewidth}
+  \begin{minipage}[h]{.32\linewidth}
 \begin{tiny}
 \begin{lstlisting}
 init{
@@ -167,7 +277,7 @@ init{
 \end{tiny}
 \caption{Process init.}\label{fig:spin:init} 
 \end{minipage}\hfill
- \begin{minipage}[h]{.42\linewidth}
+ \begin{minipage}[h]{.32\linewidth}
 \begin{tiny}
 \begin{lstlisting}
 active proctype scheduler(){ 
@@ -190,9 +300,31 @@ active proctype scheduler(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©rodique.
+\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}
 
 
@@ -208,7 +340,7 @@ 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.
 Intuitivement, un process \verb+scheduler+ (comme reprÃ©sentÃ© Ã  la {\sc Figure}~\ref{fig:scheduler}) 
-est iterrativement 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
@@ -216,37 +348,36 @@ Basiquement, le process est une boucle qui est dÃ©bloquÃ©e lorsque la valeur du
 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'exÃ©cution, le choix d'un Ã©lÃ©ment mis Ã  jour est directement
-suivi par des mis Ã  jour: ceci est rÃ©alisÃ© grÃ¢ce Ã  la modification de la valeur du sÃ©maphore
+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Ã©bloquÃ© 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 fonction \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 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)} (cf. \Sec{sub:spin:vt});
-\item finalement, le process informe le scheduler de la fin de la tÃ¢che 
-  (au travers  du sÃ©maphore \texttt{sync\_mutex}).
-\end{enumerate}
-
+L'implantation se dÃ©roule en cinq Ã©tapes:
 
 \begin{figure}[t]
-  \begin{minipage}[h]{.475\linewidth}
+\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(){
@@ -278,7 +409,7 @@ active proctype update_elems(){
   \end{minipage}\hfill%
 %\end{figure}
 %\begin{figure}
-  \begin{minipage}[h]{.45\linewidth}
+  \begin{minipage}[b]{.33\linewidth}
 \begin{tiny}
 \begin{lstlisting}
 inline F(){
@@ -294,11 +425,35 @@ inline F(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Application de la fonction $F$.}\label{fig:p}
+\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 inhÃ©rents au mode asynchrone sont 
 traduits dans le modÃ¨le  PROMELA  grÃ¢ce Ã  deux 
@@ -377,7 +532,7 @@ La premiÃ¨re fonction met Ã  jour le tableau   \verb+Xd+ requis pour les Ã©lÃ©me
 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 libellÃ© est $i$)
-dont $j$ dÃ©pend. \JFC{vÃ©rifier si c'est ce sens ici}
+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$)
@@ -388,18 +543,17 @@ Il y a deux cas.
   \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'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)+  is 0;
+    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
     dans le canal \verb+channels[i].sent[j]+  (pour peu que celui-ci ne soit pas vide).
-    Les valeurs des Ã©lÃ©ments sont ajoutÃ©es dans ce canal au travers de la fonction  \verb+diffuse_values+
-    donnÃ©e juste aprÃ¨s.
   \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 canal  \verb+channels+.
-Il permet au modÃ¨le-checker SPIN  d'exÃ©cuter 
+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}
@@ -412,10 +566,10 @@ n'y a pas d'arc de $j$ Ã  $i$ dans le graphe d'incidence;
 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)}$.  
+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 canal, 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}
@@ -434,11 +588,12 @@ dÃ©lai.
 % instructions, making the PROMELA code and the DDN as closed as possible.
 
 \subsection{PropriÃ©tÃ© de convergence universelle}
-Il reste Ã  formaliser dans le model checker SPIN que les itÃ©rations d'un systÃ¨me 
+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.
 
 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. 
+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
@@ -447,37 +602,46 @@ de prouver la formule temporelle linÃ©aire (LTL) suivante:
 \diamond  (\Box  \verb+Xp+ = \verb+X+)
 \label{eq:ltl:conv}
 \end{equation}
-oÃ¹ les opÃ©rateur  $\diamond$ et  $\Box$ on la sÃ©mantique usuelle \textit{i.e.}, Ã  savoir
+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Ã© assure seulement la stabilisation du systÃ¨me, 
-mais ne donne aucune mÃ©trique quant Ã  la maniÃ¨re dont celle-ci est obtenue.
+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.
-vers plusieurs 
+
 
 
 \section{Correction et complÃ©tude de la dÃ©marche}\label{sec:spin:proof}
 
-Cette section prÃ©sente les thÃ©orÃ¨me de correction et de  complÃ©tude de l'approche.
+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}[Correction]\label{Theo:sound}
+\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{theorem}
-
+\end{restatable}
 
 
-\begin{theorem}[ComplÃ©tude]\label{Theo:completeness}
+\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{theorem}
+\end{restatable}
+
+
 
 
 
@@ -488,12 +652,13 @@ 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$ arc dans le graphe d'incidence
+  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\times(\delta_0+1)+n(n+2)}$.
+  de l'exÃ©cution en SPIN de $\psi$ est bornÃ©e par $2^{m(\delta_0+1)+n(n+2)}$.
 \end{theorem}
 \begin{Proof}
-  Une configuration est une valuation des variables globales.
+  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.
@@ -502,37 +667,41 @@ puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
   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\times(\delta_0+1)}$ Ã©tats. 
-  Le nombre de configurations est donc bornÃ© par $2^{m\times(\delta_0+1)+n(n+2)}$.
+  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}
+  %\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 uniforme.
+La mÃ©thode dÃ©taillÃ©e ici a pu Ãªtre appliquÃ©e sur l'exemple
+pour prouver formellement sa convergence universelle.
 
 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 $l1$, \ldots $lk$:  
+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)))
 $$
 
-oÃ¹ le libellÃ© $l0$ dÃ©note le libellÃ© de la ligne prÃ©cÃ©dent le choix indÃ©terministe.
+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 uniforme 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 les non Ã©quitables, puis en le laissant vÃ©rifier la propriÃ©tÃ© de convergence dessus. 
+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.
@@ -551,106 +720,124 @@ Dans le cas contraire on doit analyser le contre exemple produit par SPIN.
 
 
 La mÃ©thode dÃ©taillÃ©e ici a Ã©tÃ© appliquÃ©e sur des exemples pour prouver formellement 
-leur convergence ou leur divergence (Fig.~\ref{fig:async:exp}).
-Dans ces expÃ©riences, les dÃ©lais on Ã©tÃ© bornÃ©s par $\delta_0=10$.
-Dans ce tableau,  $P$ est vrai ($\top$) si et seulement si la convergence uniforme 
-est Ã©tablie et faux ($\bot$) sinon. Le nombre $M$ et la taille de la  mÃ©moire consommÃ©e (en MB) et 
+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.
 
-L'exemple RE est l'exemple jouet de ce chapitre,
-AC2D est un automate cellulaire  avec 9 elements prenant des valeurs boolÃ©ennes en fonction de 
-de 4 voisins et BM99, issu de~\cite{BM99} consiste en  10 process
-qui modifient leur valeur boolÃ©ennes dans un graphe d'adjacence proche du graphe complet.
-
 
-\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}
-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{ExpÃ©rimentations avec des itÃ©rations asynchrones}\label{fig:async:exp}
+\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~\cite{RC07} concerne un rÃ©seau composÃ© de deux gÃ¨nes Ã  valeur dans $\{0,1,2\}$. 
-Comme la convergence n'est dÃ©jÃ  pas Ã©tablie pour les itÃ©rations parallÃ¨les, il en est donc 
+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 
+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)$.
-   
-  
-Dans l'exemple issu de~\cite{BM99}, nous avons 10 process
-Ã  valeur boolÃ©ennes. En raison de la dÃ©pendance forte entre les Ã©lÃ©ments, 
+$\{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 uniforme.
+lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence universelle.
 
 \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} exemples &
-$\bot$ & 2.5 & 0.001s & % RC07_sync.spin
-$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
-\hline
-\cite{BM99} exemple &
-$\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} 
+\centering
+\includegraphics[scale=0.6]{images/RC07ce.eps}   
+\caption{Contre exemple de convergence pour~\ref{fig:RC07CE}} \label{fig:RC07CE}
+\end{figure}
+
 
 
 
@@ -680,27 +867,7 @@ $\top$ &  &  \\ % BM99_sync_chao.spin
  
 \section{Conclusion}
 \label{sec:spin:concl}
-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 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.},
-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}. 
 
 
 
