X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/251b65007a909068d3344bd82b7c5ec0ffb0a21a..d1c0e5b780e93cf63c37b5c802d675247a4d5a21:/annexePromelaProof.tex?ds=inline diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex index dbc5774..70981a9 100644 --- a/annexePromelaProof.tex +++ b/annexePromelaProof.tex @@ -5,37 +5,43 @@ du chapitre~\ref{chap:promela}. \begin{lemma}[Strategy Equivalence]\label{lemma:strategy} - Let $\phi$ be a DDN with strategy $(S^t)^{t \in \Nats}$ and $\psi$ be its - translation. There exists an execution of $\psi$ with weak fairness s.t. the - scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$. + 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} - The proof is direct for $t=0$. Let us suppose it is established until $t$ is - some $t_0$. Let us consider pseudo-periodic strategies. Thanks to the weak - fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at - iteration $t$. + 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} -In what follows, let $Xd^t_{ji}$ be the value of -\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ after the $t^{\text{th}}$ call to the -function \verb+fetch_values+. Furthermore, let $Y^k_{ij}$ be the element at -index $k$ in the channel \verb+channels[i].sent[j]+ of size $m$, $m \le -\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are respectively the head and the tail -of the channel. Secondly, let $(M_{ij}^t)^{t \in \{1, 1.5, 2, 2.5,\ldots\}}$ be a -sequence such that $M_{ij}^t$ is the partial function that associates to each -$k$, $0 \le k \le m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering -into the \verb+update_elems+ at iteration $t$ where +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}$ is the value of the channel \verb+channels[i].sent[j]+ - at index $k$, + $Y^k_{ij}$ est la valeur du cannal \verb+channels[i].sent[j]+ + à l'indice $k$, %\item -$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and +$a^k_{ij}$ est la date (antérieure à $t$) mémorisant quand $Y^k_{ij}$ est ajouté et %\item -$c^k_{ij}$ is the first date at which the value is available on $j$. So, - the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$. +$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$ has the following signature: +$M_{ij}^t$ a la signature suivante: \begin{equation*} \begin{array}{rrcl} M_{ij}^t: & @@ -44,102 +50,114 @@ M_{ij}^t: & \end{array} \end{equation*} -Intuitively, $M_{ij}^t$ is the memory of \verb+channels[i].sent[j]+ while -starting the iteration $t$. Notice that the domain of any $M_{ij}^1$ is $\{0\}$ -and $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: indeed, the \verb+init+ process -initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+. - -Let us show how to make the indeterminism inside the two functions\linebreak -\verb+fetch_values+ and \verb+diffuse_values+ compliant with \Equ{eq:async}. -The function $M_{ij}^{t+1}$ is obtained by the successive updates of -$M_{ij}^{t}$ through the two functions\linebreak \verb+fetch_values+ and -\verb+diffuse_values+. Abusively, let $M_{ij}^{t+1/2}$ be the value of -$M_{ij}^{t}$ after the former function during iteration $t$. - -In what follows, we consider elements $i$ and $j$ both in $\llbracket 1, n -\rrbracket$ that are updated. At iteration $t$, $t \geq 1$, let -$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of -\verb+fetch_values+. If $t$ is equal to $c^0_{ij}+1$ then we execute the -instruction that assigns $Y^0_{ij}$ (\textit{i.e.}, the head value of -\verb+channels[i].sent[j]+) to $Xd_{ji}^t$. In that case, the function -$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each -$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$. -Otherwise (\textit{i.e.}, when $t < c^0_{ij}+1$ or when the domain of $M_{ij}$ -is empty) the \verb+skip+ statement is executed and $M_{ij}^{t+1/2} = +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}$. -In the function \verb+diffuse_values+, if there exists some $\tau$, $\tau\ge t$ -such that \mbox{$D^{\tau}_{ji} = t$}, let $c_{ij}$ be defined by $ \min\{l \mid -D^{l}_{ji} = t \} $. In that case, we execute the instruction that adds the -value \verb+Xp[i]+ to the tail of \verb+channels[i].sent[j]+. Then, -$M_{ij}^{t+1}$ is defined as an extension of $M_{ij}^{t+1/2}$ in $m$ such that -$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$. Otherwise (\textit{i.e.}, when $\forall l -\, . \, l \ge t \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+ -statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. - - -\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution} - For any sequences $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for - any map $F$ there exists a SPIN execution such that for any iteration $t$, $t - \ge 1$, for any $i$ and $j$ in $\llbracket 1, n \rrbracket$ we have the - following properties: +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 If the domain of $M_{ij}^t$ is not empty, then +\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{if $t \geq 2$ then }M_{ij}^t(0) & = & + \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 Secondly we have: +\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 Thirdly, for any $k\in S^t$. Then, the value of the computed variable -\verb+Xp[k]+ at the end of the \verb+update_elems+ process is equal to +\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)$ at the end of the $t^{\text{th}}$ iteration. + X_{n}^{D_{k\,{n}}^{t-1}}\right)$ à la fin de la $t^{\text{th}}$ itération. \end{lemma} \begin{Proof} -The proof is done by induction on the number of iterations. +La preuve est faite par induction sur le nombre d'itérations. -\paragraph{Initial case:} - -For the first item, by definition of $M_{ij}^t$, we have $M_{ij}^1(0) = \left( - \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}}, +\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)$. - -Next, the first call to the function \verb+fetch_value+ either assigns the head -of \verb+channels[i].sent[j]+ to \verb+Xd[j].v[i]+ or does not modify -\verb+Xd[j].v[i]+. Thanks to the \verb+init+ process, both cases are equal to -\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. The equation (\ref{eq:correct_retrieve}) is then -established. - - -For the last item, let $k$, $0 \le k \le n-1$. At the end of the first -execution\linebreak of the \verb+update_elems+ process, the value of -\verb+Xp[k]+ is\linebreak $F(\verb+Xd[+k\verb+].v[0]+, \ldots, -\verb+Xd[+k\verb+].v[+n-1\verb+]+)$. Thus, by definition of $Xd$, it is equal -to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Thanks to \Equ{eq:correct_retrieve}, -we can conclude the proof. - - - -\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 +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 +\verb+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{Induction:} +Supposons maintenant que le lemme~\ref{lemma:execution} est établi jusqu'à +l'itération $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} \}$. + +A l'itération $l$, si $l < c + 1$ alors \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 @@ -228,11 +246,7 @@ to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to \end{Proof} -\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound} - Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ verifies - the LTL property (\ref{eq:ltl:conv}) under weak fairness property, then - iterations of $\phi$ are universally convergent. -\end{theorem} +\promelasound* \begin{Proof} % For the case where the strategy is finite, one notice that property % verification is achieved under weak fairness property. Instructions that @@ -259,12 +273,8 @@ to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to % \end{Corol} +\promelacomplete* -\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness} - Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ does not - verify the LTL property (\ref{eq:ltl:conv}) under weak fairness property then - the iterations of $\phi$ are divergent. -\end{theorem} \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