X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/3759a997c005ffb313be135f98820410cb6061b4..fcbc9202a51285ff17060f4d330eca0d57b2a3c1:/modelchecking.tex?ds=inline

diff --git a/modelchecking.tex b/modelchecking.tex
index 96a8586..dd4bf2e 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -1,7 +1,8 @@
 
-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. 
 
@@ -95,7 +96,7 @@ avec $x^0 \neq 7$ soit $(111)$
 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;
@@ -300,7 +301,7 @@ active proctype scheduler(){
 }
 \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}
@@ -338,7 +339,7 @@ ces notions est traduite vers un modèle PROMELA.
 
 
 \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$.
@@ -405,7 +406,7 @@ active proctype update_elems(){
 }
 \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}
@@ -425,7 +426,7 @@ inline F(){
 }
 \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}
 
@@ -540,8 +541,7 @@ Il y a deux cas.
 \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;
@@ -554,7 +554,7 @@ Les valeurs des éléments sont ajoutées dans ce canal au travers de la fonctio
 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 
@@ -595,7 +595,7 @@ dynamique à ${\mathsf{N}}$ éléments est universellement convergent.
 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}
@@ -617,10 +617,10 @@ disposer de plusieurs points fixes.
 \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}
@@ -651,11 +651,11 @@ annexes~\ref{anx:promela}.
 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.
@@ -679,7 +679,7 @@ La méthode détaillée ici a pu être appliquée sur l'exemple
 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