X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/dd837d463f86ebb399eb1cac274139e98815fdd1..749714e242c186d9017fa85964d6c67edf1bf4d1:/annexePromelaProof.tex?ds=sidebyside

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index 70981a9..6b3adaa 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -1,26 +1,26 @@
-\JFC{Voir section~\ref{sec:spin:proof}}
+%\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}
+\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. 
   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}
+\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}
+\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 
+\verb+Xd[+$j$\verb+].v[+$i$\verb+]+  après le   $t^{\text{ème}}$ appel 
 à la fonction 
 \verb+fetch_values+. 
 De plus, soit $Y^k_{ij}$  l'élément à l'indice $k$ 
@@ -62,11 +62,11 @@ 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
+la valeur de  $M_{ij}^{t}$ après la première fonction pendant l'itération
  $t$.
 
 Dans ce qui suit, on  considère les éléments  $i$ et  $j$
-dans  $\llbracket  n  \rrbracket$. 
+dans  $[  \mathsf{N}  ]$. 
 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 
@@ -97,7 +97,7 @@ est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
   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$  
+  \ge  1$, et pour chaque  $i$ et $j$ dans  $[ \mathsf{N} ]$  
   on a la propriété suivante:
    
 \noindent Si le domaine de $M_{ij}^t$ n'est pas vide, alors
@@ -105,7 +105,7 @@ est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
   \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) & = &
+      \textrm{si $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}
@@ -117,33 +117,33 @@ est  exécutée et $M_{ij}^{t+1} = M_{ij}^{t+1/2}$.
   \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 
+\noindent Enfin, pour chaque $k\in S^t$, la valeur de 
 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.
+  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:}
 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+ 
+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 
 \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$. 
+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+,
-la valur   de
+la valeur   de
 \verb+Xp[k]+       est       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
-\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.  
+\verb+Xd[+k\verb+].v[+\mathsf{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},
+$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,\mathsf{N}-1})$.  Grâce à l'équation \Equ{eq:correct_retrieve},
 on peut conclure la preuve.
 
 
@@ -157,110 +157,117 @@ 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}$:
+A l'itération $l$, si  $l < c + 1$ alors l'instruction 
+ \verb+skip+ est exécutée dans la fonction \verb+fetch_values+. 
+ Ainsi,   $M_{ij}^{l+1}(0)$  est égal à
+$M_{ij}^{l}(0)$.  Puisque $c > l-1$, alors $D_{ji}^c > D_{ji}^{l-1}$ et donc, $c$
+est $\min\{k  | D_{ji}^k  > D_{ji}^{l-1} \}$.
+Cela implique que 
+$D_{ji}^c > D_{ji}^{l-2}$ et $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
+
+On considère maintenant qu'à l'itération $l$, celui-ci vaut $c + 1$. 
+Dit autrement, $M_{ij}$ est modifié en fonction du domaine $\dom(M^l_{ij})$ de
+ $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
+\item  si $\dom(M_{ij}^{l})=\{0\}$  et $\forall  k\,  . \,  k\ge l  \Rightarrow
+  D^{k}_{ji} \neq l$ sont vraies, alors  $\dom(M_{ij}^{l+1})$ est vide et le premier
+  item du lemme est vérifié;
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists  k\, . \, k\ge l \land D^{k}_{ji}
+  = l$  sont vraies, alors $M_{ij}^{l+1}(0)$  vaut  $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté 
+  dans  la fonction \verb+diffuse_values+ de sorte que   $c_{ij}  =
+  \min\{k  \mid  D^{k}_{ji}  = l  \}  $.   
+  Prouvons qu'on peut exprimer 
+  $M_{ij}^{l+1}(0)$  comme  $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$  où
+  $c'$ vaut  $\min\{k |  D_{ji}^k > D_{ji}^{l-1}  \}$.  
+  Tout d'abord, il n'est pas difficile de prouver que 
+  $D_{ji}^{c_{ij}}= l \geq  D_{ji}^{l} > D_{ji}^{l-1}$  et que 
+  $c_{ij}  \geq   c'$.   
+  Ensuite, comme   $\dom(M_{ij}^{l})=\{0\}$,  alors, entre les 
+  itérations $D_{ji}^{c}+1$ et $l-1$, la fonction  \texttt{diffuse\_values} n'a pas mis à jour
+   $M_{ij}$. On a ainsi la propriété
 $$
 \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.
