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
$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:}
\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}
\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
% 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}
