X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/d81b15b2024adaf639e9d4a85934a5b5722c1bf1..21064a689bad8fe8e8666af593cad468f1a89483:/annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 6b3adaa..ade9df0 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -6,17 +6,17 @@ 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}$ 
-  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 
-  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}
 \begin{proof}
   La preuve est directe pour $t=0$.
-  Supposons qu'elle est Ã©tablie jusqu'en $t$ vallant un certain $t_0$. 
+  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 
-  les Ã©lÃ©ments de $S^t$ Ã  l'iteration $t$.
+  les Ã©lÃ©ments de $S^t$ Ã  l'itÃ©ration $t$.
 \end{proof}
 
 Dans ce qui suit, soit     $Xd^t_{ji}$     la valeur de 
@@ -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
- $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 
@@ -50,8 +50,8 @@ M_{ij}^t: &
 \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]+.
@@ -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}.
-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$.
@@ -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
-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})$.  
@@ -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}
-  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} ]$  
@@ -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,
-  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}
 \begin{proof}
 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+ 
-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+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+,
@@ -229,17 +230,17 @@ 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$.
-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})$.      
-Grace Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
+GrÃ¢ce Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
 \end{proof}
 
 
 \begin{lemma}
-  Borner la taille du cannal Ã  $\textit{max} = \delta_0$ est suffisant 
+  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}
@@ -248,7 +249,7 @@ Grace Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
   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 cannal
+  $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}
 
@@ -261,12 +262,12 @@ Grace Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
 %   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 ?}
-  Montrons la conraposÃ©e du thÃ©orÃ¨me.
+  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 verifiera pas la propriÃ©tÃ© LTL (\ref{eq:ltl:conv}).
+  ce dernier ne vÃ©rifiera pas la propriÃ©tÃ© LTL (\ref{eq:ltl:conv}).
 \end{proof}
 
 
@@ -283,9 +284,9 @@ Grace Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
 \promelacomplete*
 
 \begin{proof}
-  Pour chaque  modele  $\psi$ 
+  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 correpondantes du
+  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..
 
