preuve promela traduite

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 881383ca188b158e5c0fb60ed4632bb4ecc7f10c..367509427fd4718d944af697b0568acae2affe18 100644 (file)
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -239,15 +239,17 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
 
 
 \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 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}
 \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$.
+  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}
 
 
 \end{Proof}
 
 


@@ -259,12 +261,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 ?}
 %   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}).
+  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}
 
 
 \end{Proof}
 
 


@@ -281,9 +283,11 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
 \promelacomplete*
 
 \begin{Proof}
 \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.
+  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
 
 %   i.e. iterations that  are divergent.   Executions are
 %   performed under weak  fairness property; we then detail  what are continuously