-L'étude de convergence de systèmes dynamiques discrets est simple à vérifier
+Sur des petits exemples, l'étude de convergence de systèmes
+dynamiques discrets est simple à vérifier
pratiquement pour le mode synchrone. Lorsqu'on introduit des stratégies
-pseudo périodiques pour les modes unaires et généralisés, le problème
+pseudo-périodiques pour les modes unaires et généralisés, le problème
se complexifie. C'est pire encore lorsqu'on traite des itérations asynchrones
et mixtes prenant de plus en compte les délais.
convergent vers $2$ soit $(010)$; celles initialisées avec
$x^0=7$ restent en 7.
Pour les modes unaires ou généralisés avec une
-stratégie pseudo périodique, on a des comportements qui dépendent
+stratégie pseudo-périodique, on a des comportements qui dépendent
de la configuration initiale:
\begin{itemize}
\item initialisées avec 7, les itérations restent en 7;
}
\end{lstlisting}
\end{tiny}
-\caption{Process scheduler pour la stratégie pseudo périodique.
+\caption{Process scheduler pour la stratégie pseudo-périodique.
\label{fig:scheduler}}
\end{minipage}
\begin{minipage}[h]{.30\linewidth}
\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
les éléments possiblement mis à jour à l'itération $t$.
}
\end{lstlisting}
\end{tiny}
-\caption{Mise à jour des éléments.}\label{fig:proc}
+\caption{Mise à jour des éléments}\label{fig:proc}
\end{minipage}\hfill%
%\end{figure}
%\begin{figure}
}
\end{lstlisting}
\end{tiny}
-\caption{Application de la fonction $f$.}\label{fig:p}
+\caption{Application de la fonction $f$}\label{fig:p}
\end{minipage}
\end{figure}
\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
+ \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'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)+ est 0;
dans ce cas, la valeur de \verb+Xd[j].v[i]+ n'est pas modifiée;
est de stocker les valeurs de $x$ (représenté
dans le modèle par \verb+Xp+) dans le canal \verb+channels+.
Il permet au model-checker SPIN d'exécuter
-le modèle PROMELA 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
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,
+\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}
\section{Correction et complétude de la démarche}\label{sec:spin:proof}
Cette section présente les théorèmes
-de correction et de complétude de l'approche.
+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}.
+annexe~\ref{anx:promela}.
\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
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 ]
+\begin{theorem}[Nombre d'états]
Soit $\phi$ un modèle de système dynamique discret à ${\mathsf{N}}$ éléments, $m$
arcs 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(\delta_0+1)+n(n+2)}$.
+ de l'exécution en SPIN de $\psi$ est borné par $2^{m(\delta_0+1)+n(n+2)}$.
\end{theorem}
\begin{proof}
Une configuration est une évaluation des variables globales.
pour prouver formellement sa convergence universelle.
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
+alors que les preuves des deux théorèmes précédents reposent sur le fait que
cette équité 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
