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

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index ade9df0..3c0724c 100644
--- 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$. 
-  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}
@@ -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
-  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