X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/9e9f22c16917d3bf287f5e1f0df739200c392594..fcbc9202a51285ff17060f4d330eca0d57b2a3c1:/annexePromelaProof.tex diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex index 881383c..3c0724c 100644 --- a/annexePromelaProof.tex +++ b/annexePromelaProof.tex @@ -6,18 +6,18 @@ du chapitre~\ref{chap:promela}. \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 @@ -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,8 +59,8 @@ $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 fonction pendant l'itération $t$. @@ -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,7 +94,7 @@ 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$ dans $[ \mathsf{N} ]$ @@ -121,21 +121,22 @@ est exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. 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+, @@ -229,43 +230,45 @@ apparaître selon que $D_{ji}^{l}$ et $D_{ji}^{l-1}$ sont égaux ou non. 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} @@ -280,10 +283,12 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve. \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 @@ -295,5 +300,5 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve. % 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}