X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/251b65007a909068d3344bd82b7c5ec0ffb0a21a..cc983a19dffed6f28851e7e37f0277fb19098f2f:/annexePromelaProof.tex?ds=inline

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index dbc5774..1f70e9f 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -228,11 +228,7 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 \end{Proof}
 
 
-\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound}
-  Let $\phi$ be  a DDN model and $\psi$ be its  translation.  If $\psi$ verifies
-  the  LTL  property  (\ref{eq:ltl:conv})  under weak  fairness  property,  then
-  iterations of $\phi$ are universally convergent.
-\end{theorem}
+\promelasound*
 \begin{Proof}
 %   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
 %   verification  is achieved  under  weak fairness  property.  Instructions  that
@@ -259,12 +255,8 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 % \end{Corol}
 
 
+\promelacomplete*
 
-\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness}
-  Let $\phi$ be a  DDN model and $\psi$ be its translation.   If $\psi$ does not
-  verify the LTL property  (\ref{eq:ltl:conv}) under weak fairness property then
-  the iterations of $\phi$ are divergent.
-\end{theorem}
 \begin{Proof}
   For models $\psi$  that do not verify the  LTL property (\ref{eq:ltl:conv}) it
   is easy  to construct corresponding iterations  of the DDN,  whose strategy is