une version de plus

[hdrcouchot.git] / annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 881383ca188b158e5c0fb60ed4632bb4ecc7f10c..3c0724c17412fe07decaf21881f004a1acb6ab69 100644 (file)
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -6,18 +6,18 @@ du chapitre~\ref{chap:promela}.
 
 \begin{lemma}[Stratégie équivalente]\label{lemma:strategy}
   Soit $\phi$  un système dynamique discret de stratégie  $(S^t)^{t \in  \Nats}$ 
 
 \begin{lemma}[Stratégie équivalente]\label{lemma:strategy}
   Soit $\phi$  un système dynamique discret de stratégie  $(S^t)^{t \in  \Nats}$ 

-  et $\psi$  sa traduction en promela. 
+  et $\psi$  sa traduction en PROMELA. 

   Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle 
   Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle 

-  le le scheduler met à jour les  elements of $S^t$
-  donnés par \verb+update_elems+ à l'iteration $t$.
+  le scheduler met à jour les  éléments of $S^t$
+  donnés par \verb+update_elems+ à l'itération $t$.

 \end{lemma}
 \end{lemma}

-\begin{Proof}
+\begin{proof}

   La preuve est directe pour $t=0$.
   La preuve est directe pour $t=0$.

-  Supposons qu'elle est établie jusqu'en $t$ vallant un certain $t_0$. 
-  On considère des stratégies pseudo périodiques.
+  Supposons qu'elle est établie jusqu'en $t$ valant un certain $t_0$. 
+  On considère des stratégies pseudo-périodiques.

   Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie 
   Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie 

-  les éléments de $S^t$ à l'iteration $t$.
-\end{Proof}
+  les éléments de $S^t$ à l'itération $t$.
+\end{proof}

 
 Dans ce qui suit, soit     $Xd^t_{ji}$     la valeur de 
 \verb+Xd[+$j$\verb+].v[+$i$\verb+]+  après le   $t^{\text{ème}}$ appel 
 
 Dans ce qui suit, soit     $Xd^t_{ji}$     la valeur de 
 \verb+Xd[+$j$\verb+].v[+$i$\verb+]+  après le   $t^{\text{ème}}$ appel 


@@ -33,7 +33,7 @@ $k$, $0 \le k \le  m-1$, le tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ en entrant
 dans la fonction \verb+update_elems+ à l'itération $t$ où
 % \begin{itemize}
 % \item
 dans la fonction \verb+update_elems+ à l'itération $t$ où
 % \begin{itemize}
 % \item

- $Y^k_{ij}$ est la valeur du cannal \verb+channels[i].sent[j]+
+ $Y^k_{ij}$ est la valeur du canal \verb+channels[i].sent[j]+

   à l'indice $k$,
 %\item 
 $a^k_{ij}$ est la  date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et 
   à l'indice $k$,
 %\item 
 $a^k_{ij}$ est la  date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et 


@@ -50,8 +50,8 @@ M_{ij}^t: &
 \end{array}  
 \end{equation*}
 
 \end{array}  
 \end{equation*}
 

-Intuitivement,  $M_{ij}^t$  est la mémoire du cannal
-\verb+channels[i].sent[j]+ à l'iterations $t$. 
+Intuitivement,  $M_{ij}^t$  est la mémoire du canal
+\verb+channels[i].sent[j]+ à l'itération $t$. 

 On note que le domaine de chaque $M_{ij}^1$ est $\{0\}$ et
 $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    en effet le processus 
 \verb+init+  initialise \verb+channels[i].sent[j]+ avec \verb+Xp[i]+.
 On note que le domaine de chaque $M_{ij}^1$ est $\{0\}$ et
 $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    en effet le processus 
 \verb+init+  initialise \verb+channels[i].sent[j]+ avec \verb+Xp[i]+.


@@ -59,8 +59,8 @@ $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$:    en effet le processus
 Montrons comment l'indéterminisme des deux fonctions 
 \verb+fetch_values+ et  \verb+diffuse_values+  
 permet de modéliser l'équation  \Equ{eq:async}.
 Montrons comment l'indéterminisme des deux fonctions 
 \verb+fetch_values+ et  \verb+diffuse_values+  
 permet de modéliser l'équation  \Equ{eq:async}.

