From e5bdb4c2cabc8ebc77d1e1b3d908780c45b94ecd Mon Sep 17 00:00:00 2001
From: gwen <gremond@cadoles.com>
Date: Tue, 12 Jun 2012 23:05:08 +0200
Subject: [PATCH] presentation

---
 doc/eole-report/presentation/statut.tex   | 29 ++++++++++++++++++++++-
 doc/eole-report/presentation/tiramisu.txt | 15 ++++++++++++
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/doc/eole-report/presentation/statut.tex b/doc/eole-report/presentation/statut.tex
index 1f665b6..7e596c1 100644
--- a/doc/eole-report/presentation/statut.tex
+++ b/doc/eole-report/presentation/statut.tex
@@ -32,9 +32,36 @@
  \item \texttt{eole-report/D03ReglesEtats.pdf}
  \item \texttt{doc/consistency.html}
  \end{itemize}
-
 \end{frame}
 
+\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 dans tiramisu, le modèle est suffisamment abstrait pour que son exploitation mathématique soit 
+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} 
+ \end{itemize}
+\end{frame}
+
+\begin{frame}
+ \frametitle{un peu de mathématiques : le Model Checking}
+ \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 ? 
+Pour vérifier cette propriété, on a besoin de connaître l'espace d'états ;
+\item la propriété : chaque chemin débutant dans un état accessible $P=1$ passe par un état où $Q=3$ et $P=2$ 
+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.
+
+ \end{itemize}
+\end{frame}
+
+
+
 \begin{frame}
  \frametitle{compatibilité Créole : ce qui reste à faire}
  \begin{itemize}
diff --git a/doc/eole-report/presentation/tiramisu.txt b/doc/eole-report/presentation/tiramisu.txt
index 4434a59..f3d3761 100644
--- a/doc/eole-report/presentation/tiramisu.txt
+++ b/doc/eole-report/presentation/tiramisu.txt
@@ -19,3 +19,18 @@ documents de présentation
 - `doc/eole-report/eolreport` : diff pdf entre creole ~ tiramisu
 - `tiramisu/report/` : rapport autmatique sur une config
 
+affichage du rapport en html
+-----------------------------
+
+espace d'état ou graphe d'accessibilité 
+-------------------------------------------
+
+
+- soit on a besoin de ne connaître que l'ensemble des états, par leurs liens
+- soit on a besoin de connaître les relations
+
+repérage des **deadlocks**
+
+
+
+