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

diff --git a/modelchecking.tex b/modelchecking.tex
index 936835b..dd804c2 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,4 +1,4 @@
-
+\JFC{donner dans les rappels les délais et les propriétés de convergence uniforme}
 
 
 \section{Rappels sur le langage PROMELA}
@@ -27,7 +27,7 @@ chan unlock_elements_update=[1] of {bool};
 chan sync_mutex=[1] of {bool};
 \end{lstlisting}
 \end{scriptsize}
-\caption{Type declaration of the DDNs translation.}
+\caption{Declaration des types de la traduction.}
 \label{fig:arrayofchannels}
 \end{figure}
 
@@ -165,7 +165,7 @@ init{
 }
 \end{lstlisting}
 \end{scriptsize}
-\caption{PROMELA init process.}\label{fig:spin:init} 
+\caption{Process init.}\label{fig:spin:init} 
 \end{minipage}\hfill
  \begin{minipage}[h]{.42\linewidth}
 \begin{scriptsize}
@@ -190,7 +190,7 @@ active proctype scheduler(){
 }
 \end{lstlisting}
 \end{scriptsize}
-\caption{Scheduler process for common pseudo-periodic strategy.
+\caption{Process scheduler pour la stratégie pseudo-periodique.
  \label{fig:scheduler}}
 \end{minipage}
 \end{figure}
@@ -219,29 +219,29 @@ Dans la séquence d'éxécution, le choix d'un élément mis à jour est directe
 suivi par des mis àjour: ceci est réalisé grace à la modification de la valeur du sémaphore
  \verb+unlock_elements_updates+.
 
-\subsection{Applying the function $F$}\label{sub:spin:update}
-Updating a set $S^t=\{s_1,\ldots, s_m\}$  of elements that occur in the strategy
-$(S^t)^{t \in \Nats}$ is implemented by the \verb+update_elems+ process given
-in~\ref{fig:proc}.  This  active  process waits  until  it is  unlocked by  the
-\verb+scheduler+  process through  the  semaphore \verb+unlock_elements_update+.
-The implementation is then fivefold:
+\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 
+{\sc Figure}~\ref{fig:proc}.  
+Ce process actif attend jusqu'à ce qu'il soit déblocqué par le process
+\verb+scheduler+  à l'aide du sémaphore \verb+unlock_elements_update+.
+L'implantation contient donc cinq étapes:
 
 \begin{enumerate}
-\item it starts with updating the variable \texttt{X} with the values of \texttt{Xp}
-  thanks to the \texttt{update\_X} function (not detailed here);
-  %%we recall that the variable \texttt{X} is only defined as 
-\item it stores in \texttt{Xd} the current available values of the elements thanks
-  to the function \texttt{fetch\_values} (see \Sec{sub:spin:vt});
-\item  a loop  over the  number \texttt{ar\_len}  of elements  that have  to evolve
-  iteratively updates the  value of $j$ (through the  function call \texttt{F(j)})
-  provided   this  has   to   evolve,  \textit{i.e.},   it   is  referenced   by
-  \texttt{mods[count]}; source code  of \texttt{F} is given in~\ref{fig:p} and is a
-  direct translation of the map $F$;
-\item the new components values in  \texttt{Xp} are symbolically sent to the other
-  components requiring them % for future access
-  thanks to the \texttt{diffuse\_values(Xp)} function (see \Sec{sub:spin:vt});
-\item finally, this process informs the scheduler about the end of the task 
-  (through the semaphore \texttt{sync\_mutex}).
+\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}
 
 
@@ -274,7 +274,7 @@ active proctype update_elems(){
 }
 \end{lstlisting}
 \end{scriptsize}
-\caption{Updatings of the elements.}\label{fig:proc}
+\caption{Mise à jour des éléments.}\label{fig:proc}
   \end{minipage}\hfill%
 %\end{figure}
 %\begin{figure}
@@ -294,40 +294,17 @@ inline F(){
 }
 \end{lstlisting}
 \end{scriptsize}
-\caption{Application of  function $F$.}\label{fig:p}
+\caption{Application de la fonction $F$.}\label{fig:p}
   \end{minipage}
 \end{figure}
 
-% \subsection{Modifying  Values of one  Element}
-
-% Each element $i$ may modify its value through the coresponding 
-% active process \verb+pi+. 
-% In Fig.~\ref{fig:p4} that gives the translation of 
-% modifying the element $4$, the process is waiting until it is unlocked
-% and then it computes the new value of $X_4$, represented by $X'_4$ 
-% and memorized as \verb+Xp[4]+. 
-
-
-% \begin{ProofCr}
-
-% First of all, the second hypothesis of the previous proof is established.
-
-% In this part, we prove that for any time $t$,  
- 
-% The proof is achieved under the hypothesis that at current time $t$, 
-
-% For $j$ in $J^t$, variables 
-% \verb+v0+, \ldots \verb+vn-1+ are respectively 
-% $X_0^{S_{j0}^t},\ldots, X_{n-1}^{S_{jn-1}^t}$.
-% Since \verb+F+ is the direct translation of $F$, rest of the proof is obvious. 
- 
-  
-% \end{ProofCr}
 
-\subsection{Delays Handling}\label{sub:spin:vt}
-This  section shows  how  delays are  translated  into PROMELA  through the  two
-functions   \verb+fetch_values+  and   \verb+diffuse_values+,   given  in~\ref{fig:val} and~\ref{fig:broadcast}, that  respectively store and transmit the
-element values.
+\subsection{Gestion des délais}\label{sub:spin:vt}
+Cette  section montre comment les délais iné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}, 
+qui récupèrent et diffusent respectivement les valeurs des elements.
 
 \begin{figure}[t]
   \begin{minipage}[h]{.475\linewidth}
