preuve promela:debut de traduction

[hdrcouchot.git] / mixage.tex

diff --git a/mixage.tex b/mixage.tex
index 0b24636263588e3ec9a4fb3386f96ae18e67a10f..4ee1171951de32a11e3f7674db2114cb10c5faa3 100644 (file)
--- a/mixage.tex
+++ b/mixage.tex
@@ -21,9 +21,6 @@ s^{t}=24 \textrm{ si  $t$ est pair et  } s^{t}=15 \textrm{ sinon }
 \end{equation}
 \noindent active successivement les deux premiers éléments (24 est 11000) 
 et les quatre derniers éléments (15  est  01111).  
 \end{equation}
 \noindent active successivement les deux premiers éléments (24 est 11000) 
 et les quatre derniers éléments (15  est  01111).  

-On dit que la stratégie est
-\emph{pseudo-periodique}  si tous les éléments sont activés infiniment 
-souvent.

 % , it is sufficient to establish  that the set $\{t \mid t \in \mathbb{N}
 % \land \textit{bin}(s^t)[i]  = 1\}$  is infinite for  any $i$,  $1 \le i  \le n$,
 % where
 % , it is sufficient to establish  that the set $\{t \mid t \in \mathbb{N}
 % \land \textit{bin}(s^t)[i]  = 1\}$  is infinite for  any $i$,  $1 \le i  \le n$,
 % where


@@ -54,7 +51,7 @@ souvent.
 Dans le mode asynchrone, a chaque itération $t$, chaque composant peut
 mettre à jour son état en 
 fonction des dernières valeurs qu'il connaît des autre composants.
 Dans le mode asynchrone, a chaque itération $t$, chaque composant peut
 mettre à jour son état en 
 fonction des dernières valeurs qu'il connaît des autre composants.

-Obtenir ou non les valeurs les plus à jours dépend du temps de calcul et 
+Obtenir ou non les valeurs les plus à jour dépend du temps de calcul et 

 du temps d'acheminement de celles-ci. On parle de latence, de délai.
 
 Formalisons le mode les itérations asynchrone.
 du temps d'acheminement de celles-ci. On parle de latence, de délai.
 
 Formalisons le mode les itérations asynchrone.


@@ -173,7 +170,7 @@ $$
 \noindent sinon. 
 En démarrant de $x^0=00011$, le système atteint $x^1 = 01011$ et boucle entre 
 ces deux configurations. Pour une même stratégies, les itérations 
 \noindent sinon. 
 En démarrant de $x^0=00011$, le système atteint $x^1 = 01011$ et boucle entre 
 ces deux configurations. Pour une même stratégies, les itérations 

-asynhrones divergent alors que les synchrones convergent.
+asynchrones divergent alors que les synchrones convergent.

 Les sections suivantes de ce chapitre montrent comment résoudre ce problème.
 
 \subsection{Itérations Mixes}
 Les sections suivantes de ce chapitre montrent comment résoudre ce problème.
 
 \subsection{Itérations Mixes}


@@ -190,7 +187,7 @@ Les itérations asynchrones sont conservées entre les groupes.
   La  \emph{relation de synchronisation} $\eqNode$ est
   définie sur l'ensemble des n{\oe}uds par:
   $i \eqNode j$ si $i$ et $j$  appartiennent à la même composante fortement
   La  \emph{relation de synchronisation} $\eqNode$ est
   définie sur l'ensemble des n{\oe}uds par:
   $i \eqNode j$ si $i$ et $j$  appartiennent à la même composante fortement

-  connexe (CFC) dans $\Gamma(F)$.
+  connexe (CFC) dans $\Gamma(f)$.

 \end{Def}
 
 On peut facilement démontrer que la relation de synchronisation est une 
 \end{Def}
 
 On peut facilement démontrer que la relation de synchronisation est une 


@@ -214,7 +211,7 @@ Ainsi $p_1$ et $p_2$ sont distinguables même s'ils appartiennent à la même
 classe.
 Pour gommer cette distinction, on définit le mode suivant:
 \begin{Def}[Itérations mixes avec delais uniformes]
 classe.
 Pour gommer cette distinction, on définit le mode suivant:
 \begin{Def}[Itérations mixes avec delais uniformes]

-  Le mode mixe a des \emph{délais uniformes}si pour chaque 
+  Le mode mixe a des \emph{délais uniformes} si pour chaque 

   $t=0,1,\ldots$ et pour chaque paire de  classes  $(\class{p}, \class{q})$,
   il existe une constante $d^t_{pq}$  telle que la propriété suivante est 
   établie:
   $t=0,1,\ldots$ et pour chaque paire de  classes  $(\class{p}, \class{q})$,
   il existe une constante $d^t_{pq}$  telle que la propriété suivante est 
   établie:


@@ -420,7 +417,7 @@ ascendants pour converger. On a dans ce cas:
   mode synchrone.
 \end{xpl}
 
   mode synchrone.
 \end{xpl}
 

-\subsection{Le mode généralisé asynchrone}
+\subsection{Le mode unaire asynchrone}

 \label{sec:evalasync}
 En terme de durée de convergence, ce mode peut être vu comme un 
 cas particulier du mode mixe où toutes les classes sont des singletons.
 \label{sec:evalasync}
 En terme de durée de convergence, ce mode peut être vu comme un 
 cas particulier du mode mixe où toutes les classes sont des singletons.


@@ -442,7 +439,7 @@ et apparaît lorsque chaque élément dépend des autres et que les calculs
 ne recouvrent nullement les communications.
 
 \begin{xpl}
 ne recouvrent nullement les communications.
 
 \begin{xpl}

-  La \Fig{fig:evalasync} présente un exemple d'exécution du mode généralisé 
+  La \Fig{fig:evalasync} présente un exemple d'exécution du mode unaire

   asynchrone.
   Certaines communications issues de l'élément $4$ n'ont pas été représentées
   pour des raisons de clarté.
   asynchrone.
   Certaines communications issues de l'élément $4$ n'ont pas été représentées
   pour des raisons de clarté.