avant chgt de salle

[hdrcouchot.git] / annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index dbc5774c131f8fda93f4de707cedf2edcace8dfa..70981a92fef0588cd3fcb0b7b340712144568724 100644 (file)
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -5,37 +5,43 @@ du chapitre~\ref{chap:promela}.
 
 
 \begin{lemma}[Strategy Equivalence]\label{lemma:strategy}
 
 
 \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}
 \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}
 
 \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
 % \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 
 %\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 
 %\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}
 %\end{itemize}

-$M_{ij}^t$ has the following signature:
+$M_{ij}^t$ a la signature suivante:

 \begin{equation*}
 \begin{array}{rrcl}
 M_{ij}^t: & 
 \begin{equation*}
 \begin{array}{rrcl}
 M_{ij}^t: & 


@@ -44,102 +50,114 @@ M_{ij}^t: &
 \end{array}  
 \end{equation*}
 
 \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}$.
 
 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) \\
 \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}
       \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}
 \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_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}
 \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)$.
   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
 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}
 
 
 \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
 \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}
 
 
 % \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
 \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