ajout d'intro et de conclusion

[hdrcouchot.git] / modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index b01a5263206e40ce136091ec1376e7548000d8b4..d9e626e015fd099041e8bfa4d0bbac4aef8a96ea 100644 (file)
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -657,7 +657,7 @@ puis présente ensuite les expérimentations issues de ce travail.
   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)}$.
 \end{theorem}
   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)}$.
 \end{theorem}

-\begin{Proof}
+\begin{proof}

   Une configuration est une évaluation des variables globales.
   Leur nombre ne dépend que de celles qui ne sont pas constantes.
 
   Une configuration est une évaluation des variables globales.
   Leur nombre ne dépend que de celles qui ne sont pas constantes.
 


@@ -673,7 +673,7 @@ puis présente ensuite les expérimentations issues de ce travail.
   $m$ et $\delta_0$.
   %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
   
   $m$ et $\delta_0$.
   %\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
   

-\end{Proof}
+\end{proof}

 
 La méthode détaillée ici a pu être appliquée sur l'exemple
 pour prouver formellement sa convergence universelle.
 
 La méthode détaillée ici a pu être appliquée sur l'exemple
 pour prouver formellement sa convergence universelle.