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}
$\delta_0$.
\end{lemma}
-\begin{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}
+\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
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}
% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
\promelacomplete*
-\begin{Proof}
+\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
% 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}
