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

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