presentation
[tiramisu.git] / doc / eole-report / presentation / statut.tex
1 \begin{frame}
2  \frametitle{Organisation en espace de nommage}
3  \begin{itemize}
4   \item dans \emph{tiramisu} l'accent est mis sur l'organisation arborescente des données ;
5   \item la validation des options de configuration se fait par l'appartenance aux groupes (families, master/slaves \dots) ;
6   \item l'organisation en groupes est unifiée par l'espace de nommage ;
7   \item la lisibilité de l'API excellente, contrairement à \emph{Creole}
8   \item \texttt{eole-report/D03ReglesEtats.pdf}
9   \item lisibilité d'une config : \texttt{tiramisu/report/build/index.html} rapport html d'une config
10
11  \end{itemize}
12
13 \end{frame}
14
15 \begin{frame}
16  \frametitle{Etats de la configuration}
17  \begin{itemize}
18   \item système d'états de la configuration par droits d'accès
19   \item \texttt{read write}, \texttt{read only};
20   \item correspond à \texttt{freeze}, \texttt{hidden}, \texttt{disabled} \dots ;
21   \item \texttt{doc/status.html}
22   \item \texttt{eole-report/D03ReglesEtats.pdf}
23  \end{itemize}
24
25 \end{frame}
26
27 \begin{frame}
28  \frametitle{hidden if in, hidden if not in}
29  \begin{itemize}
30  \item les hidden if in, disabled if, \dots sont généralisés
31  \item dans tiramisu, ce sont des pré-requis sur une (des) variables
32  \item \texttt{eole-report/D03ReglesEtats.pdf}
33  \item \texttt{doc/consistency.html}
34  \end{itemize}
35 \end{frame}
36
37 \begin{frame}
38  \frametitle{un peu de mathématiques : prévenir les deadlocks}
39  \begin{itemize}
40 \item sûreté : quelque chose de mauvais (deadlock) ne se produira pas
41 \item dans tiramisu, le modèle est suffisamment abstrait pour que son exploitation mathématique soit 
42 réalisable par les techniques de \emph{Model Checking}; 
43 \item soit on a besoin de ne connaître que l'ensemble des états, pas leurs liens $\Rightarrow$ espace d'états ; 
44 \item soit on a besoin de connaître toutes les relations $\Rightarrow$ graphe d'accessibilité ; 
45 \item la configuration peut alors être formalisée en une structures de \emph{Kripe} 
46  \end{itemize}
47 \end{frame}
48
49 \begin{frame}
50  \frametitle{un peu de mathématiques : le Model Checking}
51  \begin{itemize}
52 \item exemple : $ P = 3 \wedge Q = 1 \triangleleft \langle P = 1 \hookleftarrow Q = 0 \rangle$
53 \item la propriété dans aucun état on a $P = 3$ et $Q = 1$  est-elle vraie ? 
54 Pour vérifier cette propriété, on a besoin de connaître l'espace d'états ;
55 \item la propriété : chaque chemin débutant dans un état accessible $P=1$ passe par un état où $Q=3$ et $P=2$ 
56 est-elle vraie ? Cela demande de connaître le graphe d'accessibilité : 
57
58 \item les structures de \emph{Kripe} sont des machines à états étiquetées par les valuations de toutes les variables propositionnelles.
59
60  \end{itemize}
61 \end{frame}
62
63
64
65 \begin{frame}
66  \frametitle{compatibilité Créole : ce qui reste à faire}
67  \begin{itemize}
68 \item tous les options spéciales sont implémentées (auto, fill, obligatoire, \dots)
69 \item tous les états sont implémentés (hidden, disabled, mode (normal/expert), \dots)
70 \item reste la librairie des fonctions pour les variables automatiques
71 \item les "valprec" (valeur précédentes) 
72 \item fixer les comportement des hides (sous-groupes récursifs, \dots)
73 \item validations master/slaves, validations globales (au regard de la configuration entière) éventuellement
74 \end{itemize}
75
76 \end{frame}
77
78