X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/4027522083d5f0dfb61df0df9bb8dda73a9cb72b..44a56c5eb4a1dfdf7dc67735c5c00f478cef2ede:/annexePromelaProof.tex diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex index d56d89b..3c0724c 100644 --- a/annexePromelaProof.tex +++ b/annexePromelaProof.tex @@ -1,26 +1,26 @@ -\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. + 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{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$ @@ -33,7 +33,7 @@ $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]+ + $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 @@ -50,8 +50,8 @@ M_{ij}^t: & \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]+. @@ -59,14 +59,14 @@ $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: en effet le processus 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 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 @@ -82,8 +82,8 @@ 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 +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})$. @@ -94,10 +94,10 @@ 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 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$ 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 @@ -105,7 +105,7 @@ est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. \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} @@ -117,149 +117,158 @@ est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. \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{è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, 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 +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. +\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 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é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]+)+$. 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})$. +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} @@ -274,20 +283,22 @@ to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to \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 % 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}