dff

[hdrcouchot.git] / annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 367509427fd4718d944af697b0568acae2affe18..6b3adaa30f9719404ec6dd6a0b80436eee2f7f0f 100644 (file)
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -11,13 +11,13 @@ du chapitre~\ref{chap:promela}.
   le le scheduler met à jour les  elements of $S^t$
   donnés par \verb+update_elems+ à l'iteration $t$.
 \end{lemma}
   le le scheduler met à jour les  elements of $S^t$
   donnés par \verb+update_elems+ à l'iteration $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.
   Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie 
   les éléments de $S^t$ à l'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}

 
 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 


@@ -123,7 +123,7 @@ la variable  \verb+Xp[k]+  en sortant du processus
 $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.
 \end{lemma}
 $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.
 \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:}


@@ -235,7 +235,7 @@ $\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.
 \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}
+\end{proof}

 
 
 \begin{lemma}
 
 
 \begin{lemma}


@@ -244,17 +244,17 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
   $\delta_0$.
 \end{lemma}
 
   $\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
   $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. Elles peuvent être mémorisées dans n'importe quel cannal
   de taille $\delta_0$.
   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
   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
 %   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


@@ -267,7 +267,7 @@ Grace à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
   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}).
   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}
+\end{proof}

 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}


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

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

   Pour chaque  modele  $\psi$ 
   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
   il est immédiat de construire les itérations correpondantes du
   Pour chaque  modele  $\psi$ 
   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
   il est immédiat de construire les itérations correpondantes du


@@ -299,5 +299,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}