-\JFC{Voir section~\ref{sec:spin:proof}}
+%\JFC{Voir section~\ref{sec:spin:proof}}
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}
+\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.
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}
+\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{th}}$ appel
+\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ après le $t^{\text{ème}}$ appel
à la fonction
\verb+fetch_values+.
De plus, soit $Y^k_{ij}$ l'élément à l'indice $k$
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
+la valeur de $M_{ij}^{t}$ après la première fonction pendant l'itération
$t$.
Dans ce qui suit, on considère les éléments $i$ et $j$
-dans $\llbracket n \rrbracket$.
+dans $[ \mathsf{N} ]$.
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
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$
+ \ge 1$, et pour chaque $i$ et $j$ dans $[ \mathsf{N} ]$
on a la propriété suivante:
\noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors
\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) & = &
+ \textrm{si $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}
\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
+\noindent Enfin, pour chaque $k\in S^t$, la valeur de
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.
+ 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:}
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+
+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
\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$.
+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+,
-la valur de
-\ver+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
-\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.
+la valeur de
+\verb+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
+\verb+Xd[+k\verb+].v[+\mathsf{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},
+$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,\mathsf{N}-1})$. Grâce à l'équation \Equ{eq:correct_retrieve},
on peut conclure la preuve.
-\paragraph{Inductive case:}
+\paragraph{Induction:}
+Supposons maintenant que le lemme~\ref{lemma:execution} est établi jusqu'à
+l'itération $l$.
-Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
+Tout d'abord, si le domaine de définition de la fonction $M_{ij}^l$
+n'est pas vide, par hypothèse d'induction $M_{ij}^{l}(0)$ est
+$\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
+\right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-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} \}$.
+A l'itération $l$, si $l < c + 1$ alors l'instruction
+ \verb+skip+ est exécutée dans la fonction \verb+fetch_values+.
+ Ainsi, $M_{ij}^{l+1}(0)$ est égal à
+$M_{ij}^{l}(0)$. Puisque $c > l-1$, alors $D_{ji}^c > D_{ji}^{l-1}$ et donc, $c$
+est $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.
+Cela implique que
+$D_{ji}^c > D_{ji}^{l-2}$ et $c=\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}$:
+On considère maintenant qu'à l'itération $l$, celui-ci vaut $c + 1$.
+Dit autrement, $M_{ij}$ est modifié en fonction du domaine $\dom(M^l_{ij})$ de
+ $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
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\forall k\, . \, k\ge l \Rightarrow
+ D^{k}_{ji} \neq l$ sont vraies, alors $\dom(M_{ij}^{l+1})$ est vide et le premier
+ item du lemme est vérifié;
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists k\, . \, k\ge l \land D^{k}_{ji}
+ = l$ sont vraies, alors $M_{ij}^{l+1}(0)$ vaut $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté
+ dans la fonction \verb+diffuse_values+ de sorte que $c_{ij} =
+ \min\{k \mid D^{k}_{ji} = l \} $.
+ Prouvons qu'on peut exprimer
+ $M_{ij}^{l+1}(0)$ comme $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ où
+ $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.
+ Tout d'abord, il n'est pas difficile de prouver que
+ $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ et que
+ $c_{ij} \geq c'$.
+ Ensuite, comme $\dom(M_{ij}^{l})=\{0\}$, alors, entre les
+ itérations $D_{ji}^{c}+1$ et $l-1$, la fonction \texttt{diffuse\_values} n'a pas mis à jour
+ $M_{ij}$. On a ainsi la propriété
$$
\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.
+En particulier, on a $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$.
+On peut donc appliquer le troisième item de l'hypothèse d'induction pour déduire
+$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ et on peut conclure.
+
+\item Si $\{0,1\} \subseteq \dom(M_{ij}^{l})$, alors $M_{ij}^{l+1}(0)$ vaut
+ $M_{ij}^{l}(1)$. Soit $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij}
+ \right)$. Par construction, $a_{ij}$ vaut $\min\{t' | t' > D_{ji}^c \land
+ (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ et $c_{ij}$ est $\min\{k |
+ D_{ji}^k = a_{ij}\}$. Montrons que $c_{ij}$ est égal à $\min\{k | D_{ji}^k >
+ D_{ji}^{l-1} \}$, noté plus tard $c'$. On a tout d'abord $D_{ji}^{c_{ij}} =
+ a_{ij} > D_{ji}^c$. Puisque $c$ par définition est supérieur ou égal à $l-1$,
+ alors $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ et donc $c_{ij} \geq c'$. Ensuite, puisque
+ $c=l-1$, $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ et donc $a_{ij}
+ \leq D_{ji}^{c'}$. Ainsi, $c_{ij} \leq c'$ et on peut conclure comme dans la partie précédente.
\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.
+Le cas où le domaine $\dom(M^l_{ij})$ est vide mais où la formule $\exists k
+\, .\, k \geq l \land D_{ji}^k = l$ est vraie est équivalent au second
+cas ci-dessus et n'est pas présenté.
-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.
+Concentrons nous sur la formule~(\ref{eq:correct_retrieve}). A l'itération
+$l+1$, soit $c'$ défini par $c'=\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Deux cas peuvent
+apparaître selon que $D_{ji}^{l}$ et $D_{ji}^{l-1}$ sont égaux ou non.
\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}} =
+\item Si $D_{ji}^{l} = D_{ji}^{l-1}$, puisque $D_{ji}^{c'} > D_{ji}^{l-1}$, alors
+ $D_{ji}^{c'} > D_{ji}^{l}$ et donc $c'$ est différent de $l$. L'exécution de SPIN
+ ne modifie pas $Xd_{ji}^{l+1}$. On a ainsi $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}).
+\item Sinon, $D_{ji}^{l}$ et plus grand que $D_{ji}^{l-1}$ et $c$ est donc égal à $l$.
+ Selon l'équation \Equ{eq:Mij0}, on a
+ $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Ainsi l'exécution SPIN
+ affecte $X_i^{D_{ji}^{l}}$ à $Xd_{ji}^{l+1}$, ce qui termine la preuve
+(\ref{eq:correct_retrieve}).
\end{itemize}
-We are left to prove the induction of the third part of the lemma. Let $k$, $k
+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$.
-At the end of the first execution of the \verb+update_elems+ process, we have
+A l'issue de la première exécutions
+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]+)+$. 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}
+\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}
\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
% enabled:
% \begin{itemize}
-% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are
+% \item if the strategy is not defined as periodic, elements $0$, \ldots, $\mathsf{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}
+ \end{proof}
