\begin{lemma}[Stratégie équivalente]\label{lemma:strategy}
Soit $\phi$ un système dynamique discret de stratégie $(S^t)^{t \in \Nats}$
- et $\psi$ sa traduction en promela.
+ et $\psi$ sa traduction en PROMELA.
Il existe une exécution de $\psi$ sous hypothèse d'équité faible telle
- le le scheduler met à jour les elements of $S^t$
- donnés par \verb+update_elems+ à l'iteration $t$.
+ le scheduler met à jour les éléments of $S^t$
+ donnés par \verb+update_elems+ à l'itération $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.
+ Supposons qu'elle est établie jusqu'en $t$ valant 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}
+ les éléments de $S^t$ à l'itération $t$.
+\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
dans la fonction \verb+update_elems+ à l'itération $t$ où
% \begin{itemize}
% \item
- $Y^k_{ij}$ est la valeur du cannal \verb+channels[i].sent[j]+
+ $Y^k_{ij}$ est la valeur du canal \verb+channels[i].sent[j]+
à l'indice $k$,
%\item
$a^k_{ij}$ est la date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et
\end{array}
\end{equation*}
-Intuitivement, $M_{ij}^t$ est la mémoire du cannal
-\verb+channels[i].sent[j]+ à l'iterations $t$.
+Intuitivement, $M_{ij}^t$ est la mémoire du canal
+\verb+channels[i].sent[j]+ à l'itération $t$.
On note que le domaine de chaque $M_{ij}^1$ est $\{0\}$ et
$M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: en effet le processus
\verb+init+ initialise \verb+channels[i].sent[j]+ avec \verb+Xp[i]+.
Montrons comment l'indéterminisme des deux fonctions
\verb+fetch_values+ et \verb+diffuse_values+
permet de modéliser l'équation \Equ{eq:async}.
-La function $M_{ij}^{t+1}$ est obtenue à l'aide de mises à jour successives
-de $M_{ij}^{t}$ au travers des deux functions \verb+fetch_values+ and
+La fonction $M_{ij}^{t+1}$ est obtenue à l'aide de mises à jour successives
+de $M_{ij}^{t}$ au travers des deux fonctions \verb+fetch_values+ and
\verb+diffuse_values+. Par abus, soit $M_{ij}^{t+1/2}$
la valeur de $M_{ij}^{t}$ après la première fonction pendant l'itération
$t$.
Dans la fonction \verb+diffuse_values+,
s'il existe un $\tau$, $\tau\ge t$
tel que \mbox{$D^{\tau}_{ji} = t$}, soit alors $c_{ij}$ défini par $ \min\{l \mid
-D^{l}_{ji} = t \} $. Dans ce cas, on exécution l'instruction qui
-ajoute la valeur \verb+Xp[i]+ dans la queue du cannal
+D^{l}_{ji} = t \} $. Dans ce cas, on exécute l'instruction qui
+ajoute la valeur \verb+Xp[i]+ dans la queue du canal
\verb+channels[i].sent[j]+. Alors,
$M_{ij}^{t+1}$ est défini en étendant $M_{ij}^{t+1/2}$ à $m$ de sorte que
$M_{ij}^{t+1}(m)$ est $(\verb+Xp[i]+,t,c_{ij})$.
\begin{lemma}[Existence d'une exécution SPIN]\label{lemma:execution}
- Pour chaque sequence $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$,
+ Pour chaque séquence $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$,
pour chaque fonction $F$,
il existe une exécution SPIN telle que pour toute itération $t$, $t
\ge 1$, et pour chaque $i$ et $j$ dans $[ \mathsf{N} ]$
la variable \verb+Xp[k]+ en sortant du processus
\verb+update_elems+ est égale à
$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.
+ X_{\mathsf{N}}^{D_{k\,{\mathsf{N}}}^{t-1}}\right)$ à la fin de la $t^{\text{ème}}$ itération.
\end{lemma}
-\begin{Proof}
+\begin{proof}
La preuve est faite par induction sur le nombre d'itérations.
\paragraph{Situation initiale:}
-Pour le premier item, par definition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(
+Pour le premier item, par définition de $M_{ij}^t$, on a $M_{ij}^1(0) = \left(
\verb+Xp[i]+, 0,0 \right)$ qui est égal à $\left(X_i^{D_{ji}^{0}},
0,0 \right)$.
Ensuite, le premier appel à la fonction \verb+fetch_value+
-soit affecte à la tête de \verb+channels[i].sent[j]+ à \verb+Xd[j].v[i]+ soit ne modifie par
+soit affecte la tête de \verb+channels[i].sent[j]+
+à \verb+Xd[j].v[i]+ soit ne modifie par
\verb+Xd[j].v[i]+.
Grâce au processus \verb+init+ process,
les deux cas sont égaux à
-\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. L'equation (\ref{eq:correct_retrieve}) est ainsi établie.
+\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. L'équation (\ref{eq:correct_retrieve}) est ainsi établie.
Pour le dernier item, soit $k$, $0 \le k \le \mathsf{N}-1$.
A la fin de la première exécution du processus \verb+update_elems+,
Il reste à prouver la partie inductive de la troisième partie du lemme.
Soit $k$, $k
\in S^{l+1}$. % and $\verb+k'+ = k-1$.
-A l'issue de la première exécutions
+A l'issue de la première exécution
du processus \verb+update_elems+, on a
$\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}
+Grâce à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
+\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 canal à $\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 canal
+ 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 contraposé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 vérifiera 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 modèle $\psi$
+ qui ne vérifie pas la propriété LTL (\ref{eq:ltl:conv}),
+ il est immédiat de construire les itérations correspondantes 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}
