list is Multi now which enables us to implement item access
[tiramisu.git] / doc / eole-report / presentation / statut.tex
1
2 \begin{frame}
3  \frametitle{Etats ("status") de la configuration}
4  \begin{itemize}
5   \item système d'états de la configuration par \emph{droits d'accès} ;
6   \item \texttt{read write}, \texttt{read only} ;
7   \item correspond à \texttt{freeze}, \texttt{hidden}, \texttt{disabled} \dots ;
8   \item \texttt{doc/status.html} ;
9   \item \texttt{eole-report/D03ReglesEtats.pdf} ;
10  \end{itemize}
11 \end{frame}
12
13 \begin{frame}
14  \frametitle{hidden if in, hidden if not in}
15  \begin{itemize}
16  \item les hidden if in, disabled if, \dots sont généralisés
17  \item dans tiramisu, ce sont des pré-requis sur une (des) variables
18  \item \texttt{eole-report/D03ReglesEtats.pdf}
19  \item \texttt{doc/consistency.html}
20  \end{itemize}
21 \end{frame}
22
23 \begin{frame}
24  \frametitle{un peu de mathématiques : prévenir les deadlocks}
25  \begin{itemize}
26 \item sûreté : prévention des deadlocks ; 
27 \item dans tiramisu, le modèle est suffisamment abstrait pour que son exploitation mathématique soit 
28 réalisable par les techniques de \emph{Model Checking} ; 
29 \item soit on a besoin de ne connaître que l'ensemble des états, pas leurs liens $\Rightarrow$ espace d'états ; 
30 \item soit on a besoin de connaître toutes les relations $\Rightarrow$ graphe d'accessibilité ; 
31 \item la configuration est modélisable en une structure de \emph{Kripe} ;
32 \item déjà le parsing de la conf est facile, la preuve : \texttt{tiramisu/report/build/index.html}
33  \end{itemize}
34 \end{frame}
35
36 \begin{frame}
37  \frametitle{un peu de mathématiques (suite) CreoleLint}
38  \begin{itemize}
39 \item exemple : $ P = 3 \wedge Q = 1 \triangleleft \langle P = 1 \hookleftarrow Q = 0 \rangle$
40 \item la propriété \og dans aucun état on a $P = 3$ et $Q = 1$  \fg~ est-elle vraie ? 
41 Pour vérifier cette propriété, on a besoin de connaître l'espace d'états ;
42 \item la propriété \og chaque chemin débutant dans un état accessible $P=1$ passe par un état où $Q=3$ et $P=2$ \fg~  
43 est-elle vraie ? Cela demande de connaître le graphe d'accessibilité ; 
44 \item les structures de \emph{Kripe} sont des machines à états étiquetées par les valuations de toutes les variables propositionnelles ;
45 \item une compliation statique devient possible dans \emph{CreoleLint} \dots
46  \end{itemize}
47 \end{frame}
48
49 \begin{frame}
50  \frametitle{compatibilité Créole : ce qui reste à faire}
51  \begin{itemize}
52 \item les options spéciales sont implémentées (auto, fill, obligatoire, \dots) reste la librairie des fonctions pour les variables automatiques \texttt{eosfunc} ;
53 \item tous les états sont implémentés (hidden, disabled, mode (normal/expert), \dots), il faut fixer les comportement \texttt{read write} ; 
54 \item les "valprec" (valeur précédentes) et une mémoire de \emph{tous} les états antérieurs ; 
55 \item fixer les comportement des hides (sous-groupes récursifs, \dots) ;
56 \item validations master/slaves, validations globales au regard de la configuration entière puisque c'est possible maintenant.
57 \end{itemize}
58
59 \end{frame}
60
61