X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/4e673fe23eacd3db39c4bc51610f1650c372b13c..1d675a69268d7b43ff2d7321c7bd44413f1c10a5:/modelchecking.tex?ds=inline

diff --git a/modelchecking.tex b/modelchecking.tex
index 6f968bb..1919416 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -26,7 +26,7 @@ donnÃ© par l'outil.
 Cependant, mÃªme pour des rÃ©seaux discrets Ã  peu d'Ã©lÃ©ments, 
 le nombre de configurations induites explose rapidement.
 Les \emph{Model-Checkers}~\cite{Hol03,nusmv02,Blast07,MCErlang07,Bogor03}  
-sont des classes d'outils qui addressent le problÃ¨me de vÃ©rifier automatiquement
+sont des classes d'outils qui adressent le problÃ¨me de vÃ©rifier automatiquement
 qu'un modÃ¨le vÃ©rifie une propriÃ©tÃ© donnÃ©e. Pour traiter le problÃ¨me d'explosion 
 combinatoire, ces outils appliquent des mÃ©thodes d'ordre partiel, d'abstraction,
 de quotientage selon une relation d'Ã©quivalence.
@@ -69,7 +69,7 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
     \hfill
     \subfigure[Graphe d'intÃ©raction]{
       \includegraphics[width=4cm]{images/xplCnxMc.eps}
-      \label{fig:xplgraph}
+      \label{fig:xplgraph:inter:mc}
     }
   \end{center}
   \caption{Exemple pour SDD $\approx$ SPIN.}
@@ -79,10 +79,10 @@ sont ensuite fournies (\Sec{sec:spin:practical}).
 
 \begin{xpl}
   On considÃ¨re un exemple Ã  trois Ã©lÃ©ments dans $\Bool$. 
-  Chaque configuration est ainsi un Ã©lement de $\Bool^3$, \textit{i.e.}, 
+  Chaque configuration est ainsi un Ã©lÃ©ment de $\Bool^3$, \textit{i.e.}, 
   un nombre entre 0 et 7. 
   La \Fig{fig:map} prÃ©cise la fonction $f$ considÃ©rÃ©e et 
-  la \Fig{fig:xplgraph} donne son graphe d'intÃ©raction.
+  la \Fig{fig:xplgraph:inter:mc} donne son graphe d'intÃ©raction.
   
 
 
@@ -300,7 +300,7 @@ active proctype scheduler(){
 }
 \end{lstlisting}
 \end{tiny}
-\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©rodique.
+\caption{Process scheduler pour la stratÃ©gie pseudo pÃ©riodique.
  \label{fig:scheduler}}
 \end{minipage}
 \begin{minipage}[h]{.30\linewidth}
@@ -340,7 +340,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.
 Intuitivement, un process \verb+scheduler+ (comme reprÃ©sentÃ© Ã  la {\sc Figure}~\ref{fig:scheduler}) 
-est iterrativement appelÃ© pour construire chaque $s^t$ reprÃ©sentant 
+est itÃ©rativement 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
@@ -435,7 +435,7 @@ inline F(){
 \item elle mÃ©morise dans  \texttt{Xd} la valeurs disponible pour chaque Ã©lÃ©ment  grÃ¢ce Ã   la fonction \texttt{fetch\_values}; cette fonction est dÃ©taillÃ©e 
 dans la section suivante;
 \item  une boucle %sur les  \texttt{ar\_len} Ã©lÃ©ments qui peuvent Ãªtre modifiÃ©s
-  met Ã  jour iterrativement la valeur de $j$ (grÃ¢ce Ã  l'appel de fonction \texttt{f(j)})
+  met Ã  jour itÃ©rativement 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$;
@@ -553,7 +553,7 @@ Il y a deux cas.
 Les valeurs des Ã©lÃ©ments sont ajoutÃ©es dans ce canal au travers de la fonction  \verb+diffuse_values+. L'objectif de cette fonction 
 est de stocker les valeurs de $x$  (reprÃ©sentÃ©
 dans le modÃ¨le par \verb+Xp+) dans le canal  \verb+channels+.
-Il permet au modÃ¨le-checker SPIN  d'exÃ©cuter 
+Il permet au model-checker SPIN  d'exÃ©cuter 
 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}
@@ -658,7 +658,7 @@ puis prÃ©sente ensuite les expÃ©rimentations issues de ce travail.
   de l'exÃ©cution en SPIN de $\psi$ est bornÃ©e par $2^{m(\delta_0+1)+n(n+2)}$.
 \end{theorem}
 \begin{Proof}
-  Une configuration est une valuation des variables globales.
+  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.
