X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/251b65007a909068d3344bd82b7c5ec0ffb0a21a..98c34e4d34d6f63836eefca981f5d1ce73a865e2:/main.tex diff --git a/main.tex b/main.tex index a5fb394..e12726a 100644 --- a/main.tex +++ b/main.tex @@ -113,20 +113,21 @@ \newcommand{\Bool}[0]{\ensuremath{\mathds{B}}} \newcommand{\rel}[0]{\ensuremath{{\mathcal{R}}}} \newcommand{\Gall}[0]{\ensuremath{\mathcal{G}}} -\newcommand{\Sec}[1]{Sect.\,\ref{#1}} -\newcommand{\Fig}[1]{Fig.\,\ref{#1}} -\newcommand{\Alg}[1]{Algorithm~\ref{#1}} -\newcommand{\Tab}[1]{Table~\ref{#1}} +\newcommand{\Sec}[1]{Sect\,\ref{#1}} +\newcommand{\Fig}[1]{{\sc Figure}~\ref{#1}} +\newcommand{\Alg}[1]{Algorithme~\ref{#1}} +\newcommand{\Tab}[1]{Tableau~\ref{#1}} \newcommand{\Equ}[1]{(\ref{#1})} \newcommand{\deriv}{\mathrm{d}} \newcommand{\class}[1]{\ensuremath{\langle #1\rangle}} \newcommand{\dom}[0]{\ensuremath{\textit{dom}}} - + \newcommand{\eqNode}[0]{\ensuremath{{\mathcal{R}}}} \newtheorem{theorem}{Théorème} \newtheorem{lemma}{Lemme} -\newtheorem{xpl}{Exemple} -\newtheorem{Proof}{Preuve} +\newtheorem*{xpl}{Exemple} +\newtheorem*{Proof}{Preuve} +\newtheorem{Def}{Définition} \begin{document} \input{glossaire.tex} @@ -155,6 +156,11 @@ Blabla blabla. \input{sdd} +\chapter{Combinaisons Synchrones et Asynchrones de Systèmes Booléens} +\input{mixage} + + + \chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens}\label{chap:promela} \input{modelchecking} @@ -179,13 +185,18 @@ Blabla blabla. \chapter{Preuves sur les SDD} -\section{Preuve du théorème~\ref{th:Adrien}}\label{anx:sccg} +\section{Théorème~\ref{th:Adrien}}\label{anx:sccg} \input{annexesccg} -\section{Preuve de continuité de $G_f$ dans $(\mathcal{X},d)$}\label{anx:cont} +\section{Continuité de $G_f$ dans $(\mathcal{X},d)$}\label{anx:cont} \input{annexecontinuite.tex} -\section{Preuve de Correction et de complétude de l'approche de vérification de convergence à l'aide de SPIN}\label{anx:promela} + +\section{Convergence du mode mixe}\label{anx:mix} +\input{annexePreuveMixage} + + +\section{Correction et complétude de la vérification de convergence par SPIN}\label{anx:promela} \input{annexePromelaProof} \backmatter