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

diff --git a/modelchecking.tex b/modelchecking.tex
index ca223fb..1b8843d 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -572,20 +572,25 @@ Toutes les preuves sont déplacées en
 annexes~\ref{anx:promela}.
 
 
-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  
   Si $\psi$ vérifie
   la propriété  LTL  (\ref{eq:ltl:conv})  sous hypothèse d'équité faible,  alors
   les itérations de $\phi$ sont universellement convergentes.
-\end{theorem}
-
+\end{restatable}
 
 
-\begin{theorem}[Complétude]\label{Theo:completeness}
+\begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction.  Si $\psi$ ne vérifie pas 
   la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
   alors les itérations de  $\phi$ ne sont pas universellement convergentes.
-\end{theorem}
+\end{restatable}
+
+