X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/f4dd79b2c3181cb26ec94555b62ed77dcb0a4200..2b04820abccb0772b10b2c53542ecddc6a6f600c:/main.tex diff --git a/main.tex b/main.tex index 5e94a3c..c16595e 100644 --- a/main.tex +++ b/main.tex @@ -11,18 +11,16 @@ \documentclass[french]{spimufchdr} \usepackage{dsfont} -\usepackage{glossaries} \usepackage{graphicx} \usepackage{listings} -\usepackage{verbatim} - -% The TeX code is entering with UTF8 -% character encoding (Linux and MacOS standards) +%\usepackage[font=footnotesize]{subfig} \usepackage[utf8]{inputenc} +\usepackage{thmtools, thm-restate} +%\declaretheorem{theorem} %%-------------------- %% Search path for pictures -%\graphicspath{{path1/},{path2/}} +\graphicspath{{images/},{path2/}} %%-------------------- %% Definition of the bibliography entries @@ -121,21 +119,15 @@ \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*{Proof}{Preuve} +\newtheorem{Def}{Définition} \begin{document} -\input{glossaire.tex} - -% \chapter*{Remerciements} - -% Blabla blabla. - -% \tableofcontents @@ -150,22 +142,29 @@ Blabla blabla. \part{Système Booléens} \chapter{Iterations discrètes de Systèmes Dynamiques booléens} - -\JFC{Chapeau chapitre à faire} +\section{Formalisation} \input{sdd} -\chapter{Combinaisons Synchrones et Asynchrones de Systèmes Booléens} +\section{Combinaisons synchrones et asynchrones} \input{mixage} +\section{Conclusion} +Introduire de l'asynchronisme peut permettre de réduire le temps +d'exécution global, mais peut aussi introduire de la divergence. +Dans ce chapitre, nous avons exposé comment construire un mode combinant les +avantage du synchronisme en terme de convergence avec les avantages +de l'asynchronisme en terme de vitesse de convergence. + + + \chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens}\label{chap:promela} \input{modelchecking} - \JFC{Mixage} @@ -184,13 +183,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