X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/251b65007a909068d3344bd82b7c5ec0ffb0a21a..5307c38b9fdbec499a398c994ee36eb2ac51b2fb:/modelchecking.tex?ds=sidebyside

diff --git a/modelchecking.tex b/modelchecking.tex
index f69df76..1b8843d 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,4 +1,64 @@
-\JFC{donner dans les rappels les dÃ©lais et les propriÃ©tÃ©s de convergence uniforme}
+\JFC{donner dans les rappels les dÃ©lais et les propriÃ©tÃ©s de convergence universelle}
+
+\JFC{Statuer sur la taille des exemples traitables par la dÃ©marche, cf donnÃ©es pratiques}
+
+\section{Exemple jouet}
+
+\begin{xpl}
+  On considÃ¨re dans ce chapitre l'exemple oÃ¹ trois Ã©lÃ©ments dans $\Bool$. 
+  Chaque configuration est ainsi un Ã©lement de $\{0,1\}^3$, \textit{i.e.}, 
+  un nombre entre 0 et 7. 
+  La \Fig{fig:map} prÃ©cise la fonction $f$ considÃ©rÃ©e et 
+  la \Fig{fig:xplgraph} donne son graphe d'intÃ©raction.
+  
+\begin{figure}[ht]
+  \centering
+  \begin{minipage}%[h]
+    {.6\linewidth}
+    \begin{center}
+      $ F(x)= \left \{
+        \begin{array}{rcl}
+          f_1(x_1,x_2,x_3) & = & x_1.\overline{x_2} + x_3  \\
+          f_2(x_1,x_2,x_3) & = & x_1 + \overline{x_3} \\
+          f_3(x_1,x_2,x_3) & = & x_2.x_3
+        \end{array}
+      \right.
+      $        
+    \end{center}
+    \caption{Fonction Ã  itÃ©rer}    \label{fig:map}
+  \end{minipage}
+  \begin{minipage}%[h]
+    {.35\linewidth}
+    \begin{center}
+      \includegraphics[width=4cm]{images/xplCnxMc.eps}
+    \end{center}
+    \caption{Graphe d'intÃ©raction}
+    \label{fig:xplgraph}
+    \end{minipage}
+  \caption{Exemple pour SDD $\approx$ SPIN.}
+\end{figure}
+
+
+
+
+
+
+On peut facilement vÃ©rifier que toutes les itÃ©rations parallÃ¨les initialisÃ©es 
+avec $x^0 \neq 7$ soit $(111)$ 
+convergent vers $2$ soit $(010)$; celles initialisÃ©es avec 
+$x^0=7$ restent en 7.
+Pour les autres modes synchrones avec  une 
+stratÃ©gie pseudo pÃ©riodique, les comportements selon la configuration initiale:
+\begin{itemize}
+\item initialisÃ©e avec 7, les itÃ©rations restent en 7;
+\item initialisÃ©e avec 0, 2, 4 ou 6 les itÃ©rations convergent vers 2;
+\item initialisÃ©es avec 1, 3 ou 5, les itÃ©rations convergent vers un des 
+deux points fixes 2 ou 7.
+\end{itemize}   
+\end{xpl}
+
+
+
 
 
 \section{Rappels sur le langage PROMELA}
@@ -37,7 +97,7 @@ Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
 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 
@@ -47,23 +107,23 @@ Il dÃ©finit tout d'abord:
 \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}$
+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;
+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: 
+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 
@@ -74,7 +134,7 @@ 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
  \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.
@@ -92,13 +152,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 +171,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 +189,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 +226,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(){ 
@@ -193,6 +252,28 @@ active proctype scheduler(){
 \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}
 
 
@@ -208,7 +289,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 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
@@ -216,37 +297,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
 \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 +358,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 +374,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 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 inhÃ©rents au mode asynchrone sont 
 traduits dans le modÃ¨le  PROMELA  grÃ¢ce Ã  deux 
@@ -377,7 +481,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,17 +492,16 @@ 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+.
+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   comme s'il pouvait y avoir des dÃ©lais entre processus
 Il y a deux cas diffÃ©rents pour la valeur de $X_{j}$:
@@ -411,11 +514,11 @@ 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)}$.  
+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 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 +537,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 +551,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,9 +601,10 @@ 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.
@@ -502,8 +616,8 @@ 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}
@@ -511,28 +625,32 @@ puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
 \end{Proof}
 
 La mÃ©thode dÃ©taillÃ©e ici a pu Ãªtre appliquÃ©e sur l'exemple jouet
-pour prouver formellement sa convergence uniforme.
+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 
+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 les non Ã©quitables, puis en le laissant vÃ©rifier la propriÃ©tÃ© de convergence dessus. 
+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,17 +669,46 @@ 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: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.
 
-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}
+\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}
@@ -582,7 +729,7 @@ P & M & T &
 P & M & T&
 P & M & T \\
 \hline %cline{2-13}
-Running Example & 
+\textit{RE} & 
 $\top$ & 409 & 1m11s&
 $\bot$ & 370 & 0.54 &
 $\bot$ & 374 & 7.7s&
@@ -594,7 +741,7 @@ AC2D
 &$\bot$ & 2.5 & 0.01s   % RC07_async.spin
 &$\bot$ & 2.5 & 0.01s  \\ % RC07_async_all.spin 
 \hline %\cline{2-13}
-BM99 
+\cite{BM99}
 &$\top$ &  &   %BM99_mixed_para.spin 
 &$\top$ &  &    % RC07_async_mixed_all.spin
 &$\bot$ &  &    % RC07_async.spin
@@ -607,50 +754,40 @@ BM99
 
 
 
-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 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 
+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}
+
 
 
 
@@ -685,7 +822,8 @@ 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. 
+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.
@@ -695,9 +833,9 @@ 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}. 