-La  function   $M_{ij}^{t+1}$  est  obtenue à l'aide de mises à jour successives
-de  $M_{ij}^{t}$  au travers des deux   functions   \verb+fetch_values+  and
+La  fonction   $M_{ij}^{t+1}$  est  obtenue à l'aide de mises à jour successives
+de  $M_{ij}^{t}$  au travers des deux   fonctions   \verb+fetch_values+  and

 \verb+diffuse_values+.   Par abus,   soit  $M_{ij}^{t+1/2}$  
 la valeur de  $M_{ij}^{t}$ après la première fonction pendant l'itération
  $t$.
 \verb+diffuse_values+.   Par abus,   soit  $M_{ij}^{t+1/2}$  
 la valeur de  $M_{ij}^{t}$ après la première fonction pendant l'itération
  $t$.


@@ -82,8 +82,8 @@ M_{ij}^{t}$.
 Dans la fonction \verb+diffuse_values+, 
 s'il existe un $\tau$, $\tau\ge t$
 tel que \mbox{$D^{\tau}_{ji} = t$}, soit alors   $c_{ij}$ défini par $ \min\{l \mid
 Dans la fonction \verb+diffuse_values+, 
 s'il existe un $\tau$, $\tau\ge t$
 tel que \mbox{$D^{\tau}_{ji} = t$}, soit alors   $c_{ij}$ défini par $ \min\{l \mid

-D^{l}_{ji} =  t \} $.  Dans ce cas, on exécution l'instruction qui 
-ajoute la valeur  \verb+Xp[i]+   dans la queue du cannal
+D^{l}_{ji} =  t \} $.  Dans ce cas, on exécute l'instruction qui 
+ajoute la valeur  \verb+Xp[i]+   dans la queue du canal

 \verb+channels[i].sent[j]+.    Alors,
 $M_{ij}^{t+1}$ est défini en étendant $M_{ij}^{t+1/2}$  à $m$ de sorte que 
 $M_{ij}^{t+1}(m)$ est $(\verb+Xp[i]+,t,c_{ij})$.  
 \verb+channels[i].sent[j]+.    Alors,
 $M_{ij}^{t+1}$ est défini en étendant $M_{ij}^{t+1/2}$  à $m$ de sorte que 
 $M_{ij}^{t+1}(m)$ est $(\verb+Xp[i]+,t,c_{ij})$.  


