la veille

[hdrcouchot.git] / talk / sdd2promela.tex

diff --git a/talk/sdd2promela.tex b/talk/sdd2promela.tex
index 4676dfae2d37e2093afe3239a981f493292349b6..9389fc393189bf0457207c5fb6789ffa0c3365d9 100644 (file)
--- a/talk/sdd2promela.tex
+++ b/talk/sdd2promela.tex
@@ -3,10 +3,10 @@
 \begin{itemize}
 \item Stratégie: pseudo périodicité garantie par le choix indéterministe de 
   SPIN.
 \begin{itemize}
 \item Stratégie: pseudo périodicité garantie par le choix indéterministe de 
   SPIN.

-\item Délais(bornés par construction): oubli de certaines valeurs grâce à l'indéterminisme de SPIN.
+\item Délais (bornés par construction): oubli de certaines valeurs grâce à l'indéterminisme de SPIN.

 \end{itemize}
 \item Convergence universelle:   $\diamond  (\Box  \verb+Xp+ = \verb+X+)$.
 \end{itemize}
 \item Convergence universelle:   $\diamond  (\Box  \verb+Xp+ = \verb+X+)$.

-\end{itemize}
+

 
 \begin{theorem}[Correction et complétude de la traduction vers Promela~\cite{Cou10:ir}]
   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  
 
 \begin{theorem}[Correction et complétude de la traduction vers Promela~\cite{Cou10:ir}]
   Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.  


@@ -15,3 +15,16 @@
   $\psi$ vérifie
   la propriété  LTL  sous hypothèse d'équité faible.
 \end{theorem}
   $\psi$ vérifie
   la propriété  LTL  sous hypothèse d'équité faible.
 \end{theorem}

+
+% \item Equité faible grantie uniquement entre processus:
+% \begin{itemize}
+% \item L'imposer pour chaque choix où
+% \item Filtrer les traces non équitables retournée.
+% \end{itemize}
+\item Bilan: 
+\begin{itemize}
+\item Preuve automatique de convergence de modèles indpt. schéma/mode.
+\item A pu décider de la convergence d'exemples simples.
+\item Ne passe pas à l'échelle.
+\end{itemize}
+\end{itemize}