X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/9e9f22c16917d3bf287f5e1f0df739200c392594..523864c862215a63c5133568a9771f5b8f60c89e:/annexePromelaProof.tex?ds=sidebyside

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 881383c..6b3adaa 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -11,13 +11,13 @@ du chapitre~\ref{chap:promela}.
   le le scheduler met Ã  jour les  elements of $S^t$
   donnÃ©s par \verb+update_elems+ Ã  l'iteration $t$.
 \end{lemma}
-\begin{Proof}
+\begin{proof}
   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.
   GrÃ¢ce Ã  l'hypothÃ¨se d'Ã©quitÃ© faible, \verb+update_elems+ modifie 
   les Ã©lÃ©ments de $S^t$ Ã  l'iteration $t$.
-\end{Proof}
+\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 
@@ -123,7 +123,7 @@ la variable  \verb+Xp[k]+  en sortant du processus
 $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.
 \end{lemma}
-\begin{Proof}
+\begin{proof}
 La preuve est faite par induction sur le nombre d'itÃ©rations.
 
 \paragraph{Situation initiale:}
@@ -235,37 +235,39 @@ $\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}
+\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$.
+  Borner la taille du cannal Ã  $\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}
 
-\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 cannal
+  de taille $\delta_0$.
+\end{proof}
 
 
 \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 ?}
-
-  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 conraposÃ©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}).
+\end{proof}
 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
@@ -280,10 +282,12 @@ Grace Ã ~\Equ{eq:correct_retrieve} dÃ©jÃ  prouvÃ©e, on peut conclure la preuve.
 
 \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  modele  $\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
+  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
@@ -295,5 +299,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.
- \end{Proof}
+ \end{proof}
 
