X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/d31be79de69d9af9371a3b1fcb3df81246c5928a..fcbc9202a51285ff17060f4d330eca0d57b2a3c1:/talk/sdd2promela.tex?ds=inline

diff --git a/talk/sdd2promela.tex b/talk/sdd2promela.tex
index 4676dfa..9389fc3 100644
--- 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.
-\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}
+
 
 \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}
+
+% \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}