@@ -94,7 +94,7 @@ est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
 
 
 \begin{lemma}[Existence d'une exécution SPIN]\label{lemma:execution}
 
 
 \begin{lemma}[Existence d'une exécution SPIN]\label{lemma:execution}

-  Pour chaque  sequence $(S^t)^{t  \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, 
+  Pour chaque  séquence $(S^t)^{t  \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, 

   pour chaque fonction $F$,
   il existe une exécution SPIN  telle que pour toute itération $t$, $t
   \ge  1$, et pour chaque  $i$ et $j$ dans  $[ \mathsf{N} ]$  
   pour chaque fonction $F$,
   il existe une exécution SPIN  telle que pour toute itération $t$, $t
   \ge  1$, et pour chaque  $i$ et $j$ dans  $[ \mathsf{N} ]$  


@@ -121,21 +121,22 @@ est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
 la variable  \verb+Xp[k]+  en sortant du processus 
 \verb+update_elems+  est  égale à
 $X_k^{t}$          \textit{i.e.},          $F_{k}\left(         X_1^{D_{k\,1}^{t-1}},\ldots,
 la variable  \verb+Xp[k]+  en sortant du processus 
 \verb+update_elems+  est  égale à
 $X_k^{t}$          \textit{i.e.},          $F_{k}\left(         X_1^{D_{k\,1}^{t-1}},\ldots,

-  X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la  $t^{\text{th}}$ itération.
+  X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la  $t^{\text{ème}}$ itération.

 \end{lemma}
 \end{lemma}

-\begin{Proof}
+\begin{proof}

 La preuve est faite par induction sur le nombre d'itérations.
 
 \paragraph{Situation initiale:}
 La preuve est faite par induction sur le nombre d'itérations.
 
 \paragraph{Situation initiale:}

-Pour le premier item, par definition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(
+Pour le premier item, par définition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(

   \verb+Xp[i]+, 0,0 \right)$ qui est égal à  $\left(X_i^{D_{ji}^{0}},
   0,0 \right)$.
 Ensuite, le premier appel à la  fonction \verb+fetch_value+ 
   \verb+Xp[i]+, 0,0 \right)$ qui est égal à  $\left(X_i^{D_{ji}^{0}},
   0,0 \right)$.
 Ensuite, le premier appel à la  fonction \verb+fetch_value+ 

-soit affecte à la tête de \verb+channels[i].sent[j]+  à   \verb+Xd[j].v[i]+ soit ne modifie par 
+soit affecte la tête de \verb+channels[i].sent[j]+
+à   \verb+Xd[j].v[i]+ soit ne modifie par 

 \verb+Xd[j].v[i]+. 
 Grâce au processus \verb+init+ process, 
 les deux cas sont égaux à 
 \verb+Xd[j].v[i]+. 
 Grâce au processus \verb+init+ process, 
 les deux cas sont égaux à 

-\verb+Xp[i]+,  \textit{i.e.}, $X_i^0$.  L'equation (\ref{eq:correct_retrieve})  est ainsi établie.
+\verb+Xp[i]+,  \textit{i.e.}, $X_i^0$.  L'équation (\ref{eq:correct_retrieve})  est ainsi établie.

 
 Pour le dernier item, soit $k$, $0  \le  k \le  \mathsf{N}-1$. 
 A la fin de la première exécution du processus \verb+update_elems+,
 
 Pour le dernier item, soit $k$, $0  \le  k \le  \mathsf{N}-1$. 
 A la fin de la première exécution du processus \verb+update_elems+,


@@ -229,43 +230,45 @@ apparaître selon que $D_{ji}^{l}$ et  $D_{ji}^{l-1}$ sont égaux ou non.
 Il reste à prouver la partie inductive de la troisième partie du lemme.
 Soit $k$, $k
 \in S^{l+1}$. % and $\verb+k'+ = k-1$.
 Il reste à prouver la partie inductive de la troisième partie du lemme.
 Soit $k$, $k
 \in S^{l+1}$. % and $\verb+k'+ = k-1$.

-A l'issue de la première exécutions 
+A l'issue de la première exécution 

 du processus \verb+update_elems+, on a 
 $\verb+Xp[+k\verb+]+=                                   F(\verb+Xd[+k\verb+][0]+,
 \ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.  
 Par définition $Xd=F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      
 du processus \verb+update_elems+, on a 
 $\verb+Xp[+k\verb+]+=                                   F(\verb+Xd[+k\verb+][0]+,
 \ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$.  
 Par définition $Xd=F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      

-Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
-\end{Proof}
+Grâce à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
+\end{proof}

 
 
 \begin{lemma}
 
 
 \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$.
+  Borner la taille du canal à $\textit{max} = \delta_0$ est suffisant 
+  lorsqu'on simule un système dynamique dont les délais sont bornés par  
+  $\delta_0$.

 \end{lemma}
 
 \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{proof}
+  Pour chaque $i$ et $j$, à chaque itération $t+1$, comme les délais sont bornés par 
+  $\delta_0$,  l'élément $i$  doit connaître au plus $\delta_0$ 
+  valeurs qui sont
+  $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. Elles peuvent être mémorisées dans n'importe quel canal
+  de taille $\delta_0$.
+\end{proof}

 
 
 \promelasound*
 
 
 \promelasound*

-\begin{Proof}
+\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 ?}
 %   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}
+  Montrons la contraposée du théorème.
+  Le lemme  précédent a montré que pour chaque séquence d'itérations du système dynamique discret,
+  Il existe une exécution du modèle PROMELA qui la simule.
+  Si des itérations du système dynamique discret sont divergentes, leur exécution vont empêcher 
+  le modèle PROMELA de se stabiliser,  \textit{i.e.} 
+  ce dernier ne vérifiera pas la propriété LTL (\ref{eq:ltl:conv}).
+\end{proof}

 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}


@@ -280,10 +283,12 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
 
 \promelacomplete*
 
 
 \promelacomplete*
 

-\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.
+\begin{proof}
+  Pour chaque  modèle  $\psi$ 
+  qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
+  il est immédiat de construire les itérations correspondantes du
+  système dynamique, dont la stratégie est pseudo-périodique en raison 
+  de la propriété d'équité faible..

 
 %   i.e. iterations that  are divergent.   Executions are
 %   performed under weak  fairness property; we then detail  what are continuously
 
 %   i.e. iterations that  are divergent.   Executions are
 %   performed under weak  fairness property; we then detail  what are continuously


@@ -295,5 +300,5 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
 %   continuously enabled leading to convenient available dates $D_{ji}$.
 % \end{itemize}
 % The simulated DDN does not stabilize and its iterations are divergent.
 %   continuously enabled leading to convenient available dates $D_{ji}$.
 % \end{itemize}
 % The simulated DDN does not stabilize and its iterations are divergent.

- \end{Proof}
+ \end{proof}