+Cette section donne les preuves des deux théorèmes de correction et complétude
+du chapitre~\ref{chap:promela}.
+
+
+\begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
+ Soit $\phi$ un système dynamique discret de stratégie $(S^t)^{t \in \Nats}$
+ 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$.
+\end{lemma}
+\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}
+
+Dans ce qui suit, soit $Xd^t_{ji}$ la valeur de
+\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ après le $t^{\text{th}}$ appel
+à la fonction
+\verb+fetch_values+.
+De plus, soit $Y^k_{ij}$ l'élément à l'indice $k$
+dans le canal \verb+channels[i].sent[j]+ de taille $m$, $m \le
+\delta_0$; $Y^0_{ij}$ et $Y^{m-1}_{ij}$ sont respectivement la tête et la queue
+du canal.
+De plus, soit $(M_{ij}^t)^{t \in \{1, 1.5, 2, 2.5,\ldots\}}$ une séquence telle que
+$M_{ij}^t$ est une fonction partielle qui associe à chaque
+$k$, $0 \le k \le m-1$, le tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ en entrant
+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]+
+ à l'indice $k$,
+%\item
+$a^k_{ij}$ est la date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et
+%\item
+$c^k_{ij}$ est le premier temps où cette valeur est accessible à $j$.
+La valeur est supprimée du canal $i\rightarrow j$ à la date $c^k_{ij}+1$.
+%\end{itemize}
+$M_{ij}^t$ a la signature suivante:
+\begin{equation*}
+\begin{array}{rrcl}
+M_{ij}^t: &
+\{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\
+& k \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}).
+\end{array}
+\end{equation*}
+
+Intuitivement, $M_{ij}^t$ est la mémoire du cannal
+\verb+channels[i].sent[j]+ à l'iterations $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
+\verb+diffuse_values+. Par abus, soit $M_{ij}^{t+1/2}$
+la valeur de $M_{ij}^{t}$ après la première fonctions pendant l'itération
+ $t$.
+
+Dans ce qui suit, on considère les éléments $i$ et $j$
+dans $\llbracket n \rrbracket$.
+A l'itération $t$, $t \geq 1$, soit
+$(Y^0_{ij},a^0_{ij},c^0_{ij})$ la valeur de $M_{ij}^t(0)$ en entrant
+dans la fonction
+\verb+fetch_values+.
+Si $t$ est égal à $c^0_{ij}+1$ alors on exécute
+l'instruction qui affecte $Y^0_{ij}$ (\textit{i.e.}, la valeur de tête du
+\verb+channels[i].sent[j]+) à $Xd_{ji}^t$. Dans ce cas, la fonction
+$M_{ij}^t$ est mise à jour comme suit: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ pour chaque $k$, $0 \le k \le m-2$ et $m-1$ est supprimée du domaine de $M_{ij}^{t+1/2}$.
+Sinon, (\textit{i.e.}, lorsque $t < c^0_{ij}+1$ ou lorsque le domaine de $M_{ij}$
+est vide) l'instruction \verb+skip+ est exécutée et $M_{ij}^{t+1/2} =
+M_{ij}^{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
+\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})$.
+Sinon, (\textit{i.e.}, lorsque $\forall l
+\, . \, l \ge t \Rightarrow D^{l}_{ji} \neq t$ est établie) l'instruction
+\verb+skip+
+est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
+
+
+\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 fonction $F$,
+ il existe une exécution SPIN telle que pour toute itération $t$, $t
+ \ge 1$, et pour chaque $i$ et $j$ in $\llbracket n \rrbracket$
+ on a la propriété suivante:
+
+\noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors
+\begin{equation}
+ \left\{
+ \begin{array}{rcl}
+ M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\
+ \textrm{sit $t \geq 2$ alors }M_{ij}^t(0) & = &
+ \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, }
+ c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \}
+ \end{array}
+ \right.
+ \label{eq:Mij0}
+\end{equation}
+\noindent De plus, on a :
+\begin{equation}
+ \forall t'\, .\, 1 \le t' \le t \Rightarrow Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i
+ \label{eq:correct_retrieve}
+\end{equation}
+\noindent Enfin, pour chaque $k\in S^t$, la valeurde
+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_{n}^{D_{k\,{n}}^{t-1}}\right)$ à la fin de la $t^{\text{th}}$ itération.
+\end{lemma}
+\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(
+ \verb+Xp[i]+, 0,0 \right)$ qui est égal à $\left(X_i^{D_{ji}^{0}},
+ 0,0 \right)$.
+Ensuite, lepremier 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
+\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.
+
+Pour le dernier item, soit $k$, $0 \le k \le n-1$.
+A la fin de la première exécution du processus \verb+update_elems+,
+la valur de
+\ver+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
+\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.
+Ainsi par définition de $Xd$, ceci est égal à
+$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Grâce à l'équation \Equ{eq:correct_retrieve},
+on peut conclure la preuve.
+
+
+
+\paragraph{Inductive case:}
+
+Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
+
+First, if domain of definition of the function $M_{ij}^l$ is not empty, by
+induction hypothesis $M_{ij}^{l}(0)$ is $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
+\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
+
+At iteration $l$, if $l < c + 1$ then the \verb+skip+ statement is executed in
+the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to
+$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
+is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that
+$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
+
+We now consider that at iteration $l$, $l$ is $c + 1$. In other words, $M_{ij}$
+is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$:
+\begin{itemize}
+\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow
+ D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the
+ first item of the lemma is established;
+\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji}
+ = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that
+ is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} =
+ \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express
+ $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where
+ $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to
+ establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus
+ $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between
+ iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
+ not updated $M_{ij}$. Formally we have
+$$
+\forall t,k \, .\, D_{ji}^c < t < l \land k \geq t \Rightarrow D_{ji}^k \neq
+t.$$
+
+Particularly, $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. We can apply
+the third item of the induction hypothesis to deduce
+$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude.
+
+\item if $\{0,1\} \subseteq \dom(M_{ij}^{l})$ then $M_{ij}^{l+1}(0)$ is
+ $M_{ij}^{l}(1)$. Let $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij}
+ \right)$. By construction $a_{ij}$ is $\min\{t' | t' > D_{ji}^c \land
+ (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k |
+ D_{ji}^k = a_{ij}\}$. Let us show $c_{ij}$ is equal to $\min\{k | D_{ji}^k >
+ D_{ji}^{l-1} \}$ further referred as $c'$. First we have $D_{ji}^{c_{ij}} =
+ a_{ij} > D_{ji}^c$. Since $c$ by definition is greater or equal to $l-1$ ,
+ then $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ and then $c_{ij} \geq c'$. Next, since
+ $c$ is $l-1$, $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ and then $a_{ij}
+ \leq D_{ji}^{c'}$. Thus, $c_{ij} \leq c'$ and we can conclude as in the
+ previous part.
+\end{itemize}
+
+
+The case where the domain $\dom(M^l_{ij})$ is empty but the formula $\exists k
+\, .\, k \geq l \land D_{ji}^k = l$ is established is equivalent to the second
+case given above and then is omitted.
+
+
+Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}). At iteration
+$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Two cases
+have to be considered depending on whether $D_{ji}^{l}$ and $D_{ji}^{l-1}$ are
+equal or not.
+\begin{itemize}
+\item If $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'} > D_{ji}^{l-1}$, then
+ $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$ is distinct from $l$. Thus, the SPIN
+ execution detailed above does not modify $Xd_{ji}^{l+1}$. It is obvious to
+ establish that $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} =
+ X_i^{D_{ji}^{l}}$.
+\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$.
+ According to \Equ{eq:Mij0} we have proved, we have
+ $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Then the SPIN execution
+ detailed above assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$, which ends the
+ proof of (\ref{eq:correct_retrieve}).
+\end{itemize}
+
+We are left to prove the induction of the third part of the lemma. Let $k$, $k
+\in S^{l+1}$. % and $\verb+k'+ = k-1$.
+At the end of the first execution of the \verb+update_elems+ process, we have
+$\verb+Xp[+k\verb+]+= F(\verb+Xd[+k\verb+][0]+,
+\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. By definition of $Xd$, it is equal
+to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to
+\Equ{eq:correct_retrieve} we have proved, we can conclude the 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$.
+\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}
+
+
+\promelasound*
+\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}
+
+
+% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
+% Let $\phi$ be a DDN model where strategy, $X^(0)$
+% are only constrained to be pseudo-periodic and
+% in $E$ respectively.
+% Let $\psi$ be its translation.
+% If all the executions of $\psi$ converge,
+% then iterations of $\phi$ are universally convergent.
+% \end{Corol}
+
+
+\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.
+
+% i.e. iterations that are divergent. Executions are
+% performed under weak fairness property; we then detail what are continuously
+% enabled:
+% \begin{itemize}
+% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are
+% infinitely often updated leading to pseudo-periodic strategy;
+% \item instructions that write or read into \verb+channels[j].sent[i]+ 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}
+
