62 lines
2.9 KiB
TeX
62 lines
2.9 KiB
TeX
|
|
||
|
|
\begin{frame}
|
||
|
|
\frametitle{Etats ("status") de la configuration}
|
||
|
|
\begin{itemize}
|
||
|
|
\item système d'états de la configuration par \emph{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}
|
||
|
|
\end{frame}
|
||
|
|
|
||
|
|
\begin{frame}
|
||
|
|
\frametitle{un peu de mathématiques : prévenir les deadlocks}
|
||
|
|
\begin{itemize}
|
||
|
|
\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} ;
|
||
|
|
\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 est modélisable en une structure de \emph{Kripe} ;
|
||
|
|
\item déjà le parsing de la conf est facile, la preuve : \texttt{tiramisu/report/build/index.html}
|
||
|
|
\end{itemize}
|
||
|
|
\end{frame}
|
||
|
|
|
||
|
|
\begin{frame}
|
||
|
|
\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é \og dans aucun état on a $P = 3$ et $Q = 1$ \fg~ est-elle vraie ?
|
||
|
|
Pour vérifier cette propriété, on a besoin de connaître l'espace d'états ;
|
||
|
|
\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~
|
||
|
|
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}
|
||
|
|
|
||
|
|
\begin{frame}
|
||
|
|
\frametitle{compatibilité Créole : ce qui reste à faire}
|
||
|
|
\begin{itemize}
|
||
|
|
\item les options spéciales sont implémentées (auto, fill, obligatoire, \dots) reste la librairie des fonctions pour les variables automatiques \texttt{eosfunc} ;
|
||
|
|
\item tous les états sont implémentés (hidden, disabled, mode (normal/expert), \dots), il faut fixer les comportement \texttt{read write} ;
|
||
|
|
\item les "valprec" (valeur précédentes) et une mémoire de \emph{tous} les états antérieurs ;
|
||
|
|
\item fixer les comportement des hides (sous-groupes récursifs, \dots) ;
|
||
|
|
\item validations master/slaves, validations globales au regard de la configuration entière puisque c'est possible maintenant.
|
||
|
|
\end{itemize}
|
||
|
|
|
||
|
|
\end{frame}
|
||
|
|
|
||
|
|
|