une version de plus

[hdrcouchot.git] / annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 367509427fd4718d944af697b0568acae2affe18..3c0724c17412fe07decaf21881f004a1acb6ab69 100644 (file)
--- 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}$ 
 
 \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 
   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}
 \end{lemma}

-\begin{Proof}
+\begin{proof}

   La preuve est directe pour $t=0$.
   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 
   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 
 
 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
 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 
   à 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*}
 
 \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]+.
 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}.
 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$.
 \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
 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})$.  
 \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}
 
 
 \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} ]$  
   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,
 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}
 \end{lemma}

-\begin{Proof}
+\begin{proof}

 La preuve est faite par induction sur le nombre d'itérations.
 
 \paragraph{Situation initiale:}
 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+ 
   \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+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+,
 
 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,45 +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$.
 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})$.      
 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}
 
 
 \begin{lemma}

-  Borner la taille du cannal à $\textit{max} = \delta_0$ est suffisant 
+  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}
 
   lorsqu'on simule un système dynamique dont les délais sont bornés par  
   $\delta_0$.
 \end{lemma}
 

-\begin{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
   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 cannal
+  $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$.
   de taille $\delta_0$.

-\end{Proof}
+\end{proof}

 
 
 \promelasound*
 
 
 \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 ?}
 %   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 ?}

-  Montrons la conraposée du théorème.
+  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.} 
   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 verifiera pas la propriété LTL (\ref{eq:ltl:conv}).
-\end{Proof}
+  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}
 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}


@@ -282,11 +283,11 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
 
 \promelacomplete*
 
 
 \promelacomplete*
 

-\begin{Proof}
-  Pour chaque  modele  $\psi$ 
+\begin{proof}
+  Pour chaque  modèle  $\psi$ 

   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 

-  il est immédiat de construire les itérations correpondantes du
-  système dynamique, dont la stratégie est pseudo périodique en raison 
+  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
   de la propriété d'équité faible..
 
 %   i.e. iterations that  are divergent.   Executions are


@@ -299,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.
 %   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}