\documentclass[a4paper]{book}
\usepackage{fullpage}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[francais]{babel}

\usepackage{latexsym}
\usepackage{fancyhdr}
\usepackage{makeidx}
\usepackage{graphics}
\usepackage{graphicx}
\usepackage{longtable}
\usepackage{moreverb}
\usepackage{listings}

\newcommand{\altarica}{{\sc AltaRica}}

\begin{document}

\title{Master 1, Conceptions Formelles\\
Projet du module \altarica\\
Synthèse (assistée) d'un contrôleur du niveau d'une cuve}

\date{}

\author{Nom1 \and Nom2 \and Nom3}

\maketitle

\chapter{Le sujet}
\input{tank}

\chapter{Le rapport}
Le rapport est sur 20 points.

\section{Processus} \subsection{Rôle du fichier {\tt GNUmakefile} (1.5 points)}
% A COMPLETER en expliquant les enchainements des calculs effectués.

\paragraph{Le fichier GNUMakeFile} sert à compiler les différents éléments du
projet via la commande \textit{make}. La cible \textit{\$(MODEL).time} est la
plus interresante~: elle utilise trois paramètres afin de contruite les
différents calculs. Cest éléments sont utilisés dans l'ordre défini dans la
liste ci-dessous dans des boucles \texttt{for} imbriquées

\begin{enumerate}
    \item les controlleurs à partir desquel construire les modèles -
        \texttt{Crtl} et \texttt{CtrlVV}
    \item les nombres de pannes - de 0 à 3
    \item l'itération - de 1 à 5 
\end{enumerate}

Une fois effectués, les résultats de chaque calcul sont exportées dans le répertoire
\texttt{LaTeX} afin d'étre \textbf{inclus dans ce rapport}.

\subsection{Rôle de la constante {\tt nbFailures} et de l'assertion associée (0.5 point)}
% A COMPLETER en expliquant le rôle de la constante.

\paragraph{nbFailure} détermine le nimbre maximal de panne pouvans intervenir en
même temps sur les valves de notre système. Cette variable est définie à partir
de \texttt{NbPannes} qui elle même est définie dynamiquement dans notre
\textit{Makefile} (cible \textit{\$(MODEL).time}).

\paragraph{} Cette constante est utilisés dans l'assertion \texttt{nbFailures >=
(V[0].stucked + V[1].stucked + V[2].stucked);} afin de s'assurer que le nombre
de pannes sur le modèle (\texttt{V[x].stucked}) ne dépasse pas le nombre de
panne définis dans \texttt{nbFailures}.

