\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}
+ 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$.
+\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$.
+\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
+% \begin{itemize}
+% \item
+ $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+
+ at index $k$,
+%\item
+$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and
+%\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$.
+%\end{itemize}
+$M_{ij}^t$ has the following signature:
+\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*}
+
+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} =
+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:
+
+\noindent If the domain of $M_{ij}^t$ is not empty, then
+\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) & = &
+ \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:
+\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
+$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.
+\end{lemma}
+\begin{Proof}
+The proof is done by induction on the number of iterations.
+
+\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}},
+ 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
+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}
+
+
+\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}
+\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}
+
+
+
+\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
+ 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}
+
\begin{figure}[ht]
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
#define N 3
#define d_0 5
chan unlock_elements_update=[1] of {bool};
chan sync_mutex=[1] of {bool};
\end{lstlisting}
-\end{scriptsize}
+\end{tiny}
\caption{Declaration des types de la traduction.}
\label{fig:arrayofchannels}
\end{figure}
Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte},
\texttt{short} et \texttt{int}. Comme dans le langage C par exemple,
-on peut declarer des tableaux à une dimension de taille constante
+on peut déclarer des tableaux à une dimension de taille constante
ou des nouveaux types de données (introduites par le mot clef
\verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux
dimension.
déclarations de variables qui serviront dans l'exemple jouet de ce chapitre.
Il définit tout d'abord:
\begin{itemize}
-\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le numbre
+\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le nombre
$n$ d'éléments et le délais maximum $\delta_0$;
\item les deux tableaux (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes;
les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $X_{i+1}$
-d'un systène dynamique discret
-(le décallage d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau);
-Elles memorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour;
+d'un système dynamique discret
+(le décalages d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau);
+Elles mémorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour;
il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $X$ à changé ou pas;
-\item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'iteration
+\item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'itération
en cours; cela correspond naturellement à l'ensemble des éléments $S^t$;
\item le type de données structurées \verb+vals+ et le tableau de tableaux
\verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $X_{j+1}^{D^{t-1}_{i+1j+1}}$
\end{itemize}
-Puisque le décallage d'un indices ne change pas fondamentalement
+Puisque le décalage d'un indices ne change pas fondamentalement
le comportement de la version PROMELA par rapport au modèle initial
-et pour des raisons de clareté, on utilisera par la suite la même
+et pour des raisons de clarté, on utilisera par la suite la même
lettre d'indice entre les deux niveaux (pour le modèle: $X_i$ et pour PROMELA:
-\texttt{X[i]}). Cependant, ce décallage devra être conservé mémoire.
+\texttt{X[i]}). Cependant, ce décalage devra être conservé mémoire.
Une donnée de type \texttt{channel} permet le
transfert de messages entre processus dans un ordre FIFO.
Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité
-(qui est constante), son nom et le type des messages qui sont stockés dans ce cannal.
+(qui est constante), son nom et le type des messages qui sont stockés dans ce canal.
Dans l'exemple précédent, on déclare successivement:
\begin{itemize}
-\item un cannal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type
+\item un canal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type
\verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+
éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $X_j$;
Il permet donc de temporiser leur emploi par d'autres elements $i$.
-\item les deux cannaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant
+\item les deux canaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant
chacun un message booléen et utilisé ensuite comme des sémaphores.
\end{itemize}
\end{xpl}
%\subsection{PROMELA Processes}
-Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurence
-au sein de systèmes. Un process est déclaréavec le mot-clef
-\verb+proctype+ et est instancié soit imédiatement (lorsque sa déclaration est préfixée
+Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurrence
+au sein de systèmes. Un process est déclaré avec le mot-clé
+\verb+proctype+ et est instancié soit immédiatement (lorsque sa déclaration est préfixée
par le mot-clef \verb+active+) ou bien au moment de l'exécution de l'instruction
\texttt{run}.
Parmi tous les process, \verb+init+ est le process initial qui permet
-d'initialiser les variables, lancer d'autres processes\ldots
+d'initialiser les variables, lancer d'autres process\ldots
-Les instructions d'affecatation sont interprétées usuellement.
-Les cannaux sont cernés par des instructions particulières d'envoi et de
-réception de messages. Pour un cannal
+Les instructions d'affectation sont interprétées usuellement.
+Les canaux sont cernés par des instructions particulières d'envoi et de
+réception de messages. Pour un canal
\verb+ch+, ces instruction sont respectivement notées
\verb+ch ! m+ et \verb+ch ? m+.
-L'instruction de réception consomme la valeur en tête du cannal \verb+ch+
+L'instruction de réception consomme la valeur en tête du canal \verb+ch+
et l'affecte à la variable \verb+m+ (pour peu que \verb+ch+ soit initialisé et non vide).
De manière similaire,l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal
\verb+ch+ (pour peu que celui-ci soit initialisé et non rempli).
-Dans les cas problématiques, canal non initialisé et vide pour une reception ou bien rempli pour un envoi,
-le processus est blocké jusqu'à ce que les conditions soient remplies.
+Dans les cas problématiques, canal non initialisé et vide pour une réception ou bien rempli pour un envoi,
+le processus est bloqué jusqu'à ce que les conditions soient remplies.
La structures de contrôle \verb+if+ (resp. \verb+do+) définit un choix non déterministe
(resp. une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle,
Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init},
une boucle de taille $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+.
-Ceci permet par la suite de verifier si les itérations sont convergentes pour n'importe
+Ceci permet par la suite de vérifier si les itérations sont convergentes pour n'importe
quelle configuration initiale $X^{(0)}$.
à $j$ s'il y a un arc de $i$ à $j$ dans le graphe d'incidence. Dans ce cas,
c'est la fonction \verb+hasnext+ (non détaillée ici)
\JFC{la détailler}
- qui memorise ce graphe
+ qui mémorise ce graphe
en fixant à \texttt{true} la variable \verb+is_succ+, naturellement et à
\texttt{false} dans le cas contraire.
Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+.
\begin{figure}[t]
\begin{minipage}[h]{.52\linewidth}
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
init{
int i=0; int j=0; bool is_succ=0;
sync_mutex ! 1;
}
\end{lstlisting}
-\end{scriptsize}
+\end{tiny}
\caption{Process init.}\label{fig:spin:init}
\end{minipage}\hfill
\begin{minipage}[h]{.42\linewidth}
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
active proctype scheduler(){
do
od
}
\end{lstlisting}
-\end{scriptsize}
-\caption{Process scheduler pour la stratégie pseudo-periodique.
+\end{tiny}
+\caption{Process scheduler pour la stratégie pseudo pérodique.
\label{fig:scheduler}}
\end{minipage}
\end{figure}
\subsection{La stratégie}\label{sub:spin:strat}
-Regardons comment une stratégie pseudo-périodique peut être représentée en PROMELA.
+Regardons comment une stratégie pseudo périodique peut être représentée en PROMELA.
Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler})
-est itérativement appelé pour construire chaque $S^t$ représentant
+est iterrativement appelé pour construire chaque $S^t$ représentant
les éléments possiblement mis à jour à l'itération $t$.
Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore
\verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis
aléatoirement (grâce à $n$ choix successifs) et sont mémorisés dans le tableau
\verb+mods+, dont la taille est \verb+ar_len+.
-Dans la séquence d'éxécution, le choix d'un élément mis à jour est directement
-suivi par des mis àjour: ceci est réalisé grace à la modification de la valeur du sémaphore
+Dans la séquence d'exécution, le choix d'un élément mis à jour est directement
+suivi par des mis à jour: ceci est réalisé grâce à la modification de la valeur du sémaphore
\verb+unlock_elements_updates+.
\subsection{Itérer la fonction $F$}\label{sub:spin:update}
La mise à jour de l'ensemble $S^t=\{s_1,\ldots, s_m\}$ des éléments qui constituent la stratégie
$(S^t)^{t \in \Nats}$ est implanté à l'aide du process \verb+update_elems+ fourni à la
{\sc Figure}~\ref{fig:proc}.
-Ce process actif attend jusqu'à ce qu'il soit déblocqué par le process
+Ce process actif attend jusqu'à ce qu'il soit débloqué par le process
\verb+scheduler+ à l'aide du sémaphore \verb+unlock_elements_update+.
L'implantation contient donc cinq étapes:
\item elle commence en mettant à jour la variable \texttt{X} avec les valeurs de \texttt{Xp}
dans la fonction \texttt{update\_X} (non détaillée ici);
\item elle mémorise dans \texttt{Xd} la valeurs disponibles des éléments grâce à
- la function \texttt{fetch\_values} (cf. \Sec{sub:spin:vt});
+ la fonction \texttt{fetch\_values} (cf. \Sec{sub:spin:vt});
\item une boucle sur les \texttt{ar\_len} éléments qui peuvent être modifiés
- met à jour itérativement la valeur de $j$ (grace à l'appel de fonction \texttt{F(j)})
+ met à jour iterrativement la valeur de $j$ (grâce à l'appel de fonction \texttt{F(j)})
pour peu que celui-ci doive être modifié, \textit{i.e.}, pour peu qu'il soit renseigné dans
\texttt{mods[count]}; le code source de \texttt{F} est donné en {\sc Figure}~\ref{fig:p} et est une
traduction directe de l'application $F$;
-\item les nouvelles valeurs des éléments \texttt{Xp} sont symbolicallement envoyés aux
+\item les nouvelles valeurs des éléments \texttt{Xp} sont symboliquement envoyés aux
autres éléments qui en dépendent grâce à la fonction
\texttt{diffuse\_values(Xp)} (cf. \Sec{sub:spin:vt});
-\item finallement, le process informe le scheduler de la fin de la tâche
- (au travers du semaphore \texttt{sync\_mutex}).
+\item finalement, le process informe le scheduler de la fin de la tâche
+ (au travers du sémaphore \texttt{sync\_mutex}).
\end{enumerate}
\begin{figure}[t]
\begin{minipage}[h]{.475\linewidth}
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
active proctype update_elems(){
do
od
}
\end{lstlisting}
-\end{scriptsize}
+\end{tiny}
\caption{Mise à jour des éléments.}\label{fig:proc}
\end{minipage}\hfill%
%\end{figure}
%\begin{figure}
\begin{minipage}[h]{.45\linewidth}
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
inline F(){
if
fi
}
\end{lstlisting}
-\end{scriptsize}
+\end{tiny}
\caption{Application de la fonction $F$.}\label{fig:p}
\end{minipage}
\end{figure}
\subsection{Gestion des délais}\label{sub:spin:vt}
-Cette section montre comment les délais inérents au mode asynchrone sont
+Cette section montre comment les délais inhérents au mode asynchrone sont
traduits dans le modèle PROMELA grâce à deux
fonctions \verb+fetch_values+ et \verb+diffuse_values+.
Celles-ci sont données en {\sc Figure}~\ref{fig:val} et~\ref{fig:broadcast},
\begin{figure}[t]
\begin{minipage}[h]{.475\linewidth}
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
inline fetch_values(){
int countv = 0;
od
}
\end{lstlisting}
-\end{scriptsize}
+\end{tiny}
\caption{Récupérer les valeurs des elements\label{fig:val}}
\end{minipage}\hfill%
\begin{minipage}[h]{.475\linewidth}
-\begin{scriptsize}
+\begin{tiny}
\begin{lstlisting}
inline diffuse_values(values){
int countb=0;
od
}
\end{lstlisting}
-\end{scriptsize}
+\end{tiny}
\caption{Diffuser les valeurs des elements}\label{fig:broadcast}
\end{minipage}
\end{figure}
-La première fonction met à jour le tableau array \verb+Xd+ recquis pour les éléments
+La première fonction met à jour le tableau \verb+Xd+ requis pour les éléments
qui doivent être modifiés.
Pour chaque élément dans \verb+mods+, identifié par la variable
-$j$, la fonction récupère les valeurs des autres éléments (dont le libélé est $i$)
+$j$, la fonction récupère les valeurs des autres éléments (dont le libellé est $i$)
dont $j$ dépend. \JFC{vérifier si c'est ce sens ici}
Il y a deux cas.
\begin{itemize}
\item puisque $i$ connaît sa dernière valeur (\textit{i.e.}, $D^t_{ii}$ est toujours $t$)
\verb+Xd[i].v[i]+ est donc \verb+Xp[i]+;
-\item sinon, il y a deux sous-cas qui peuvent peuvent potentiellement modifier la valeur
- que $j$ a de $i$ (et qui peuvent être choisies de manière alléatoire):
+\item sinon, il y a deux sous cas qui peuvent peuvent potentiellement modifier la valeur
+ que $j$ a de $i$ (et qui peuvent être choisies de manière aléatoire):
\begin{itemize}
\item depuis la perspective de $j$ la valeur de $i$ peut ne pas avoir changé (
c'est l'instruction \verb+skip+) ou n'est pas utile; ce dernier cas apparaît
- lorsqu'il n'y a pas d'arce de $i$ à $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
+ lorsqu'il n'y a pas d'arc de $i$ à $j$ dans le graphe d'incidence, \textit{i.e.}, lorsque
la valeur de \verb+is_succ+ qui est calculée par \verb+hasnext(i,j)+ is 0;
dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiée;
\item sinon, on affecte à \verb+Xd[j].v[i]+ la valeur mémorisée
- dansle cannal \verb+channels[i].sent[j]+ (pour peu que celui-ci ne soit pas vide).
- Les valeurs des éléments sont ajoutées dans ce cannal au travers de la fonction \verb+diffuse_values+
+ dans le canal \verb+channels[i].sent[j]+ (pour peu que celui-ci ne soit pas vide).
+ Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonction \verb+diffuse_values+
donnée juste après.
\end{itemize}
\end{itemize}
L'objectif de la fonction \verb+diffuse_values+ est de stocker les valeurs de $X$ représenté
-dans le modèle par \verb+Xp+ dans le cannal \verb+channels+.
+dans le modèle par \verb+Xp+ dans le canal \verb+channels+.
Il permet au modèle-checker SPIN d'exécuter
-le modèle PROMELA model comme s'il pouvait y avoir des délais entre processus
+le modèle PROMELA comme s'il pouvait y avoir des délais entre processus
Il y a deux cas différents pour la valeur de $X_{j}$:
\begin{itemize}
\item soit elle est \og perdue\fg{}, \og oubliée\fg{} pour permettre à $i$ de ne pas tenir compte d'une
des valeurs de $j$; ce cas a lieu soit lors de l'instruction \verb+skip+ ou lorsqu'il
n'y a pas d'arc de $j$ à $i$ dans le graphe d'incidence;
-\item soit elle est mémorisée dans le cannal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein).
+\item soit elle est mémorisée dans le canal \verb+channels[j].sent[i]+ (pour peu que celui-ci ne soit pas plein).
\end{itemize}
L'introduction de l'indéterminisme à la fois dans les fonctions \verb+fetch_values+
et \verb+diffuse_values+ est nécessaire dans notre contexte. Si celui-ci n'était
présent que dans la fonction \verb+fetch_values+, nous ne pourrions pas par exemple récupérer
la valeur $X_i^{(t)}$ sans considérer la valeur $X_i^{(t-1)}$.
-De manière duale, si le non-determinism était uniquement
+De manière duale, si le non déterminisme était uniquement
utilisé dans la fonction \verb+diffuse_values+, alors chaque fois qu'une valeur serait
-mise dans le cannal, elle serait immédiatement consommé, ce qui est contradictoire avec la notion de
+mise dans le canal, elle serait immédiatement consommé, ce qui est contradictoire avec la notion de
délai.
% \subsection{Discussion}
% The use of the \verb+atomic+ keyword allows the grouping of
% instructions, making the PROMELA code and the DDN as closed as possible.
-\subsection{Propriéte de convergence universelle}
+\subsection{Propriété de convergence universelle}
Il reste à formaliser dans le model checker SPIN que les itérations d'un système
dynamique à $n$ éléments est universellement convergent.
-We first recall that the
-variables \verb+X+ and \verb+Xp+ respectively contain the value of $X$ before
-and after an update. Then, by applying a non-deterministic initialization of
-\verb+Xp+ and applying a pseudo-periodic strategy, it is necessary and
-sufficient to establish the following Linear Temporal Logic (LTL) formula:
+Rappelons tout d'abord que les variables \verb+X+ et \verb+Xp+
+contiennent respectivement la valeur de $X$ avant et après la mise à jour.
+Ainsi, si l'on effectue une initialisation non déterministe de
+\verb+Xp+ et si l'on applique une stratégie pseudo périodique,
+il est nécessaire et suffisant
+de prouver la formule temporelle linéaire (LTL) suivante:
\begin{equation}
\diamond (\Box \verb+Xp+ = \verb+X+)
\label{eq:ltl:conv}
\end{equation}
-where $\diamond$ and $\Box$ have the usual meaning \textit{i.e.}, respectively
-{\em eventually} and {\em always} in the subsequent path. It is worth noticing
-that this property only ensures the stabilization of the system, but it does not
-provide any information over the way the system converges. In particular, some
-indeterminism may still be present under the form of multiple fixed points
-accessible from some initial states.
+où les opérateur $\diamond$ et $\Box$ on la sémantique usuelle \textit{i.e.}, à savoir
+respectivement {\em éventuellement} et {\em toujours} dans les chemins suivants.
+On note que cette propriété assure seulement la stabilisation du système,
+mais ne donne aucune métrique quant à la manière dont celle-ci est obtenue.
+En particulier, on peut converger très lentement ou le système peut même
+disposer de plusieurs points fixes.
+vers plusieurs
+\section{Correction et complétude de la démarche}\label{sec:spin:proof}
-\section{Proof of Translation Correctness}\label{sec:spin:proof}
-\JFC{Déplacer les preuves en annexes}
+Cette section présente les théorème de correction et de complétude de l'approche.
+(Théorèmes~\ref{Theo:sound} et~\ref{Theo:completeness}).
+Toutes les preuves sont déplacées en
+annexes~\ref{anx:promela}.
-This section establishes the soundness and completeness of the approach
-(Theorems~\ref{Theo:sound} and ~\ref{Theo:completeness}). Technical lemmas are
-first shown to ease the proof of the two theorems.
-
-
-% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock}
-% Let $\phi$ be a DDN model and $\psi$ be its translation. There is no deadlock
-% in any execution of $\psi$.
-% \end{Lemma}
-% \begin{Proof}
-% In current translation, deadlocks of PROMELA may only be introduced through
-% sending or receiving messages in channels. Sending (resp. receiving) a
-% message in the \verb+diffuse_values+ (resp. \verb+fetch_values+) function is
-% executed only if the channel is not full (resp. is not empty). In the
-% \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value
-% in any semaphore channel (\verb+unlock_elements_update+ and
-% \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the
-% way.
-% \end{Proof}
-
-
-\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$.
-\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$.
-\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
-% \begin{itemize}
-% \item
- $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+
- at index $k$,
-%\item
-$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and
-%\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$.
-%\end{itemize}
-$M_{ij}^t$ has the following signature:
-\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*}
-
-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} =
-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:
-
-\noindent If the domain of $M_{ij}^t$ is not empty, then
-\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) & = &
- \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:
-\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
-$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.
-\end{lemma}
-\begin{Proof}
-The proof is done by induction on the number of iterations.
-
-\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}},
- 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
-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}
-
-
-\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.
+\begin{theorem}[Correction]\label{Theo:sound}
+ Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
+ Si $\psi$ vérifie
+ la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, alors
+ les itérations de $\phi$ sont universellement convergentes.
\end{theorem}
-\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}
-
-\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.
+\begin{theorem}[Complétude]\label{Theo:completeness}
+ Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction. Si $\psi$ ne vérifie pas
+ la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
+ alors les itérations de $\phi$ ne sont pas universellement convergentes.
\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
- 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}
-\section{Practical Issues}
+\section{Données pratiques}
\label{sec:spin:practical}
-This section first gives some notes about complexity and later presents
-experiments.
-%\subsection{Complexity Analysis}
-%\label{sub:spin:complexity}
-\begin{theorem}[Number of states]
- Let $\phi$ be a DDN model with $n$ elements, $m$ edges in the incidence graph
- and $\psi$ be its translation into PROMELA. The number of configurations of
- the $\psi$ SPIN execution is bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
+Cette section donne tout d'abord quelques mesures de complexité de l'approche
+puis présente ensuite les expérimentations issues de ce travail.
+
+\begin{theorem}[Nombre d'états ]
+ Soit $\phi$ un modèle de système dynamique discret à $n$ éléments, $m$ arc dans le graphe d'incidence
+ et $\psi$ sa traduction en PROMELA. Le nombre de configurations
+ de l'exécution en SPIN de $\psi$ est bornée par $2^{m\times(\delta_0+1)+n(n+2)}$.
\end{theorem}
\begin{Proof}
- A configuration is a valuation of global variables. Their number only depends
- on those that are not constant.
-
- The variables \verb+Xp+ \verb+X+ lead to $2^{2n}$ states. The variable
- \verb+Xs+ leads to $2^{n^2}$ states. Each channel of \verb+array_of_channels+
- may yield $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ states. Since the
- number of edges in the incidence graph is $m$, there are $m$ non-constant
- channels, leading to approximately $2^{m\times(\delta_0+1)}$ states. The
- number of configurations is then bounded by $2^{m\times(\delta_0+1)+n(n+2)}$.
- Notice that this bound is tractable by SPIN for small values of $n$,
- $m$ and $\delta_0$.
+ Une configuration est une valuation des variables globales.
+ Leur nombre ne dépend que de celles qui ne sont pas constantes.
+
+ Les variables \verb+Xp+ et \verb+X+ engendrent $2^{2n}$ états.
+ La variable
+ \verb+Xs+ génère $2^{n^2}$ états.
+ Chaque canal de \verb+array_of_channels+
+ peut engendrer $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ états.
+ Puisque le nombre d'arêtes du graphe d'incidence est $m$,
+ il y a $m$ canaux non constants, ce qui génère approximativement $2^{m\times(\delta_0+1)}$ états.
+ Le nombre de configurations est donc borné par $2^{m\times(\delta_0+1)+n(n+2)}$.
+ On remarque que cette borne est traitable par SPIN pour des valeurs raisonnables de $n$,
+ $m$ et $\delta_0$.
+ \JFC{Donner un ordre de grandeur de cet ordre de grandeur}
+
\end{Proof}
+La méthode détaillée ici a pu être appliquée sur l'exemple jouet
+pour prouver formellement sa convergence uniforme.
-
-The method detailed along the line of this article has been applied on the
-running example to formally prove its universally convergence.
-
-First of all, SPIN only considers weak fairness property between processes
-whereas above proofs need such a behavior to be established each time a
-non-deterministic choice is done.
-
-
-A first attempt has consisted in building the following formula
-each time an undeterministic choice between $k$ elements
-respectively labeled $l1$, \ldots $lk$ occurs:
+On peut remarquer que SPIN n'impose l'équité faible qu'entre les process
+alors que les preuves des deux théorèmes précédentes reposent sur le fait que
+celle-ci est établie dès qu'un choix indéterministe est effectué.
+Naïvement, on pourrait considérer comme hypothèse la formule suivante
+chaque fois qu'un choix indéterministe se produit entre $k$ événements
+respectivement notés $l1$, \ldots $lk$:
$$
[] <> (l == l0) \Rightarrow
(([] <> (l== l1)) \land \ldots \land ([] <> (l == lk)))
$$
-where label $l0$ denotes the line before the choice.
-This formula exactly translates the fairness property.
-The negation of such a LTL formula may then be efficiently translated
-into a Büchi automata with the tool ltl2ba~\cite{GO01}.
-However due to an explosion of the size of the product
-between this automata and the automata issued from the PROMELA program
-SPIN did not success to verify whether the property is established or not.
-
-This problem has been practically tackled by leaving spin generating all the (not necessarily fair) computations and verifying convergence property on them.
-We are then left to interpret its output with two issues.
-If property is established for all the computations,
-it is particularly established for fair ones and iterations are convergent.
-In the opposite case, when facing to a counter example, an analysis of the SPIN
-output is achieved.
-\begin{xpl}
-Experiments have shown that all the iterations of the running example are
-convergent for a delay equal to 1 in less than 10 min.
-The example presented in~\cite{abcvs05} with five elements taking boolean
-values has been verified with method presented in this article.
-Immediately, SPIN computes a counter example, that unfortunately does not
-fulfill fairness properties. Fair counter example is obtained
-after few minutes.
-All the experimentation have been realized in a classic desktop computer.
-\end{xpl}
-
-
-
-
-%However preliminary experiments have shown the interest of the approach.
-
-
-
-% The method detailed along the line of this article has been
-% applied on some examples to formally prove their convergence
-% (Fig.~\ref{fig:async:exp}).
-% In these experiments, Delays are supposed to be bounded by $\delta_0$ set to 10.
-% In these arrays,
-% $P$ is true ($\top$) provided the uniform convergence property is established, false ($\bot$) otherwise,
-% $M$ is the amount of memory usage (in MB) and
-% $T$ is the time needed on a Intel Centrino Dual Core 2 Duo @1.8GHz with 2GB of memory, both
-% to establish or refute the property.
-
-% RE is the running example of this article,
-% AC2D is a cellular automata with 9 elements taking boolean values
-% according their four neighbors
-% and BM99 is has been proposed in~\cite{BM99} and consists of 10 process
-% modifying their boolean values, but with many connected connection graph.
-
-
-
-
-
-% \begin{figure}
-% \begin{center}
-% \scriptsize
-% \begin{tabular}{|*{13}{c|}}
-% \cline{2-13}
-% \multicolumn{1}{c|}{ }
-% &\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
-% \cline{2-13}
-% \multicolumn{1}{c|}{ }
-% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
-% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-% \cline{2-13}
-% \multicolumn{1}{c|}{ }
-% &P & M & T &
-% P & M & T &
-% P & M & T&
-% P & M & T \\
-% \hline %cline{2-13}
-% Running Example &
-% $\top$ & 409 & 1m11s&
-% $\bot$ & 370 & 0.54 &
-% $\bot$ & 374 & 7.7s&
-% $\bot$ & 370 & 0.51s \\
-% \hline %\cline{2-13}
-% AC2D
-% &$\bot$ & 2.5 & 0.001s % RC07_async_mixed.spin
-% &$\bot$ & 2.5 & 0.01s % RC07_async_mixed_all.spin
-% &$\bot$ & 2.5 & 0.01s % RC07_async.spin
-% &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin
-% \hline %\cline{2-13}
-% BM99
-% &$\top$ & & %BM99_mixed_para.spin
-% &$\top$ & & % RC07_async_mixed_all.spin
-% &$\bot$ & & % RC07_async.spin
-% &$\bot$ & & \\ % RC07_async_all.spin
-% \hline %\cline{2-13}
-% \end{tabular}
-% \end{center}
-% \caption{Experimentations with Asynchronous Iterations}\label{fig:async:exp}
-% \end{figure}
-
-
-
-% The example~\cite{RC07} deals with a network composed of two genes taking their
-% values into $\{0,1,2\}$. Since parallel iterations is already diverging,
-% the same behavior is observed for all other modes.
-% The Figure~\ref{fig:RC07CE} gives the trace leading to convergence property
-% violation output by SPIN.
-% It corresponds to peridic strategy that repeats $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ and starts with $X=(0,0)$.
+où le libellé $l0$ dénote le libellé de la ligne précédent le choix indéterministe.
+Cette formule traduit exactement l'équité faible.
+Cependant en raison de l'explosion de la taille du produit entre
+l'automate de Büchi issu de cette formule et celui issu du programme PROMELA,
+SPIN n'arrive pas à vérifier si la convergence uniforme est établie ou non sur des exemples
+simples\JFC{faire référence à un tel exemple}.
+
+Ce problème a été pratiquement résolu en laissant SPIN générer toutes les traces d'exécution,
+même les non équitables, puis en le laissant vérifier la propriété de convergence dessus.
+Il reste alors à interpréter les résultats qui peuvent être de deux types. Si la convergence est
+établie pour toutes les traces, elle le reste en particulier pour les traces équitables.
+Dans le cas contraire on doit analyser le contre exemple produit par SPIN.
+
+% \begin{xpl}
+% \JFC{Reprendre ce qui suit}
+% Experiments have shown that all the iterations of the running example are
+% convergent for a delay equal to 1 in less than 10 min.
+% The example presented in~\cite{abcvs05} with five elements taking boolean
+% values has been verified with method presented in this article.
+% Immediately, SPIN computes a counter example, that unfortunately does not
+% fulfill fairness properties. Fair counter example is obtained
+% after few minutes.
+% All the experimentation have been realized in a classic desktop computer.
+% \end{xpl}
+
+
+La méthode détaillée ici a été appliquée sur des exemples pour prouver formellement
+leur convergence ou leur divergence (Fig.~\ref{fig:async:exp}).
+Dans ces expériences, les délais on été bornés par $\delta_0=10$.
+Dans ce tableau, $P$ est vrai ($\top$) si et seulement si la convergence uniforme
+est établie et faux ($\bot$) sinon. Le nombre $M$ et la taille de la mémoire consommée (en MB) et
+$T$ est le temps d'exécution sur un Intel Centrino Dual Core 2 Duo @1.8GHz avec 2GB de mémoire vive
+pour établir un verdict.
+
+L'exemple RE est l'exemple jouet de ce chapitre,
+AC2D est un automate cellulaire avec 9 elements prenant des valeurs booléennes en fonction de
+de 4 voisins et BM99, issu de~\cite{BM99} consiste en 10 process
+qui modifient leur valeur booléennes dans un graphe d'adjacence proche du graphe complet.
+
+
+\begin{figure}
+\begin{center}
+\tiny
+\begin{tabular}{|*{13}{c|}}
+\cline{2-13}
+\multicolumn{1}{c|}{ }
+&\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\
+\cline{2-13}
+\multicolumn{1}{c|}{ }
+&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} &
+\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
+\cline{2-13}
+\multicolumn{1}{c|}{ }
+&P & M & T &
+P & M & T &
+P & M & T&
+P & M & T \\
+\hline %cline{2-13}
+Running Example &
+$\top$ & 409 & 1m11s&
+$\bot$ & 370 & 0.54 &
+$\bot$ & 374 & 7.7s&
+$\bot$ & 370 & 0.51s \\
+\hline %\cline{2-13}
+AC2D
+&$\bot$ & 2.5 & 0.001s % RC07_async_mixed.spin
+&$\bot$ & 2.5 & 0.01s % RC07_async_mixed_all.spin
+&$\bot$ & 2.5 & 0.01s % RC07_async.spin
+&$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin
+\hline %\cline{2-13}
+BM99
+&$\top$ & & %BM99_mixed_para.spin
+&$\top$ & & % RC07_async_mixed_all.spin
+&$\bot$ & & % RC07_async.spin
+&$\bot$ & & \\ % RC07_async_all.spin
+\hline %\cline{2-13}
+\end{tabular}
+\end{center}
+\caption{Expérimentations avec des itérations asynchrones}\label{fig:async:exp}
+\end{figure}
+
+
+
+L'exemple~\cite{RC07} concerne un réseau composé de deux gènes à valeur dans $\{0,1,2\}$.
+Comme la convergence n'est déjà pas établie pour les itérations parallèles, il en est donc
+de même pour les itérations asynchrones.
+LA {\sc Figure}~\ref{fig:RC07CE} donne une trace de la sortie de SPIN de menant à la violation
+de la convergence. Celle-ci correspond à une stratégie périodique qui répète
+$\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ et débute avec $X=(0,0)$.
-% In the example extracted from~\cite{BM99},
-% we have 10 processors computing a binary value.
-% Due to the huge number of dependencies between these calculus,
-% $\delta_0$ is reduced to 1. It nevertheless leads to about $2^{100}$
-% configurations in asynchronous iterations.
-
-% Let us focus on checking universal convergence of asynchronous iterations
-% of example~\cite{BCVC10:ir}.
-% With a $\delta_0$ set to 5, SPIN generates an out of memory error.
-% However, it succeed to prove that the property is not established even
-% with $\delta_0$ set to 1 which is then sufficient.
-
-
-% \begin{figure}
-% \begin{center}
-% \begin{tiny}
-% \begin{tabular}{|*{7}{c|}}
-% \cline{2-7}
-% \multicolumn{1}{c|}{ }
-% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
-% \cline{2-7}
-% \multicolumn{1}{c|}{ }&
-% P & M & T&
-% P & M & T \\
-% \hline %\cline{2-7}
-% Running &
-% $\top$ & 2.7 & 0.01s &
-% $\bot$ & 369.371 & 0.509s \\
-% \hline %\cline{2-7}
-% \cite{RC07} example &
-% $\bot$ & 2.5 & 0.001s & % RC07_sync.spin
-% $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
-% \hline
-% \cite{BM99} example &
-% $\top$ & 36.7 & 12s & % BM99_sync_para.spin
-% $\top$ & & \\ % BM99_sync_chao.spin
-% \hline
-% \end{tabular}
-% \end{tiny}
-% \end{center}
-% \caption{Experimentations with Synchronous Iterations}\label{fig:sync:exp}
-% \end{figure}
-
-
-
-
-
-
-% \begin{tabular}{|*{}{c|}}
+Dans l'exemple issu de~\cite{BM99}, nous avons 10 process
+à valeur booléennes. En raison de la dépendance forte entre les éléments,
+$\delta_0$ est réduit à 1. Cela aboutit cependant à $2^{100}$
+configurations dans le mode des itérations asynchrones.
+La convergence des itérations asynchrones de l'exemple~\cite{BCVC10:ir} n'est pas établie
+lorsque pour $\delta_0$ vaut 1. Il ne peut donc y avoir convergence uniforme.
+
+\begin{figure}
+\begin{center}
+\begin{tiny}
+\begin{tabular}{|*{7}{c|}}
+\cline{2-7}
+\multicolumn{1}{c|}{ }
+&\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\
+\cline{2-7}
+\multicolumn{1}{c|}{ }&
+P & M & T&
+P & M & T \\
+\hline %\cline{2-7}
+Running &
+$\top$ & 2.7 & 0.01s &
+$\bot$ & 369.371 & 0.509s \\
+\hline %\cline{2-7}
+\cite{RC07} exemples &
+$\bot$ & 2.5 & 0.001s & % RC07_sync.spin
+$\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin
+\hline
+\cite{BM99} exemple &
+$\top$ & 36.7 & 12s & % BM99_sync_para.spin
+$\top$ & & \\ % BM99_sync_chao.spin
+\hline
+\end{tabular}
+\end{tiny}
+\end{center}
+\caption{Expérimentations avec des itérations synchrones}\label{fig:sync:exp}
+\end{figure}
+
+
+
+
+
+
+% \begin{tabular}{|*{19}{c|}}
% % \hline
% % e \\
% %
% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\
-% \end{tabular}
+% \end{tabular}
-\section{Conclusion and Future Work}
+\section{Conclusion}
\label{sec:spin:concl}
-Stochastic based prototypes have been implemented to generate both
-strategies and delays for asynchronous iterations in first in~\cite{BM99,BCV02}.
-However, since these research softwares are not exhaustive, they really give an
-formal answer when they found a counterexample. When facing convergence, they only convince
-the user about this behavior without exhibiting a proof.
-
-As far as we know, no implemented formal method tackles the problem of
-proving asynchronous iterations convergence.
-In the theoretical work~\cite{Cha06} Chandrasekaran shows that asynchronous iterations
-are convergent iff we can build a decreasing Lyaponov function,
-but does not gives any automated method to compute it.
-
-In this work, we have shown how convergence proof for any asynchronous
-iterations of discrete dynamical networks with bounded delays
-can be automatically achieved.
-The key idea is to translate the network (map, strategy) into PROMELA and
-to leave the SPIN model checker establishing the validity
-of the temporal property corresponding to the convergence.
-The correctness and completeness of the approach have been proved, notably
-by computing a SPIN execution of the PROMELA model that have the same
-behaviors than initial network.
-The complexity of the problem is addressed. It shows that non trivial example
-may be addressed by this technique.
-
+Des méthodes de simulation basées sur des stratégies et des délais générés aléatoirement
+ont déjà été présentées~\cite{BM99,BCV02}.
+Cependant, comme ces implantations ne sont pas exhaustives, elles ne donnent un résultat
+formel que lorsqu'elles fournissent un contre-exemple. Lorsqu'elles exhibent une convergence,
+cela ne permet que donner une intuition de convergence, pas une preuve.
+Autant que nous sachions, aucune démarche de preuve formelle de convergence n'a jamais été établie.
+Dans le travail théorique~\cite{Cha06}, Chandrasekaran a montré que les itérations asynchrones sont convergentes
+si et seulement si on peut construire une fonction de Lyaponov décroissante, mais il ne donne pas de méthode
+automatique pour construire cette fonction.
+
+\JFC{Déplacer ceci dans les perspective}
Among drawbacks of the method, one can argue that bounded delays is only
realistic in practice for close systems.
However, in real large scale distributed systems where bandwidth is weak,
