la veille

[hdrcouchot.git] / annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index ade9df01b8b50d8b7f9f07e7c6564f003499ba4a..3c0724c17412fe07decaf21881f004a1acb6ab69 100644 (file)
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -14,7 +14,7 @@ du chapitre~\ref{chap:promela}.
 \begin{proof}
   La preuve est directe pour $t=0$.
   Supposons qu'elle est établie jusqu'en $t$ valant un certain $t_0$. 
 \begin{proof}
   La preuve est directe pour $t=0$.
   Supposons qu'elle est établie jusqu'en $t$ valant un certain $t_0$. 

-  On considère des stratégies pseudo périodiques.
+  On considère des stratégies pseudo-périodiques.

   Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie 
   les éléments de $S^t$ à l'itération $t$.
 \end{proof}
   Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie 
   les éléments de $S^t$ à l'itération $t$.
 \end{proof}


@@ -287,7 +287,7 @@ Grâce à~\Equ{eq:correct_retrieve} déjà prouvée, on peut conclure la preuve.
   Pour chaque  modèle  $\psi$ 
   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
   il est immédiat de construire les itérations correspondantes du
   Pour chaque  modèle  $\psi$ 
   qui ne vérifie pas la propriété  LTL  (\ref{eq:ltl:conv}), 
   il est immédiat de construire les itérations correspondantes du

-  système dynamique, dont la stratégie est pseudo périodique en raison 
+  système dynamique, dont la stratégie est pseudo-périodique en raison 

   de la propriété d'équité faible..
 
 %   i.e. iterations that  are divergent.   Executions are
   de la propriété d'équité faible..
 
 %   i.e. iterations that  are divergent.   Executions are