\section{Résultats avec le contrôleur initial {\tt Ctrl}}
\subsection{Calcul d'un contrôleur}
\subsubsection{Avec 0 défaillance (0.5 point)}
\input{LaTeX/System0FCtrl.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\paragraph{} Lors de la premiere itération, avec un controleur initial
\textit{Ctrl} et sans défaillance, nous n'avons pas de situation de
\textit{deadlock}. Nous pouvons attendre 86 état de \textbf{niveau critiques} et
autant de \textbf{situation redoutée} pour un total de 247 états atteignables. 
Côté transitions, le système en comporte 3474 dont un tier environ mène à
des coups gagnant.

\paragraph{}lors de la seconde itération, nous obtenons 97 états et toujours
aucun \textit{deadlock}. Nous ne constatons plus de \textbf{niveau critique} ni
de \textbf{situation redoutée}. Côté transitions, environ \textbf{83\%} mène à
des coups gagnants, mais nous en avons aussi près de 4 fois moins par rapport à
l'itération précédente.

Les itérations suivantes n'entrainent pas de modification sur le contrôleurs. 
Nous pouvons donc dire que qu'il est correct.

Nous observons aussi que les état \texttt{out1}, \texttt{out2} et \texttt{out3}
sont atteinds dans toutes les itérations, ce qui montre que la vanne de sortie
fonctionne dans ses trois configurations: ouverte, semi-ouverte et fermée.

\subsubsection{Avec 1 défaillance (0.5 point)}
\input{LaTeX/System1FCtrl.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsubsection{Avec 2 défaillances (0.5 point)}
\input{LaTeX/System2FCtrl.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsubsection{Avec 3 défaillances (0.5 point)} \input{LaTeX/System3FCtrl.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsection{Bilan avec le contrôleur initial (1 point)}
% A COMPLETER

\section{Construction d'un contrôleur initial plus performant}
\subsection{Rôle du composant {\tt ValveVirtual}(2 points)}
\includegraphics[height=.2\textheight,width=.5\textwidth]{Graphs/Valve-modes.pdf}
\includegraphics[height=.2\textheight,width=.5\textwidth]{Graphs/ValveVirtual-modes.pdf}
% A COMPLETER en expliquant sa sémantique et son rôle.

\subsection{Rôle du composant {\tt CtrlVV} (4 points)}
% A COMPLETER en expliquant les mécanismes mis en oeuvre, leurs rôles et les avantages de ce contrôleur par rapport au précédent CtrlVV.

\section{Résultats avec le contrôleur {\tt CtrlVV}}
\subsection{Calcul d'un contrôleur}
\subsubsection{Avec 0 défaillance (0.5 point)}
\input{LaTeX/System0FCtrlVV.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsubsection{Avec 1 défaillance (0.5 point)}
\input{LaTeX/System1FCtrlVV.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsubsection{Avec 2 défaillances (0.5 point)}
\input{LaTeX/System2FCtrlVV.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsubsection{Avec 3 défaillances (0.5 point)}
\input{LaTeX/System3FCtrlVV.tex}
\paragraph{Interprétation des résultats}
% A COMPLETER

\subsection{Bilan avec le contrôleur CtrlVV (1 point)}
% A COMPLETER

\section{Une première optimisation des contrôleurs pour améliorer le débit aval}
\subsection{Une optimisation basée sur les priorités (1 point)}
\small{\lstinputlisting{ControleursOpt/Optimisation.alt}}
% A COMPLETER en expliquant en quoi consiste l'optimisation mise en place.

\subsection{Calcul des contrôleurs optimisés avec {\tt CtrlVV}}
\paragraph{Avec 0 défaillance}\ \\
\input{LaTeX/System0FCtrlVV_opt.tex}

\paragraph{Avec 1 défaillance}\ \\
\input{LaTeX/System1FCtrlVV_opt.tex}

\paragraph{Avec 2 défaillances}\ \\
\input{LaTeX/System2FCtrlVV_opt.tex}

\paragraph{Avec 3 défaillances}\ \\
\input{LaTeX/System3FCtrlVV_opt.tex}

\subsection{Bilan avec la première optimisation du contrôleur CtrlVV (1 point)}
% A COMPLETER

\section{Une deuxième optimisation (3 points)}
Il est possible d'obtenir de meilleurs résultats que les précédents par au moins deux façons.
\begin{enumerate}
\item En utilisant un meilleur ordre pour les priorités entre événements.
\item En introduisant cet objectif dans le système de calcul de point fixe des actions du contrôleur.
\end{enumerate}

Vous devez proposer une des deux optimisations conduisant à une solution dans laquelle le débit de la vanne aval est le moins souvent possible décrémenter, voire jamais. Pour cela, vous pouvez~:
\begin{itemize}
\item Meilleur ordre sur les événements.
  \begin{enumerate}
  \item Modifier le fichier \texttt{ControleursOpt/Optimisation.alt}.
  \item Faites \texttt{make}.
  \item Quand vos résultats sont satisfaisants, notez les, puis copiez votre fichier dans \texttt{ControleursOpt/Optimisation-2.alt}.
  \item Remettez le fichier \texttt{ControleursOpt/Optimisation.alt} d'origine.
  \item Faites \texttt{make}.
  \end{enumerate}
\item Meilleur système d'équations au point fixe.
  \begin{enumerate}
  \item Modifier le fichier \texttt{Spec/System.spe}.
  \item Faites \texttt{make}.
  \item Quand vos résultats sont satisfaisants, notez les, puis copiez votre fichier dans \texttt{Spec/System-2.spe}.
  \item Remettez le fichier \texttt{Spec/System.spe} d'origine.
  \item Faites \texttt{make}.
  \end{enumerate}
\end{itemize}

\paragraph{Le nouvel ordre}\ \\
\small{\lstinputlisting{ControleursOpt/Optimisation-2.alt}
% A COMPLETER en décrivant les résultats obtenus

\paragraph{Le nouveau système d'équations}\ \\
\small{\lstinputlisting[texcl]{Spec/System-2.spe}}
% A COMPLETER en décrivant les résultats obtenus

\section{Conclusion sur la synthèse de contrôleur (1 point)}
% A COMPLETER

\end{document}