+En particulier, on a   $D_{ji}^{c'} \not  \in \{D_{ji}^{c}+1,\ldots,l-1\}$.  
+On peut donc appliquer le troisième item de l'hypothèse d'induction pour déduire
+$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ et on peut conclure.
+
+\item  Si   $\{0,1\}  \subseteq  \dom(M_{ij}^{l})$, alors  $M_{ij}^{l+1}(0)$ vaut
+  $M_{ij}^{l}(1)$.   Soit  $M_{ij}^{l}(1)=  \left(\verb+Xp[i]+, a_{ij}  ,  c_{ij}
+  \right)$.   Par construction,  $a_{ij}$  vaut $\min\{t'  |  t' >  D_{ji}^c  \land
+  (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$  et  $c_{ij}$ est $\min\{k |
+  D_{ji}^k = a_{ij}\}$.  Montrons que   $c_{ij}$ est égal à  $\min\{k | D_{ji}^k >
+  D_{ji}^{l-1} \}$, noté plus tard $c'$.  On a tout d'abord $D_{ji}^{c_{ij}} =
+  a_{ij} >  D_{ji}^c$. Puisque $c$  par définition est supérieur ou égal à  $l-1$,
+  alors $D_{ji}^{c_{ij}}>  D_{ji}^{l-1}$ et donc $c_{ij} \geq  c'$.  Ensuite, puisque
+  $c=l-1$, $c'$ vaut  $\min\{k |  D_{ji}^k > D_{ji}^{c} \}$  et donc $a_{ij}
+  \leq  D_{ji}^{c'}$. Ainsi,  $c_{ij} \leq  c'$  et on peut conclure comme dans la partie précédente.
 \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.
+Le cas où le domaine $\dom(M^l_{ij})$ est vide mais où la formule  $\exists k
+\, .\, k \geq  l \land D_{ji}^k = l$ est vraie est équivalent au second
+cas ci-dessus et n'est pas présenté.
 
 
-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.
+Concentrons nous sur la formule~(\ref{eq:correct_retrieve}).  A l'itération 
+$l+1$, soit $c'$ défini par  $c'=\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.  Deux cas peuvent 
+apparaître selon que $D_{ji}^{l}$ et  $D_{ji}^{l-1}$ sont égaux ou non.
 \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}}   =
+\item Si  $D_{ji}^{l} = D_{ji}^{l-1}$, puisque $D_{ji}^{c'}  > D_{ji}^{l-1}$, alors
+  $D_{ji}^{c'} > D_{ji}^{l}$ et donc $c'$  est différent de  $l$. L'exécution de SPIN
+  ne modifie pas $Xd_{ji}^{l+1}$.  On a ainsi  $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}).
+\item Sinon, $D_{ji}^{l}$ et plus grand que $D_{ji}^{l-1}$ et $c$ est donc égal à $l$.
+  Selon l'équation \Equ{eq:Mij0},    on a 
+  $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$.  Ainsi l'exécution SPIN 
+  affecte  $X_i^{D_{ji}^{l}}$ à $Xd_{ji}^{l+1}$,  ce qui termine la preuve 
+(\ref{eq:correct_retrieve}).
 \end{itemize}
 
-We are left to prove the induction of  the third part of the lemma.  Let $k$, $k
+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$.
-At the  end of the first  execution of the \verb+update_elems+  process, we have
+A l'issue de la première exécutions 
+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]+)+$.  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}
+\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}
 
 
 \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$.
+  Borner la taille du cannal à $\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}
 
-\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}
+\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$.
+\end{proof}
 
 
 \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 ?}
-
-  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}
+  Montrons la conraposé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.} 
+  ce dernier ne verifiera pas la propriété LTL (\ref{eq:ltl:conv}).
+\end{proof}
 
 
 % \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound}
@@ -275,20 +282,22 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 
 \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.
+\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
+  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
 %   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
+% \item if the strategy is not  defined as periodic, elements $0$, \ldots, $\mathsf{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}
+ \end{proof}