tiramisu/doc/eole-report/presentation/statut.tex

79 lines
3.2 KiB
TeX
Raw Normal View History

2012-05-13 20:48:51 +02:00
\begin{frame}
\frametitle{Organisation en espace de nommage}
\begin{itemize}
\item dans \emph{tiramisu} l'accent est mis sur l'organisation arborescente des données ;
\item la validation des options de configuration se fait par l'appartenance aux groupes (families, master/slaves \dots) ;
\item l'organisation en groupes est unifiée par l'espace de nommage ;
\item la lisibilité de l'API excellente, contrairement à \emph{Creole}
\item \texttt{eole-report/D03ReglesEtats.pdf}
\item lisibilité d'une config : \texttt{tiramisu/report/build/index.html} rapport html d'une config
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{Etats de la configuration}
\begin{itemize}
\item système d'états de la configuration par droits d'accès
\item \texttt{read write}, \texttt{read only};
\item correspond à \texttt{freeze}, \texttt{hidden}, \texttt{disabled} \dots ;
\item \texttt{doc/status.html}
\item \texttt{eole-report/D03ReglesEtats.pdf}
\end{itemize}
\end{frame}
\begin{frame}
\frametitle{hidden if in, hidden if not in}
\begin{itemize}
\item les hidden if in, disabled if, \dots sont généralisés
\item dans tiramisu, ce sont des pré-requis sur une (des) variables
\item \texttt{eole-report/D03ReglesEtats.pdf}
\item \texttt{doc/consistency.html}
\end{itemize}
2012-06-12 23:05:08 +02:00
\end{frame}
2012-05-13 20:48:51 +02:00
2012-06-12 23:05:08 +02:00
\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}
2012-05-13 20:48:51 +02:00
\end{frame}
2012-06-12 23:05:08 +02:00
\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}
2012-05-13 20:48:51 +02:00
\begin{frame}
\frametitle{compatibilité Créole : ce qui reste à faire}
\begin{itemize}
\item tous les options spéciales sont implémentées (auto, fill, obligatoire, \dots)
\item tous les états sont implémentés (hidden, disabled, mode (normal/expert), \dots)
\item reste la librairie des fonctions pour les variables automatiques
\item les "valprec" (valeur précédentes)
\item fixer les comportement des hides (sous-groupes récursifs, \dots)
\item validations master/slaves, validations globales (au regard de la configuration entière) éventuellement
\end{itemize}
\end{frame}