Logo AND Algorithmique Numérique Distribuée

Private GIT Repository
azerazerzer
[hdrcouchot.git] / annexePromelaProof.tex
index dbc5774c131f8fda93f4de707cedf2edcace8dfa..1f70e9fa587944560b29c723c7a19f42e3274a2e 100644 (file)
@@ -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