\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}
- Borner la taille du cannal à $\textit{max} = \delta_0$ est suffisant
+ 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}
+\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
+ $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}
+\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 ?}
- Montrons la conraposée du théorème.
+ 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 verifiera pas la propriété LTL (\ref{eq:ltl:conv}).
-\end{Proof}
+ 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}
- Pour chaque modele $\psi$
+\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 correpondantes du
- système dynamique, dont la stratégie est pseudo périodique en raison
+ 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
% 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}