@@ -361,7 +338,7 @@ inline fetch_values(){
 }
 \end{lstlisting}
 \end{scriptsize}
-\caption{Fetching of the elements values\label{fig:val}}
+\caption{Récupérer les valeurs des elements\label{fig:val}}
   \end{minipage}\hfill%
   \begin{minipage}[h]{.475\linewidth}
 \begin{scriptsize}
@@ -392,76 +369,75 @@ inline diffuse_values(values){
 }	
 \end{lstlisting}
 \end{scriptsize}
-\caption{Diffusion of the elements values}\label{fig:broadcast}
+\caption{Diffuser les valeurs des elements}\label{fig:broadcast}
   \end{minipage}
 \end{figure}
 
-The former potentially updates the  array \verb+Xd+ needed by elements that have
-to be  modified.  For  each element in  \verb+mods+, identified by  the variable
-$j$, the  function retrieves the values  of the other elements  (labeled by $i$)
-whose $j$ depends on.  There are two cases:
+La première fonction met à jour le tableau array \verb+Xd+ recquis 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}
+Il y a deux cas.
 \begin{itemize}
-\item since $i$  knows its last value (\textit{i.e.},  $D^t_{ii}$ is always $t$)
-  \verb+Xd[i].v[i]+ is then \verb+Xp[i]+.
-\item otherwise, there are two sub-cases which potentially update the value that
-  $j$ knows about $i$ (that may be chosen in a random way):
+\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):
   \begin{itemize}
-  \item  from the viewpoint of $j$  the value  of  $i$ may  not change  (the
-    \verb+skip+  statement) or  is not  relevant; this  latter case  arises when
-    there is no edge from $i$ to $j$ in the incidence graph, \textit{i.e.}, when
-    the value  of \verb+is_succ+ that  is computed by \verb+hasnext(i,j)+  is 0;
-    then the value of \verb+Xd[j].v[i]+ is not modified;
-  \item otherwise,  \verb+Xd[j].v[i]+ is assigned  with the value stored  in the
-    channel  \verb+channels[i].sent[j]+  (provided   this  one  is  not  empty).
-    Element  values  are  added  into  this channel  during  the  \verb+diffuse_values+
-    function as follows.
+  \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;
+    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.
   \end{itemize}
 \end{itemize}
 
-The \verb+diffuse_values+  function aims  at storing the  values of $X$  represented by
-\verb+Xp+ in the  \verb+channels+.  It allows the SPIN  model-checker to execute
-the PROMELA model as if it allowed delays between processes.
-% as if computation mode were asynchronous. 
-%For that reason, when an iteration has to synchronize the elements $i$ and 
-%$j$  (\textit{i.e.} when \verb+sync[j] == sync[i]+ is true), 
-% no delay emulation is performed.
-%In the asynchronous mode, 
-There are two cases concerning the value of $X_{j}$:
+L'objectif de la fonction \verb+diffuse_values+  est de stocker les valeurs de $X$  représenté
+dans le modèle par \verb+Xp+ dans le cannal  \verb+channels+.
+Il permet au modèle-checker SPIN  d'exécuter 
+le modèle PROMELA model comme s'il pouvait y avoir des délais entre processus
+Il y a deux cas différents pour la valeur de $X_{j}$:
 \begin{itemize}
-\item either it is left out to allow $i$ not to take into account all the values
-  of  $j$; this case  occurs either  through the  \verb+skip+ statement  or when
-  there is no edge from $j$ to $i$ in the incidence graph;
-\item or it is stored  in the channel \verb+channels[j].sent[i]+ (provided it is
-  not full).
+\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).
 \end{itemize}
 
-Introducing     non-determinism      both     in     \verb+fetch_values+     and
-\verb+diffuse_values+   functions  is   necessary  in   our  context.    If  the
-non-determinism would be used only  in \verb+fetch_values+, then it would not be
-possible  for instance  to retrieve  the value  $X_i^{(t)}$ without  taking into
-account the value  $X_i^{(t-1)}$.  On the other hand,  if the non-determinism is
-only used  in \verb+diffuse_values+, then each  time a value is  pushed into the
-channel, this  value is  immediately consumed, which  contradicts the  notion of
-delays.
-
-\subsection{Discussion}
-A  coarse approach  could consist  in providing  one process  for  each element.
-However, the  distance with  the mathematical model  given in  \Equ{eq:async} of
-such a translation would be larger  than the method presented along these lines.
-It induces  that it would be harder  to prove the soundness  and completeness of
-such a translation.   For that reason we have developed a  PROMELA model that is
-as close as possible to the mathematical one.
-
-Notice furthermore that PROMELA is an  imperative language which
-often results in generating  intermediate  states 
-(to  execute  a matrix assignment  for
-instance). 
-The  use  of  the  \verb+atomic+  keyword  allows  the  grouping  of
-instructions, making the PROMELA code and the DDN as closed as possible.
-
-\subsection{Universal Convergence Property}
-We are left to show how to formalize into the SPIN model-checker that iterations
-of a DDN with $n$ elements are universally convergent.  We first recall that the
+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
+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 
+délai.
+
+% \subsection{Discussion}
+% A  coarse approach  could consist  in providing  one process  for  each element.
+% However, the  distance with  the mathematical model  given in  \Equ{eq:async} of
+% such a translation would be larger  than the method presented along these lines.
+% It induces  that it would be harder  to prove the soundness  and completeness of
+% such a translation.   For that reason we have developed a  PROMELA model that is
+% as close as possible to the mathematical one.
+
+% Notice furthermore that PROMELA is an  imperative language which
+% often results in generating  intermediate  states 
+% (to  execute  a matrix assignment  for
+% instance). 
+% 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 
+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