From d5ef46635048a70507bf4868248c9003da8138a1 Mon Sep 17 00:00:00 2001 From: gwen Date: Wed, 13 Jun 2012 08:37:27 +0200 Subject: [PATCH] eole presentation --- doc/eole-report/presentation/definition.tex | 8 ++++---- doc/eole-report/presentation/statut.tex | 10 ++++++---- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/doc/eole-report/presentation/definition.tex b/doc/eole-report/presentation/definition.tex index b87b759..65166e4 100644 --- a/doc/eole-report/presentation/definition.tex +++ b/doc/eole-report/presentation/definition.tex @@ -2,7 +2,7 @@ \frametitle{Gestionnaire de configuration existants} \begin{itemize} \item Le gestionnaire de conf de Victor Stinner $\Rightarrow$ \emph{NuFw}; - \item puppet, cfgengine... $\Rightarrow$ intéressant, de nombreux comportement peuvent être repris, mais tel quel difficilement compatible avec \emph{Creole}; + \item puppet, cfgengine... $\Rightarrow$ intéressant, de nombreux comportements peuvent être repris, mais tel quel difficilement compatible avec \emph{Creole}; \item \emph{Creole} $\Leftrightarrow$ \texttt{tiramisu/doc/build/glossary.html} \end{itemize} \end{frame} @@ -17,9 +17,9 @@ \item Et en plus : \begin{itemize} - \item \emph{Créole} valide le type mais pas la structure (fait confiance au \texttt{XML}) ; - \item \emph{Créole} difficile d'ajouter un type à cause de la métaclasse ; - \item \emph{Tiramisu} valide le type \emph{et} la structure, ajout de types aisé. + \item \emph{Créole} valide le type mais pas la structure (fait trop confiance au \texttt{XML}) ; + \item Avec \emph{Créole} il est compliqué d'ajouter un type à cause de la métaclasse ; + \item \emph{Tiramisu} valide le type \emph{et} la structure, et l'ajout de types est aisé. \end{itemize} \item \texttt{eole-report/D02CoherenceVariables.pdf} \end{itemize} diff --git a/doc/eole-report/presentation/statut.tex b/doc/eole-report/presentation/statut.tex index 7e596c1..575de2f 100644 --- a/doc/eole-report/presentation/statut.tex +++ b/doc/eole-report/presentation/statut.tex @@ -37,17 +37,18 @@ \begin{frame} \frametitle{un peu de mathématiques : prévenir les deadlocks} \begin{itemize} -\item sûreté : quelque chose de mauvais (deadlock) ne se produira pas +\item sûreté : prévention des deadlocks ; \item dans tiramisu, le modèle est suffisamment abstrait pour que son exploitation mathématique soit -réalisable par les techniques de \emph{Model Checking}; +réalisable par les techniques de \emph{Model Checking} ; \item soit on a besoin de ne connaître que l'ensemble des états, pas leurs liens $\Rightarrow$ espace d'états ; \item soit on a besoin de connaître toutes les relations $\Rightarrow$ graphe d'accessibilité ; -\item la configuration peut alors être formalisée en une structures de \emph{Kripe} +\item la configuration est modélisable en une structure de \emph{Kripe} ; +\item déjà le parsing de la conf est facile \texttt{tiramisu/report/build/index.html} \end{itemize} \end{frame} \begin{frame} - \frametitle{un peu de mathématiques : le Model Checking} + \frametitle{un peu de mathématiques (suite) CreoleLint} \begin{itemize} \item exemple : $ P = 3 \wedge Q = 1 \triangleleft \langle P = 1 \hookleftarrow Q = 0 \rangle$ \item la propriété dans aucun état on a $P = 3$ et $Q = 1$ est-elle vraie ? @@ -56,6 +57,7 @@ Pour vérifier cette propriété, on a besoin de connaître l'espace d'états ; est-elle vraie ? Cela demande de connaître le graphe d'accessibilité : \item les structures de \emph{Kripe} sont des machines à états étiquetées par les valuations de toutes les variables propositionnelles. +\item une compliation statique devient possible dans \emph{CreoleLint} \dots \end{itemize} \end{frame}