X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/1b923f193392e3ce847882c24a128eff4bee9992..2cab029edf9da6ea85d0e69680545d338febc6e2:/annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 8c95761..70981a9 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -1,2 +1,294 @@
 \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}
+  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
+\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
+$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}
+
