From: couchot Date: Tue, 24 Jun 2014 14:28:32 +0000 (+0200) Subject: un paquet d'ajouts X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/commitdiff_plain/1b923f193392e3ce847882c24a128eff4bee9992?ds=inline;hp=--cc un paquet d'ajouts --- 1b923f193392e3ce847882c24a128eff4bee9992 diff --git a/Gi.dot b/Gi.dot new file mode 100644 index 0000000..cf9e416 --- /dev/null +++ b/Gi.dot @@ -0,0 +1,9 @@ +digraph { +1 -> 1 [label=" -"] +1 -> 4 [label=" +-"] +2 -> 2 [label=" -"] +2 -> 4 [label=" +-"] +3 -> 3 [label=" -"] +3 -> 4 [label=" +-"] +4 -> 4 [label=" +-"] +} \ No newline at end of file diff --git a/Gi.pdf b/Gi.pdf new file mode 100644 index 0000000..22af9dc Binary files /dev/null and b/Gi.pdf differ diff --git a/Makefile b/Makefile new file mode 100755 index 0000000..7e5377b --- /dev/null +++ b/Makefile @@ -0,0 +1,49 @@ +MAIN = main +SOURCES = $(MAIN).tex abstract.tex intro.tex ddn.tex xpl.tex promela.tex translation.tex proof.tex complexity.tex exp.tex conclusion.tex abbrev.bib biblioand.bib +LOG=logLatex + +pdf: $(MAIN).pdf + +$(MAIN).pdf: $(SOURCES) + @printf "***** Compilation 1 *****\n" + @pdflatex $(MAIN) > $(LOG) + @printf "***** Biblio *****\n" + @bibtex $(MAIN) >> $(LOG) + @printf "***** Compilation 2 *****\n" + @pdflatex $(MAIN) >> $(LOG) + @printf "***** Compilation 3 *****\n" + @pdflatex $(MAIN) >> $(LOG) + +all: + latex $(MAIN).tex > $(LOG) + latex $(MAIN).tex >> $(LOG) + bibtex $(MAIN) >> $(LOG) + latex $(MAIN).tex >> $(LOG) + dvips -t a4 $(MAIN).dvi -o >> $(LOG) + ps2pdf $(MAIN).ps >> $(LOG) + +fast: + latex $(MAIN).tex > $(LOG) + dvips -t a4 $(MAIN).dvi -o >> $(LOG) + ps2pdf $(MAIN).ps >> $(LOG) + +test: + acroread $(MAIN).pdf + +testr: + kghostview $(MAIN).ps + +clean: + rm -rf *~ *.aux *.log *.bbl *.blg *.dvi *.bak *.thm *.lof *.loe *.lot *.out *.toc + + +# construit l'archive toute prete (pour Springer) +TEXSOURCES = main.tex ddn.tex +PACKAGES = mathpartir.sty synttree.sty bcprules.sty arydshln.sty +CLSSTY = llncs.cls llncsdoc.sty splncs.bst sprmindx.sty +UTIL = Makefile copyright.pdf CL07-CameraReady.pdf readme +FILES = $(TEXSOURCES) $(PACKAGES) $(CLSSTY) $(UTIL) + +arch: + zip Archive.zip $(FILES) + diff --git a/Suite_logistique_390_100.png b/Suite_logistique_390_100.png new file mode 100644 index 0000000..2e3dc12 Binary files /dev/null and b/Suite_logistique_390_100.png differ diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex new file mode 100644 index 0000000..8c95761 --- /dev/null +++ b/annexePromelaProof.tex @@ -0,0 +1,2 @@ +\JFC{Voir section~\ref{sec:spin:proof}} + diff --git a/annexecontinuite.tex b/annexecontinuite.tex new file mode 100644 index 0000000..85cbd4c --- /dev/null +++ b/annexecontinuite.tex @@ -0,0 +1,48 @@ +Montrons que pour toute fonction booléenne +$f$ de $\Bool^n$ dans lui même, $G_f$ est continue sur $(\mathcal{X},d)$. + +Soit donc $(s_t,x^t)^{t \in \Nats}$ une suite de points de +l'espace $\mathcal{X}$ qui converge vers $(s,x)$. +Montrons que $(G_f (s_t,x^t))^{t \in \Nats}$ converge vers $G_f (s,x)$. + +La distance $d((s_t,x^t), (s,x))$ tend vers 0. +Il en est donc de même pour $d_H(x^t, x)$ et $d_S(s_t, s)$. +Or, $d_H(x^t, x)$ ne prend que des valeurs entières. +Cette distance est donc nulle à partir d'un certain $t_0$. +Ainsi, à partir de $t>t_0$, on a $x^t = x$ . +De plus, $d_S(s_t, s)$ tend vers $0$ donc $d_S(s_t, s) < 10^{-1}$ +à partir d'un certain rang $t_1$. +Ainsi, à partir de $t>t_1$, les suites $(s_t)_{t \in \Nats}$ +ont toutes le même premier terme, qui est celui +de $s$ pour $t$ supérieur à $t_1$. +Pour $t > \max(t_0,t_1)$, les configurations $x^t$ et $x$ +sont les mêmes, +et les stratégies $s_t$ et $s$ ont le même premier terme +($s_0^t = s_0$), donc les configurations +de $F_f(s_0^t,x^t)$ et de $F_f (s_0,x)$ sont égales et donc la distance +entre $G_f(s_t,x^t)$ et $G_f (s,x)$ est inférieure à 1. + +Montrons maintenant que la distance entre +$G_f (s_t,x^t)$ et $G_f (s,x)$ +tend bien vers 0 quand $t$ tend vers $+\infty$. Soit $\epsilon > 0$. +\begin{itemize} + \item Si $\epsilon \ge 1$. Comme la distance $d(G_f(s_t,x^t), G_f (s,x))<1$ + pour $t > \max(t_0, t_1)$, alors + $d(G_f(s_t,x^t), G_f (s,x))<\epsilon$ + \item Si $\epsilon < 1$, alors $\exists k \in \Nats \textrm{ tel que } + 10^{-k} > \epsilon > 10^{-(k+1)}$. + Comme $d_S(s_t, s)$ tend vers 0, il existe +un rang $t_2$ à partir duquel +$\forall t > t_2 , d_S(s_t, s) < 10^{-(k+2)}$: +à partir de ce rang, les $k+2$ premiers termes de $s_t$ sont ceux de $s$. +Donc les $k + 1$ premiers termes des stratégies de +$G_f (s_t,x^t)$ et de +$G_f (s,x)$ sont les mêmes (puisque $G_f$ +opère un décalage sur les stratégies), et vue la +définition de $d_S$, la partie décimale de la distance entre les points +$(s_t,x^t)$ et $(s,x)$ est +inférieure à $10^{-(k+1)} \le \epsilon$. +\end{itemize} +Pour conclure, pour tout $\epsilon > 0$, +$\exists~T_0 = \max(t_0, t_1, t_2) \in \Nats \textrm{ tel que } +\forall t > T_0 , d (Gf (s_t,x^t),G_f (s,x))< \epsilon$. diff --git a/annexesccg.tex b/annexesccg.tex new file mode 100644 index 0000000..3db4320 --- /dev/null +++ b/annexesccg.tex @@ -0,0 +1,126 @@ +Soit $\alpha\in\Bool$. +On nomme $f^{\alpha}$ la fonction de $\Bool^{n-1}$ +dans lui-même définie pour +chaque $x\in\Bool^{n-1}$ par +\[ +f^{\alpha}(x)=(f_1(x,\alpha),\dots,f_{n-1}(x,\alpha)). +\] +On nomme $\Gamma(f)^\alpha$ le sous-graphe +de $\Gamma(f)$ engendré par le sous-ensemble +$\Bool^{n-1} \times \{\alpha\}$ de $\Bool^n$. + + + + +Énonçons et prouvons tout d'abord les lemmes techniques suivants: + +\begin{lemma}\label{lemma:subgraph} +$G(f^\alpha)$ est un sous-graphe de $G(f)$: chaque arc de $G(f^\alpha)$ est +un arc de $G(f)$. De plus si $G(f)$ n'a pas d'arc de $n$ vers un autre +sommet $i\neq n$, alors on déduit +$G(f^\alpha)$ de $G(f)$ en supprimant le sommet $n$ ainsi que tous les +arcs dont $n$ est soit l'extrémité, soit l'origine (et dans ce dernier +cas, les arcs sont des boucles sur $n$). +\end{lemma} + +\begin{Proof} +Supposons que $G(f^{\alpha})$ possède un arc de $j$ vers $i$ de signe +$s$. Par définition, il existe un sommet $x\in\Bool^{n-1}$ tel que +$f^{\alpha}_{ij}(x)=s$, et puisque +$f^{\alpha}_{ij}(x)=f_{ij}(x,\alpha)$, on en déduit que $G(f)$ possède un arc +de $j$ à $i$ de signe $s$. Ceci prouve la première assertion. +Pour démontrer la seconde, il suffit de prouver que si +$G(f)$ a un arc de $j$ vers $i$ de signe $s$, avec $i,j\neq n$, alors +$G(f^\alpha)$ contient aussi cet arc. Ainsi, supposons que $G(f)$ a un +arc de $j$ vers $i$ de signe $s$, avec $i,j\neq n$. +Alors, il existe +$x\in\Bool^{n-1}$ et $\beta\in\Bool$ tels que +$f_{ij}(x,\beta)=s$. Si $f_{ij}(x,\beta)\neq f_{ij}(x,\alpha)$, alors +$f_i$ dépend du $n^{\textrm{ème}}$ composant, ce qui est en contradiction +avec les hypothèses. +Ainsi $f_{ij}(x,\alpha)$ est égal à $s$. +On a donc aussi +$f^{\alpha}_{ij}(x)=s$. Ainsi $G(f^\alpha)$ possède un arc +arc de $j$ vers $i$ de signe $s$. +\end{Proof} + +\begin{lemma}\label{lemma:iso} +Les graphes $\Gamma(f^\alpha)$ et $\Gamma(f)^\alpha$ sont isomorphes. +\end{lemma} + +\begin{Proof} +Soit $h$ la bijection de $\Bool^{n-1}$ vers +$\Bool^{n-1}\times \{\alpha\}$ définie par $h(x)=(x,\alpha)$ pour chaque +$x\in\Bool^{n-1}$. +On voit facilement que $h$ permet de définir un isomorphisme +entre $\Gamma(f^\alpha)$ et $\Gamma(f)^\alpha$: +$\Gamma(f^\alpha)$ possède un arc de $x$ vers $y$ si et seulement si +$\Gamma(f)^\alpha$ a un arc de $h(x)$ vers $h(y)$. +\end{Proof} + + +\begin{Proof} +du Théorème~\ref{th:Adrien}. +La preuve se fait par induction sur $n$. +Soit $f$ une fonction de $\Bool^n$ dans lui-même et qui vérifie les hypothèses +du théorème. +Si $n=1$ la démonstration est élémentaire: +en raison du troisième point du théorème, $G(f)$ a une boucle négative; +ainsi $f(x)=\overline{x}$ et $\Gamma(f)$ est un cycle de longueur 2. +On suppose donc que $n>1$ et que le théorème est valide pour toutes les +fonctions de $\Bool^{n-1}$ dans lui-même. +En raison du premier point du théorème, $G(f)$ +contient au moins un sommet $i$ tel qu'il n'existe pas dans $G(f)$ +d'arc de $i$ vers un autre sommet $j\neq i$. +Sans perte de généralité, on peut considérer que +ce sommet est $n$. +Alors, d'après le lemme~\ref{lemma:subgraph}, +$f^0$ et $f^1$ vérifient les conditions de l'hypothèse. +Alors, par hypothèse d'induction $\Gamma(f^0)$ et +$\Gamma(f^1)$ sont fortement connexes. +Ainsi, d'après le lemme~\ref{lemma:iso}, +$\Gamma(f)^0$ et $\Gamma(f)^1$ sont fortement +connexes. +Pour prouver que $\Gamma(f)$ est fortement connexe, il suffit +de prouver que $\Gamma(f)$ contient un arc $x\to y$ avec +$x_n=0y_n$. +En d'autres mots, il suffit de prouver que: +\begin{equation}\tag{$*$} +\forall \alpha\in\Bool,~\exists x\in\Bool^n,\qquad x_n=\alpha\neq f_n(x). +\end{equation} + +On suppose tout d'abord que $n$ a une boucle +négative. +Alors, d'après la définition de +$G(f)$, il existe $x\in\Bool^n$ tel que $f_{nn}(x)<0$. +Ainsi si $x_n=0$, on a $f_n(x)>f_n(\overline{x}^n)$, et donc +$x_n=0\neq f_n(x)$ et +$\overline{x}^n_n=1\neq f_n(\overline{x}^n)$; +et si $x_n=1$, on a +$f_n(x) 00 + 00 -> 10 + 01 -> 00 + 01 -> 11 + 10 -> 11 + 10 -> 00 + 11 -> 10 + 11 -> 01 +} diff --git a/g.pdf b/g.pdf new file mode 100644 index 0000000..4f69e01 Binary files /dev/null and b/g.pdf differ diff --git a/glossaire.tex b/glossaire.tex new file mode 100644 index 0000000..4932ec2 --- /dev/null +++ b/glossaire.tex @@ -0,0 +1,92 @@ +\newglossaryentry{graphoriente}{name=graphe orienté, description={ +Un graphe orienté $G=(S,A)$ +est défini par la donnée d'un ensemble de sommets $S$ et +d'un ensemble d'arcs $A$, +chaque arc étant représenté par un couple de sommets. +Si $x$ et $y$ sont des sommets de $S$, +le couple $(x,y)$ représente l'arc orienté allant du sommet \emph{origine} +$x$ au sommet \emph{extremité} $y$.}} + +\newglossaryentry{graphfortementconnexe}{name=graphe fortement connexe, description={ +Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout +couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ +et $y$ à $x$.} +} + + +\newglossaryentry{distributionuniforme}{name=distribution uniforme, description={Les lois de distribution uniforme (ou loi uniformes continues) +forment une famille de lois à densité caractérisées par la propriété suivante: +tous les intervalles de même longueur inclus dans le support de la loi ont +la même probabilité.} +} + + +\newglossaryentry{partieentiere}{name=partie entière, description= +{La partie entière d'un nombre réel est l'entier qui lui est immédiatement + inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor$. +}, +symbol={\ensuremath{\lfloor x \rfloor}} +} + + +\newglossaryentry{distanceHamming}{name=distance de Hamming, description= +{La distance de Hamming entre deux éléments $x=(x_1,\ldots,x_n)$ et +$y=(y_1,\ldots,y_n)$ dans $\Bool^n$ +est le nombre d'indices $i$, $1 \le i \le n$ tels que +$x_i$ diffère de $y_i$. +}} + + + +\newglossaryentry{decalageDeBits}{name=décalage de bits, +plural=décalages de bits, +description={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. +Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) +est obtenu en +décalant les bits de $x$ de $b$ bits vers la gauche +(resp. vers la droite) et +en complétant avec des zéros à droite (resp. à gauche). +}} + + + +\newglossaryentry{chaineDeMarkov}{name=chaîne de Markov, +plural=chaînes de Markov, description={ +On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci +désigne une suite de variables aléatoires $(X_n)_{n \in \Nats}$ +à temps discret, à espace d'états discret, sans mémoire et +dont le mécanisme de transition ne change pas au cours du temps. +Formellement la propriété suivante doit être établie:\newline +$ +%\begin{array}{l} +\forall n \ge 0, \forall (i_0, \ldots, i_{n-1}, i,j),\\ +\textrm{ }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots, X_{n-1}=i_{n-1}, X_{n}=i) \\ +\textrm{ }= P(X_{1}=j\mid X_n=i). +%\end{array} +$ +}} + + +\newglossaryentry{vecteurDeProbabilite}{name=vecteur de probabilités, +plural=vecteurs de probabilités, description={ +Un vecteur de probabilités est un vecteur tel que toutes ses composantes +sont positives ou nulles et leur somme vaut 1.}} + +\newglossaryentry{matriceDAdjacence}{name=matrice d'adjacence, description={ +La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets +est la matrice $\check{M}$ de dimension $n \times n$ +dont l'élément $\check{M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.}} + + +\newglossaryentry{xor}{name=ou exclusif, description= +{La fonction \og ou exclusif\fg{}, XOR, est l'opérateur de $\Bool^2$ dans +$\Bool$ qui prend la valeur 1 si seulement +si les deux opérandes ont des valeurs distinctes.}, +symbol={\ensuremath{\oplus}} +} + +\newglossaryentry{matriceDeTransitions}{name=matrice de transitions, description= +{ + Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition + de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ + est la matrice de transitions associée à la chaine de Markov $X$.}} \ No newline at end of file diff --git a/gp.dot b/gp.dot new file mode 100644 index 0000000..161e9d2 --- /dev/null +++ b/gp.dot @@ -0,0 +1,5 @@ +digraph{ + 1 -> 1 [label=" -"] + 1 -> 2 [label=" +"] + 2 -> 2 [label=" -"] +} \ No newline at end of file diff --git a/gp.pdf b/gp.pdf new file mode 100644 index 0000000..0a99b1f Binary files /dev/null and b/gp.pdf differ diff --git a/h.dot b/h.dot new file mode 100644 index 0000000..b23b196 --- /dev/null +++ b/h.dot @@ -0,0 +1,10 @@ +digraph { + 00 -> 00 + 00 -> 10 + 01 -> 11 + 01 -> 01 + 10 -> 11 + 10 -> 00 + 11 -> 10 + 11 -> 01 +} diff --git a/h.pdf b/h.pdf new file mode 100644 index 0000000..df4d68b Binary files /dev/null and b/h.pdf differ diff --git a/hp.dot b/hp.dot new file mode 100644 index 0000000..a8145cf --- /dev/null +++ b/hp.dot @@ -0,0 +1,5 @@ +digraph{ + 1 -> 1 [label=" -"] + 1 -> 2 [label=" +-"] + 2 -> 2 [label=" +-"] +} \ No newline at end of file diff --git a/hp.pdf b/hp.pdf new file mode 100644 index 0000000..d474682 Binary files /dev/null and b/hp.pdf differ diff --git a/images/Gi.dot b/images/Gi.dot new file mode 100644 index 0000000..cf9e416 --- /dev/null +++ b/images/Gi.dot @@ -0,0 +1,9 @@ +digraph { +1 -> 1 [label=" -"] +1 -> 4 [label=" +-"] +2 -> 2 [label=" -"] +2 -> 4 [label=" +-"] +3 -> 3 [label=" -"] +3 -> 4 [label=" +-"] +4 -> 4 [label=" +-"] +} \ No newline at end of file diff --git a/images/Gi.pdf b/images/Gi.pdf new file mode 100644 index 0000000..22af9dc Binary files /dev/null and b/images/Gi.pdf differ diff --git a/images/Suite_logistique_390_100.png b/images/Suite_logistique_390_100.png new file mode 100644 index 0000000..2e3dc12 Binary files /dev/null and b/images/Suite_logistique_390_100.png differ diff --git a/images/g.dot b/images/g.dot new file mode 100644 index 0000000..6f25f41 --- /dev/null +++ b/images/g.dot @@ -0,0 +1,10 @@ +digraph { + 00 -> 00 + 00 -> 10 + 01 -> 00 + 01 -> 11 + 10 -> 11 + 10 -> 00 + 11 -> 10 + 11 -> 01 +} diff --git a/images/g.pdf b/images/g.pdf new file mode 100644 index 0000000..4f69e01 Binary files /dev/null and b/images/g.pdf differ diff --git a/images/gp.dot b/images/gp.dot new file mode 100644 index 0000000..161e9d2 --- /dev/null +++ b/images/gp.dot @@ -0,0 +1,5 @@ +digraph{ + 1 -> 1 [label=" -"] + 1 -> 2 [label=" +"] + 2 -> 2 [label=" -"] +} \ No newline at end of file diff --git a/images/gp.pdf b/images/gp.pdf new file mode 100644 index 0000000..0a99b1f Binary files /dev/null and b/images/gp.pdf differ diff --git a/images/h.dot b/images/h.dot new file mode 100644 index 0000000..b23b196 --- /dev/null +++ b/images/h.dot @@ -0,0 +1,10 @@ +digraph { + 00 -> 00 + 00 -> 10 + 01 -> 11 + 01 -> 01 + 10 -> 11 + 10 -> 00 + 11 -> 10 + 11 -> 01 +} diff --git a/images/h.pdf b/images/h.pdf new file mode 100644 index 0000000..df4d68b Binary files /dev/null and b/images/h.pdf differ diff --git a/images/hp.dot b/images/hp.dot new file mode 100644 index 0000000..a8145cf --- /dev/null +++ b/images/hp.dot @@ -0,0 +1,5 @@ +digraph{ + 1 -> 1 [label=" -"] + 1 -> 2 [label=" +-"] + 2 -> 2 [label=" +-"] +} \ No newline at end of file diff --git a/images/hp.pdf b/images/hp.pdf new file mode 100644 index 0000000..d474682 Binary files /dev/null and b/images/hp.pdf differ diff --git a/images/logistique.png b/images/logistique.png new file mode 100644 index 0000000..88a4288 Binary files /dev/null and b/images/logistique.png differ diff --git a/images/tente.png b/images/tente.png new file mode 100644 index 0000000..d5b6f24 Binary files /dev/null and b/images/tente.png differ diff --git a/images/texput.log b/images/texput.log new file mode 100644 index 0000000..8597ede --- /dev/null +++ b/images/texput.log @@ -0,0 +1,21 @@ +This is pdfTeX, Version 3.1415926-1.40.10 (TeX Live 2009/Debian) (format=pdflatex 2010.9.1) 31 MAR 2011 21:10 +entering extended mode + restricted \write18 enabled. + %&-line parsing enabled. +**main.tex + +! Emergency stop. +<*> main.tex + +End of file on the terminal! + + +Here is how much of TeX's memory you used: + 3 strings out of 495061 + 105 string characters out of 1182622 + 45108 words of memory out of 3000000 + 3282 multiletter control sequences out of 15000+50000 + 3640 words of font info for 14 fonts, out of 3000000 for 9000 + 28 hyphenation exceptions out of 8191 + 0i,0n,0p,1b,6s stack positions out of 5000i,500n,10000p,200000b,50000s +! ==> Fatal error occurred, no output PDF file produced! diff --git a/latexStyle/tex-templates b/latexStyle/tex-templates new file mode 160000 index 0000000..15fc32d --- /dev/null +++ b/latexStyle/tex-templates @@ -0,0 +1 @@ +Subproject commit 15fc32dafcfefd531b8e19721d3e66d22b269b8c diff --git a/logistique.png b/logistique.png new file mode 100644 index 0000000..88a4288 Binary files /dev/null and b/logistique.png differ diff --git a/main.glsdefs b/main.glsdefs new file mode 100644 index 0000000..334ef46 --- /dev/null +++ b/main.glsdefs @@ -0,0 +1,330 @@ +\ifglsentryexists{graphoriente}{}% +{% +\gls@defglossaryentry{graphoriente}% +{% +name={graphe orienté},% +sort={graphe orienté},% +type={main},% +first={graphe orient\IeC {\'e}},% +firstplural={graphe orient\IeC {\'e}s},% +text={graphe orient\IeC {\'e}},% +plural={graphe orient\IeC {\'e}s},% +description={Un graphe orienté $G=(S,A)$ est défini par la donnée d'un ensemble de sommets $S$ et d'un ensemble d'arcs $A$, chaque arc étant représenté par un couple de sommets. Si $x$ et $y$ sont des sommets de $S$, le couple $(x,y)$ représente l'arc orienté allant du sommet \emph {origine} $x$ au sommet \emph {extremité} $y$.},% +descriptionplural={Un graphe orienté $G=(S,A)$ est défini par la donnée d'un ensemble de sommets $S$ et d'un ensemble d'arcs $A$, chaque arc étant représenté par un couple de sommets. Si $x$ et $y$ sont des sommets de $S$, le couple $(x,y)$ représente l'arc orienté allant du sommet \emph {origine} $x$ au sommet \emph {extremité} $y$.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{graphfortementconnexe}{}% +{% +\gls@defglossaryentry{graphfortementconnexe}% +{% +name={graphe fortement connexe},% +sort={graphe fortement connexe},% +type={main},% +first={graphe fortement connexe},% +firstplural={graphe fortement connexes},% +text={graphe fortement connexe},% +plural={graphe fortement connexes},% +description={Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ et $y$ à $x$.},% +descriptionplural={Un graphe orienté $G=(S,A)$ est fortement connexe si pour tout couple de sommets $x$, $y$ de $S$ il existe un chemin reliant $x$ à $y$ et $y$ à $x$.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{distributionuniforme}{}% +{% +\gls@defglossaryentry{distributionuniforme}% +{% +name={distribution uniforme},% +sort={distribution uniforme},% +type={main},% +first={distribution uniforme},% +firstplural={distribution uniformes},% +text={distribution uniforme},% +plural={distribution uniformes},% +description={Les lois de distribution uniforme (ou loi uniformes continues) forment une famille de lois à densité caractérisées par la propriété suivante: tous les intervalles de même longueur inclus dans le support de la loi ont la même probabilité.},% +descriptionplural={Les lois de distribution uniforme (ou loi uniformes continues) forment une famille de lois à densité caractérisées par la propriété suivante: tous les intervalles de même longueur inclus dans le support de la loi ont la même probabilité.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{partieentiere}{}% +{% +\gls@defglossaryentry{partieentiere}% +{% +name={partie entière},% +sort={partie entière},% +type={main},% +first={partie enti\IeC {\`e}re},% +firstplural={partie enti\IeC {\`e}res},% +text={partie enti\IeC {\`e}re},% +plural={partie enti\IeC {\`e}res},% +description={La partie entière d'un nombre réel est l'entier qui lui est immédiatement inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor $.},% +descriptionplural={La partie entière d'un nombre réel est l'entier qui lui est immédiatement inférieur ou égal. Pour un nombre réel $x$, on la note $\lfloor x \rfloor $.},% +symbol={\ensuremath {\lfloor x \rfloor }},% +symbolplural={\ensuremath {\lfloor x \rfloor }},% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{distanceHamming}{}% +{% +\gls@defglossaryentry{distanceHamming}% +{% +name={distance de Hamming},% +sort={distance de Hamming},% +type={main},% +first={distance de Hamming},% +firstplural={distance de Hammings},% +text={distance de Hamming},% +plural={distance de Hammings},% +description={La distance de Hamming entre deux éléments $x=(x_1,\ldots ,x_n)$ et $y=(y_1,\ldots ,y_n)$ dans $\Bool ^n$ est le nombre d'indices $i$, $1 \le i \le n$ tels que $x_i$ diffère de $y_i$.},% +descriptionplural={La distance de Hamming entre deux éléments $x=(x_1,\ldots ,x_n)$ et $y=(y_1,\ldots ,y_n)$ dans $\Bool ^n$ est le nombre d'indices $i$, $1 \le i \le n$ tels que $x_i$ diffère de $y_i$.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{decalageDeBits}{}% +{% +\gls@defglossaryentry{decalageDeBits}% +{% +name={décalage de bits},% +sort={décalage de bits},% +type={main},% +first={d\IeC {\'e}calage de bits},% +firstplural={d\IeC {\'e}calages de bits},% +text={d\IeC {\'e}calage de bits},% +plural={d\IeC {\'e}calages de bits},% +description={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) est obtenu en décalant les bits de $x$ de $b$ bits vers la gauche (resp. vers la droite) et en complétant avec des zéros à droite (resp. à gauche).},% +descriptionplural={Soit $x$ un nombre binaire de $n$ bits et $b$ un entier. Le nombre binaire de $n$ bits $x \ll b$ (respectivement $x \gg b$) est obtenu en décalant les bits de $x$ de $b$ bits vers la gauche (resp. vers la droite) et en complétant avec des zéros à droite (resp. à gauche).},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{chaineDeMarkov}{}% +{% +\gls@defglossaryentry{chaineDeMarkov}% +{% +name={chaîne de Markov},% +sort={chaîne de Markov},% +type={main},% +first={cha\IeC {\^\i }ne de Markov},% +firstplural={cha\IeC {\^\i }nes de Markov},% +text={cha\IeC {\^\i }ne de Markov},% +plural={cha\IeC {\^\i }nes de Markov},% +description={On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci désigne une suite de variables aléatoires $(X_n)_{n \in \Nats }$ à temps discret, à espace d'états discret, sans mémoire et dont le mécanisme de transition ne change pas au cours du temps. Formellement la propriété suivante doit être établie:\newline $ \forall n \ge 0, \forall (i_0, \ldots , i_{n-1}, i,j),\\ \textrm { }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots , X_{n-1}=i_{n-1}, X_{n}=i) \\ \textrm { }= P(X_{1}=j\mid X_n=i). $},% +descriptionplural={On se restreint à la définition d'une chaîne de Markov homogène. Celle-ci désigne une suite de variables aléatoires $(X_n)_{n \in \Nats }$ à temps discret, à espace d'états discret, sans mémoire et dont le mécanisme de transition ne change pas au cours du temps. Formellement la propriété suivante doit être établie:\newline $ \forall n \ge 0, \forall (i_0, \ldots , i_{n-1}, i,j),\\ \textrm { }P(X_{n+1}=j\mid X_0=i_0, X_1=i_1, X_2=i_2, \ldots , X_{n-1}=i_{n-1}, X_{n}=i) \\ \textrm { }= P(X_{1}=j\mid X_n=i). $},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{vecteurDeProbabilite}{}% +{% +\gls@defglossaryentry{vecteurDeProbabilite}% +{% +name={vecteur de probabilités},% +sort={vecteur de probabilités},% +type={main},% +first={vecteur de probabilit\IeC {\'e}s},% +firstplural={vecteurs de probabilit\IeC {\'e}s},% +text={vecteur de probabilit\IeC {\'e}s},% +plural={vecteurs de probabilit\IeC {\'e}s},% +description={Un vecteur de probabilités est un vecteur tel que toutes ses composantes sont positives ou nulles et leur somme vaut 1.},% +descriptionplural={Un vecteur de probabilités est un vecteur tel que toutes ses composantes sont positives ou nulles et leur somme vaut 1.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{matriceDAdjacence}{}% +{% +\gls@defglossaryentry{matriceDAdjacence}% +{% +name={matrice d'adjacence},% +sort={matrice d'adjacence},% +type={main},% +first={matrice d'adjacence},% +firstplural={matrice d'adjacences},% +text={matrice d'adjacence},% +plural={matrice d'adjacences},% +description={La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets est la matrice $\check {M}$ de dimension $n \times n$ dont l'élément $\check {M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.},% +descriptionplural={La matrice d'adjacence du graphe orienté $G=(S,A)$ à $n$ sommets est la matrice $\check {M}$ de dimension $n \times n$ dont l'élément $\check {M}_{ij}$ représente le nombre d'arcs d'origine $i$ et d'extrémité $j$.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{xor}{}% +{% +\gls@defglossaryentry{xor}% +{% +name={ou exclusif},% +sort={ou exclusif},% +type={main},% +first={ou exclusif},% +firstplural={ou exclusifs},% +text={ou exclusif},% +plural={ou exclusifs},% +description={La fonction \og ou exclusif\fg {}, XOR, est l'opérateur de $\Bool ^2$ dans $\Bool $ qui prend la valeur 1 si seulement si les deux opérandes ont des valeurs distinctes.},% +descriptionplural={La fonction \og ou exclusif\fg {}, XOR, est l'opérateur de $\Bool ^2$ dans $\Bool $ qui prend la valeur 1 si seulement si les deux opérandes ont des valeurs distinctes.},% +symbol={\ensuremath {\oplus }},% +symbolplural={\ensuremath {\oplus }},% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% +\ifglsentryexists{matriceDeTransitions}{}% +{% +\gls@defglossaryentry{matriceDeTransitions}% +{% +name={matrice de transitions},% +sort={matrice de transitions},% +type={main},% +first={matrice de transitions},% +firstplural={matrice de transitionss},% +text={matrice de transitions},% +plural={matrice de transitionss},% +description={Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ est la matrice de transitions associée à la chaine de Markov $X$.},% +descriptionplural={Le nombre $p_{ij}= P(X_1=j \mid X_0 =i)$ est appelé probabilité de transition de l'état $i$ à l'état $j$ en un pas. La matrice composée des $p_{ij}$ est la matrice de transitions associée à la chaine de Markov $X$.},% +symbol={\relax },% +symbolplural={\relax },% +user1={},% +user2={},% +user3={},% +user4={},% +user5={},% +user6={},% +long={},% +longplural={},% +short={},% +shortplural={},% +counter={page},% +parent={},% +% +}% +}% diff --git a/main.tex b/main.tex new file mode 100644 index 0000000..79ec26a --- /dev/null +++ b/main.tex @@ -0,0 +1,204 @@ +%% Use the standard UP-methodology class +%% with French language. +%% +%% You may specify the option 'twoside' or 'oneside' for +%% the document. +%% +%% See the documentation tex-upmethodology on +%% http://www.arakhne.org/tex-upmethodology/ +%% for details about the macros that are provided by the class and +%% to obtain the list of the packages that are already included. + +\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[utf8]{inputenc} + +%%-------------------- +%% Search path for pictures +%\graphicspath{{path1/},{path2/}} + +%%-------------------- +%% Definition of the bibliography entries +\declarebiblio{J}{Journaux internationaux avec comités de lecture}{mabiblio} + +%%-------------------- +%% Title of the document +\declarehdr{Title}{XX Mois XXXX} + +%%-------------------- +%% Set the author of the HDR +\addauthor[first.name@utbm.fr]{First}{Name} + +%%-------------------- +%% Add a member of the jury +%% \addjury{Firstname}{Lastname}{Role in the jury}{Position} +\addjury{First}{Name}{Rapporteur}{Professeur à l'Université de XXX} +\addjury{First}{Name}{Examinateur}{Professeur à l'Université de XXX} + +%%-------------------- +%% Change the style of the text in the list of the members of the jury. +%% \Set{jurystyle}{ style of the text} +%\Set{jurystyle}{\small} + +%%-------------------- +%% Set the University where HDR was made +\hdrpreparedin{Université de Technologie de Belfort-Montbéliard} + +%%-------------------- +%% Set the English abstract +%\hdrabstract[english]{This is the abstract in English} + +%%-------------------- +%% Set the English keywords. They only appear if +%% there is an English abstract +%\hdrkeywords[english]{Keyword 1, Keyword 2} + +%%-------------------- +%% Set the French abstract +\hdrabstract[french]{Blabla blabla.} + +%%-------------------- +%% Set the French keywords. They only appear if +%% there is an French abstract +%\hdrkeywords[french]{Mot-cl\'e 1, Mot-cl\'e 2} + +%%-------------------- +%% Change the layout and the style of the text of the "primary" abstract. +%% If your document is written in French, the primary abstract is in French, +%% otherwise it is in English. +\Set{primaryabstractstyle}{\small} + +%%-------------------- +%% Change the layout and the style of the text of the "secondary" abstract. +%% If your document is written in French, the secondary abstract is in English, +%% otherwise it is in French. +%\Set{secondaryabstractstyle}{\tiny} + +%%-------------------- +%% Change the layout and the style of the text of the "primary" keywords. +%% If your document is written in French, the primary keywords are in French, +%% otherwise they are in English. +%\Set{primarykeywordstyle}{\tiny} + +%%-------------------- +%% Change the layout and the style of the text of the "secondary" keywords. +%% If your document is written in French, the secondary keywords are in English, +%% otherwise they are in French. +%\Set{secondarykeywordstyle}{\tiny} + +%%-------------------- +%% Change the speciality of the PhD thesis +%\Set{speciality}{Informatique} + +%%-------------------- +%% Change the institution +%\Set{universityname}{Universit\'e de Technologie de Belfort-Montb\'eliard} + +%%-------------------- +%% Add the logo of a partner or a sponsor +%\addpartner{partner_logo} +\newcommand{\JFC}[1]{\begin{color}{green}\textit{#1}\end{color}} +\newcommand{\vectornorm}[1]{\ensuremath{\left|\left|#1\right|\right|_2}} +\newcommand{\ie}{\textit{i.e.}} +\newcommand{\Nats}[0]{\ensuremath{\mathbb{N}}} +\newcommand{\Reels}[0]{\ensuremath{\mathbb{R}}} +\newcommand{\Zed}[0]{\ensuremath{\mathbb{Z}}} +\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{\Equ}[1]{(\ref{#1})} +\newcommand{\deriv}{\mathrm{d}} +\newcommand{\class}[1]{\ensuremath{\langle #1\rangle}} +\newcommand{\dom}[0]{\ensuremath{\textit{dom}}} + + +\newtheorem{theorem}{Théorème} +\newtheorem{lemma}{Lemme} +\newtheorem{xpl}{Exemple} +\newtheorem{Proof}{Preuve} + +\begin{document} +\input{glossaire.tex} + +% \chapter*{Remerciements} + +% Blabla blabla. + +% \tableofcontents + + + + + +\chapter*{Introduction} + +Blabla blabla. + +\mainmatter + +\part{Système Booléens} + +\chapter{Iterations discrètes de Systèmes Dynamiques booléens} + +\JFC{Chapeau chapitre à faire} +\input{sdd} + + +\chapter[Preuve de convergence de systèmes booléens]{Preuve automatique de convergence de systèmes booléens} +\input{modelchecking} + + + + +\JFC{Mixage} + + + + + + +% \part{Conclusion et Perspectives} + +% \chapter{Conclusion} + +% Blabla blabla. + + +\appendix + +\chapter{Preuves sur les SDD} + +\section{Preuve du 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} +\input{annexecontinuite.tex} + +\section{Preuve de Correction et de complétude de l'approche de vérification de convergence à l'aide de SPIN} +\input{annexePromelaProof} + +\backmatter + +\bibliographystyle{apalike} +\bibliography{abbrev,biblioand} +\listoffigures +\listoftables +\listofdefinitions + +\end{document} + + + + + diff --git a/modelchecking.tex b/modelchecking.tex new file mode 100644 index 0000000..936835b --- /dev/null +++ b/modelchecking.tex @@ -0,0 +1,1042 @@ + + + +\section{Rappels sur le langage PROMELA} +\label{sec:spin:promela} + +Cette section rappelle les éléments fondamentaux du langage PROMELA (Process Meta Language). +On peut trouver davantage de détails dans~\cite{Hol03,Wei97}. + + + + +\begin{figure}[ht] +\begin{scriptsize} +\begin{lstlisting} +#define N 3 +#define d_0 5 + +bool X [N]; bool Xp [N]; int mods [N]; +typedef vals{bool v [N]}; +vals Xd [N]; + +typedef a_send{chan sent[N]=[d_0] of {bool}}; +a_send channels [N]; + +chan unlock_elements_update=[1] of {bool}; +chan sync_mutex=[1] of {bool}; +\end{lstlisting} +\end{scriptsize} +\caption{Type declaration of the DDNs translation.} +\label{fig:arrayofchannels} +\end{figure} + + +Les types primaires de PROMELA sont \texttt{bool}, \texttt{byte}, +\texttt{short} et \texttt{int}. Comme dans le langage C par exemple, +on peut declarer des tableaux à une dimension de taille constante +ou des nouveaux types de données (introduites par le mot clef +\verb+typedef+). Ces derniers sont utilisés pour définir des tableaux à deux +dimension. + +\begin{xpl} +Le programme donné à la {\sc Figure}~\ref{fig:arrayofchannels} correspond à des +déclarations de variables qui serviront dans l'exemple jouet de ce chapitre. +Il définit tout d'abord: +\begin{itemize} +\item les constantes \verb+N+ et \verb+d_0+ qui précisent respectivement le numbre + $n$ d'éléments et le délais maximum $\delta_0$; +\item les deux tableaux (\verb+X+ et \verb+Xp+) de \verb+N+ variables booléennes; +les cellules \verb+X[i]+ et \verb+Xp[i]+ sont associées à la variables $X_{i+1}$ +d'un systène dynamique discret +(le décallage d'un entier est dû à l'indexation à partir de zéro des cellules d'un tableau); +Elles memorisent les valeurs de $X_{i+1}$ respectivement avant et après sa mise à jour; +il suffit ainsi de comparer \verb+X+ et \verb+Xp+ pour constater si $X$ à changé ou pas; +\item le tableau \verb+mods+ contient les éléments qui doivent être modifiés lors de l'iteration +en cours; cela correspond naturellement à l'ensemble des éléments $S^t$; +\item le type de données structurées \verb+vals+ et le tableau de tableaux + \verb+Xd[+$i$\verb+].v[+$j$\verb+]+ qui vise à mémoriser $X_{j+1}^{D^{t-1}_{i+1j+1}}$ + pour l'itération au temps $t$ (en d'autres termes, utile lors du calcul de $X^{t}$). +\end{itemize} + + +Puisque le décallage d'un indices ne change pas fondamentalement +le comportement de la version PROMELA par rapport au modèle initial +et pour des raisons de clareté, on utilisera par la suite la même +lettre d'indice entre les deux niveaux (pour le modèle: $X_i$ et pour PROMELA: +\texttt{X[i]}). Cependant, ce décallage devra être conservé mémoire. + +Une donnée de type \texttt{channel} permet le +transfert de messages entre processus dans un ordre FIFO. +Elles serait déclarée avec le mot clef \verb+chan+ suivi par sa capacité +(qui est constante), son nom et le type des messages qui sont stockés dans ce cannal. +Dans l'exemple précédent, on déclare successivement: +\begin{itemize} +\item un cannal \verb+sent+ qui vise à mémoriser\verb+d_0+ messages de type + \verb+bool+; le tableau nommé \verb+channels+ de \verb+N+*\verb+N+ + éléments de type \verb+a_send+ est utilisé pour mémoriser les valeurs intermédiaires $X_j$; + Il permet donc de temporiser leur emploi par d'autres elements $i$. +\item les deux cannaux \verb+unlock_elements_update+ et \verb+sync_mutex+ contenant +chacun un message booléen et utilisé ensuite comme des sémaphores. +\end{itemize} +\end{xpl} + +%\subsection{PROMELA Processes} +Le langage PROMELA exploite la notion de \emph{process} pour modéliser la concurence +au sein de systèmes. Un process est déclaréavec le mot-clef +\verb+proctype+ et est instancié soit imédiatement (lorsque sa déclaration est préfixée + par le mot-clef \verb+active+) ou bien au moment de l'exécution de l'instruction +\texttt{run}. +Parmi tous les process, \verb+init+ est le process initial qui permet +d'initialiser les variables, lancer d'autres processes\ldots + + +Les instructions d'affecatation sont interprétées usuellement. +Les cannaux sont cernés par des instructions particulières d'envoi et de +réception de messages. Pour un cannal +\verb+ch+, ces instruction sont respectivement notées +\verb+ch ! m+ et \verb+ch ? m+. +L'instruction de réception consomme la valeur en tête du cannal \verb+ch+ +et l'affecte à la variable \verb+m+ (pour peu que \verb+ch+ soit initialisé et non vide). +De manière similaire,l'instruction d'envoi ajoute la valeur de \verb+m+ à la queue du canal +\verb+ch+ (pour peu que celui-ci soit initialisé et non rempli). +Dans les cas problématiques, canal non initialisé et vide pour une reception ou bien rempli pour un envoi, +le processus est blocké jusqu'à ce que les conditions soient remplies. + +La structures de contrôle \verb+if+ (resp. \verb+do+) définit un choix non déterministe + (resp. une boucle non déterministe). Que ce soit pour la conditionnelle ou la boucle, +si plus d'une des conditions est établie, l'ensemble des instructions correspondantes +sera choisi aléatoirement puis exécuté. + +Dans le process \verb+init+ détaillé à la {\sc Figure}~\ref{fig:spin:init}, +une boucle de taille $N$ initialise aléatoirement la variable globale de type tableau \verb+Xp+. +Ceci permet par la suite de verifier si les itérations sont convergentes pour n'importe +quelle configuration initiale $X^{(0)}$. + + + +Pour chaque élément $i$, si les itérations sont asynchrones +\begin{itemize} +\item on stocke d'abord la valeur de \verb+Xp[i]+ dans chaque \verb+Xd[j].v[i]+ +puisque la matrice $S^0$ est égale à $(0)$, +\item puis, la valeur de $i$ (représentée par \verb+Xp[i]+) devrait être transmise + à $j$ s'il y a un arc de $i$ à $j$ dans le graphe d'incidence. Dans ce cas, + c'est la fonction \verb+hasnext+ (non détaillée ici) + \JFC{la détailler} + qui memorise ce graphe + en fixant à \texttt{true} la variable \verb+is_succ+, naturellement et à + \texttt{false} dans le cas contraire. + Cela permet d'envoyer la valeur de $i$ dans le canal au travers de \verb+channels[i].sent[j]+. +\end{itemize} + +\begin{figure}[t] + \begin{minipage}[h]{.52\linewidth} +\begin{scriptsize} +\begin{lstlisting} +init{ + int i=0; int j=0; bool is_succ=0; + do + ::i==N->break; + ::i< N->{ + if + ::Xp[i]=0; + ::Xp[i]=1; + fi; + j=0; + do + ::j==N -> break; + ::j< N -> Xd[j].v[i]=Xp[i]; j++; + od; + j=0; + do + ::j==N -> break; + ::j< N -> { + hasnext(i,j); + if + ::(i!=j && is_succ==1) -> + channels[i].sent[j] ! Xp[i]; + ::(i==j || is_succ==0) -> skip; + fi; + j++;} + od; + i++;} + od; + sync_mutex ! 1; +} +\end{lstlisting} +\end{scriptsize} +\caption{PROMELA init process.}\label{fig:spin:init} +\end{minipage}\hfill + \begin{minipage}[h]{.42\linewidth} +\begin{scriptsize} +\begin{lstlisting} +active proctype scheduler(){ + do + ::sync_mutex ? 1 -> { + int i=0; int j=0; + do + :: i==N -> break; + :: i< N -> { + if + ::skip; + ::mods[j]=i; j++; + fi; + i++;} + od; + ar_len=i; + unlock_elements_update ! 1; + } + od +} +\end{lstlisting} +\end{scriptsize} +\caption{Scheduler process for common pseudo-periodic strategy. + \label{fig:scheduler}} +\end{minipage} +\end{figure} + + + +\section{Du système booléen au modèle PROMELA} +\label{sec:spin:translation} +Les éléments principaux des itérations asynchrones rappelées à l'équation +(\ref{eq:async}) sont la stratégie, la fonctions et la gestion des délais. +Dans cette section, nous présentons successivement comment chacune de +ces notions est traduite vers un modèle PROMELA. + + +\subsection{La stratégie}\label{sub:spin:strat} +Regardons comment une stratégie pseudo-périodique peut être représentée en PROMELA. +Intuitivement, un process \verb+scheduler+ (comme représenté à la {\sc Figure}~\ref{fig:scheduler}) +est itérativement appelé pour construire chaque $S^t$ représentant +les éléments possiblement mis à jour à l'itération $t$. + +Basiquement, le process est une boucle qui est débloquée lorsque la valeur du sémaphore +\verb+sync_mutex+ est 1. Dans ce cas, les éléments à modifier sont choisis +aléatoirement (grâce à $n$ choix successifs) et sont mémorisés dans le tableau +\verb+mods+, dont la taille est \verb+ar_len+. +Dans la séquence d'éxécution, le choix d'un élément mis à jour est directement +suivi par des mis àjour: ceci est réalisé grace à la modification de la valeur du sémaphore + \verb+unlock_elements_updates+. + +\subsection{Applying the function $F$}\label{sub:spin:update} +Updating a set $S^t=\{s_1,\ldots, s_m\}$ of elements that occur in the strategy +$(S^t)^{t \in \Nats}$ is implemented by the \verb+update_elems+ process given +in~\ref{fig:proc}. This active process waits until it is unlocked by the +\verb+scheduler+ process through the semaphore \verb+unlock_elements_update+. +The implementation is then fivefold: + +\begin{enumerate} +\item it starts with updating the variable \texttt{X} with the values of \texttt{Xp} + thanks to the \texttt{update\_X} function (not detailed here); + %%we recall that the variable \texttt{X} is only defined as +\item it stores in \texttt{Xd} the current available values of the elements thanks + to the function \texttt{fetch\_values} (see \Sec{sub:spin:vt}); +\item a loop over the number \texttt{ar\_len} of elements that have to evolve + iteratively updates the value of $j$ (through the function call \texttt{F(j)}) + provided this has to evolve, \textit{i.e.}, it is referenced by + \texttt{mods[count]}; source code of \texttt{F} is given in~\ref{fig:p} and is a + direct translation of the map $F$; +\item the new components values in \texttt{Xp} are symbolically sent to the other + components requiring them % for future access + thanks to the \texttt{diffuse\_values(Xp)} function (see \Sec{sub:spin:vt}); +\item finally, this process informs the scheduler about the end of the task + (through the semaphore \texttt{sync\_mutex}). +\end{enumerate} + + +\begin{figure}[t] + \begin{minipage}[h]{.475\linewidth} +\begin{scriptsize} +\begin{lstlisting} +active proctype update_elems(){ + do + ::unlock_elements_update ? 1 -> + { + atomic{ + bool is_succ=0; + update_X(); + fetch_values(); + int count = 0; + int j = 0; + do + ::count == ar_len -> break; + ::count < ar_len -> + j = mods[count]; + F(j); + count++; + od; + diffuse_values(Xp); + sync_mutex ! 1 + } + } + od +} +\end{lstlisting} +\end{scriptsize} +\caption{Updatings of the elements.}\label{fig:proc} + \end{minipage}\hfill% +%\end{figure} +%\begin{figure} + \begin{minipage}[h]{.45\linewidth} +\begin{scriptsize} +\begin{lstlisting} +inline F(){ + if + ::j==0 -> Xp[0] = + (Xs[j].v[0] & !Xs[j].v[1]) + |(Xs[j].v[2]) + ::j==1 -> Xp[1] = Xs[j].v[0] + | !Xs[j].v[2] + ::j==2 -> Xp[2] = Xs[j].v[1] + & Xs[j].v[2] + fi +} +\end{lstlisting} +\end{scriptsize} +\caption{Application of function $F$.}\label{fig:p} + \end{minipage} +\end{figure} + +% \subsection{Modifying Values of one Element} + +% Each element $i$ may modify its value through the coresponding +% active process \verb+pi+. +% In Fig.~\ref{fig:p4} that gives the translation of +% modifying the element $4$, the process is waiting until it is unlocked +% and then it computes the new value of $X_4$, represented by $X'_4$ +% and memorized as \verb+Xp[4]+. + + +% \begin{ProofCr} + +% First of all, the second hypothesis of the previous proof is established. + +% In this part, we prove that for any time $t$, + +% The proof is achieved under the hypothesis that at current time $t$, + +% For $j$ in $J^t$, variables +% \verb+v0+, \ldots \verb+vn-1+ are respectively +% $X_0^{S_{j0}^t},\ldots, X_{n-1}^{S_{jn-1}^t}$. +% Since \verb+F+ is the direct translation of $F$, rest of the proof is obvious. + + +% \end{ProofCr} + +\subsection{Delays Handling}\label{sub:spin:vt} +This section shows how delays are translated into PROMELA through the two +functions \verb+fetch_values+ and \verb+diffuse_values+, given in~\ref{fig:val} and~\ref{fig:broadcast}, that respectively store and transmit the +element values. + +\begin{figure}[t] + \begin{minipage}[h]{.475\linewidth} +\begin{scriptsize} +\begin{lstlisting} +inline fetch_values(){ + int countv = 0; + do + :: countv == ar_len -> break ; + :: countv < ar_len -> + j = mods[countv]; + i = 0; + do + :: (i == N) -> break; + :: (i < N && i == j) -> { + Xd[j].v[i] = Xp[i] ; + i++ } + :: (i < N && i != j) -> { + hasnext(i,j); + if + :: skip + :: is_succ==1 && + nempty(channels[i].sent[j]) -> + channels[i].sent[j] ? + Xd[j].v[i]; + fi; + i++ } + od; + countv++ + od +} +\end{lstlisting} +\end{scriptsize} +\caption{Fetching of the elements values\label{fig:val}} + \end{minipage}\hfill% + \begin{minipage}[h]{.475\linewidth} +\begin{scriptsize} +\begin{lstlisting} +inline diffuse_values(values){ + int countb=0; + do + :: countb == ar_len -> break ; + :: countb < ar_len -> + j = mods[countb]; + i = 0 ; + do + :: (i == N) -> break; + :: (i < N && i == j) -> i++; + :: (i < N && i != j) -> { + hasnext(j,i); + if + :: skip + :: is_succ==1 && + nfull(channels[j].sent[i]) -> + channels[j].sent[i] ! + values[j]; + fi; + i++ } + od; + countb++ + od +} +\end{lstlisting} +\end{scriptsize} +\caption{Diffusion of the elements values}\label{fig:broadcast} + \end{minipage} +\end{figure} + +The former potentially updates the array \verb+Xd+ needed by elements that have +to be modified. For each element in \verb+mods+, identified by the variable +$j$, the function retrieves the values of the other elements (labeled by $i$) +whose $j$ depends on. There are two cases: +\begin{itemize} +\item since $i$ knows its last value (\textit{i.e.}, $D^t_{ii}$ is always $t$) + \verb+Xd[i].v[i]+ is then \verb+Xp[i]+. +\item otherwise, there are two sub-cases which potentially update the value that + $j$ knows about $i$ (that may be chosen in a random way): + \begin{itemize} + \item from the viewpoint of $j$ the value of $i$ may not change (the + \verb+skip+ statement) or is not relevant; this latter case arises when + there is no edge from $i$ to $j$ in the incidence graph, \textit{i.e.}, when + the value of \verb+is_succ+ that is computed by \verb+hasnext(i,j)+ is 0; + then the value of \verb+Xd[j].v[i]+ is not modified; + \item otherwise, \verb+Xd[j].v[i]+ is assigned with the value stored in the + channel \verb+channels[i].sent[j]+ (provided this one is not empty). + Element values are added into this channel during the \verb+diffuse_values+ + function as follows. + \end{itemize} +\end{itemize} + +The \verb+diffuse_values+ function aims at storing the values of $X$ represented by +\verb+Xp+ in the \verb+channels+. It allows the SPIN model-checker to execute +the PROMELA model as if it allowed delays between processes. +% as if computation mode were asynchronous. +%For that reason, when an iteration has to synchronize the elements $i$ and +%$j$ (\textit{i.e.} when \verb+sync[j] == sync[i]+ is true), +% no delay emulation is performed. +%In the asynchronous mode, +There are two cases concerning the value of $X_{j}$: +\begin{itemize} +\item either it is left out to allow $i$ not to take into account all the values + of $j$; this case occurs either through the \verb+skip+ statement or when + there is no edge from $j$ to $i$ in the incidence graph; +\item or it is stored in the channel \verb+channels[j].sent[i]+ (provided it is + not full). +\end{itemize} + +Introducing non-determinism both in \verb+fetch_values+ and +\verb+diffuse_values+ functions is necessary in our context. If the +non-determinism would be used only in \verb+fetch_values+, then it would not be +possible for instance to retrieve the value $X_i^{(t)}$ without taking into +account the value $X_i^{(t-1)}$. On the other hand, if the non-determinism is +only used in \verb+diffuse_values+, then each time a value is pushed into the +channel, this value is immediately consumed, which contradicts the notion of +delays. + +\subsection{Discussion} +A coarse approach could consist in providing one process for each element. +However, the distance with the mathematical model given in \Equ{eq:async} of +such a translation would be larger than the method presented along these lines. +It induces that it would be harder to prove the soundness and completeness of +such a translation. For that reason we have developed a PROMELA model that is +as close as possible to the mathematical one. + +Notice furthermore that PROMELA is an imperative language which +often results in generating intermediate states +(to execute a matrix assignment for +instance). +The use of the \verb+atomic+ keyword allows the grouping of +instructions, making the PROMELA code and the DDN as closed as possible. + +\subsection{Universal Convergence Property} +We are left to show how to formalize into the SPIN model-checker that iterations +of a DDN with $n$ elements are universally convergent. We first recall that the +variables \verb+X+ and \verb+Xp+ respectively contain the value of $X$ before +and after an update. Then, by applying a non-deterministic initialization of +\verb+Xp+ and applying a pseudo-periodic strategy, it is necessary and +sufficient to establish the following Linear Temporal Logic (LTL) formula: +\begin{equation} +\diamond (\Box \verb+Xp+ = \verb+X+) +\label{eq:ltl:conv} +\end{equation} +where $\diamond$ and $\Box$ have the usual meaning \textit{i.e.}, respectively +{\em eventually} and {\em always} in the subsequent path. It is worth noticing +that this property only ensures the stabilization of the system, but it does not +provide any information over the way the system converges. In particular, some +indeterminism may still be present under the form of multiple fixed points +accessible from some initial states. + + + +\section{Proof of Translation Correctness}\label{sec:spin:proof} +\JFC{Déplacer les preuves en annexes} + +This section establishes the soundness and completeness of the approach +(Theorems~\ref{Theo:sound} and ~\ref{Theo:completeness}). Technical lemmas are +first shown to ease the proof of the two theorems. + + +% \begin{Lemma}[Absence of deadlock]\label{lemma:deadlock} +% Let $\phi$ be a DDN model and $\psi$ be its translation. There is no deadlock +% in any execution of $\psi$. +% \end{Lemma} +% \begin{Proof} +% In current translation, deadlocks of PROMELA may only be introduced through +% sending or receiving messages in channels. Sending (resp. receiving) a +% message in the \verb+diffuse_values+ (resp. \verb+fetch_values+) function is +% executed only if the channel is not full (resp. is not empty). In the +% \verb+update_elems+ and \verb+scheduler+ processes, each time one adds a value +% in any semaphore channel (\verb+unlock_elements_update+ and +% \verb+sync_mutex+), the corresponding value is read; avoiding deadlocks by the +% way. +% \end{Proof} + + +\begin{lemma}[Strategy Equivalence]\label{lemma:strategy} + Let $\phi$ be a DDN with strategy $(S^t)^{t \in \Nats}$ and $\psi$ be its + translation. There exists an execution of $\psi$ with weak fairness s.t. the + scheduler makes \verb+update_elems+ update elements of $S^t$ at iteration $t$. +\end{lemma} +\begin{Proof} + The proof is direct for $t=0$. Let us suppose it is established until $t$ is + some $t_0$. Let us consider pseudo-periodic strategies. Thanks to the weak + fairness equity property, \verb+update_elems+ will modify elements of $S^t$ at + iteration $t$. +\end{Proof} + +In what follows, let $Xd^t_{ji}$ be the value of +\verb+Xd[+$j$\verb+].v[+$i$\verb+]+ after the $t^{\text{th}}$ call to the +function \verb+fetch_values+. Furthermore, let $Y^k_{ij}$ be the element at +index $k$ in the channel \verb+channels[i].sent[j]+ of size $m$, $m \le +\delta_0$; $Y^0_{ij}$ and $Y^{m-1}_{ij}$ are respectively the head and the tail +of the channel. Secondly, let $(M_{ij}^t)^{t \in \{1, 1.5, 2, 2.5,\ldots\}}$ be a +sequence such that $M_{ij}^t$ is the partial function that associates to each +$k$, $0 \le k \le m-1$, the tuple $(Y^k_{ij},a^k_{ij},c^k_{ij})$ while entering +into the \verb+update_elems+ at iteration $t$ where +% \begin{itemize} +% \item + $Y^k_{ij}$ is the value of the channel \verb+channels[i].sent[j]+ + at index $k$, +%\item +$a^k_{ij}$ is the date (previous to $t$) when $Y^k_{ij}$ has been added and +%\item +$c^k_{ij}$ is the first date at which the value is available on $j$. So, + the value is removed from the channel $i\rightarrow j$ at date $c^k_{ij}+1$. +%\end{itemize} +$M_{ij}^t$ has the following signature: +\begin{equation*} +\begin{array}{rrcl} +M_{ij}^t: & +\{0,\ldots, \textit{max}-1\} &\rightarrow & E_i\times \Nats \times \Nats \\ +& k \in \{0,\ldots, m-1\} & \mapsto & M_{ij}(k)= (Y^k_{ij},a^k_{ij},c^k_{ij}). +\end{array} +\end{equation*} + +Intuitively, $M_{ij}^t$ is the memory of \verb+channels[i].sent[j]+ while +starting the iteration $t$. Notice that the domain of any $M_{ij}^1$ is $\{0\}$ +and $M_{ij}^1(0)=(\verb+Xp[i]+,0,0)$: indeed, the \verb+init+ process +initializes \verb+channels[i].sent[j]+ with \verb+Xp[i]+. + +Let us show how to make the indeterminism inside the two functions\linebreak +\verb+fetch_values+ and \verb+diffuse_values+ compliant with \Equ{eq:async}. +The function $M_{ij}^{t+1}$ is obtained by the successive updates of +$M_{ij}^{t}$ through the two functions\linebreak \verb+fetch_values+ and +\verb+diffuse_values+. Abusively, let $M_{ij}^{t+1/2}$ be the value of +$M_{ij}^{t}$ after the former function during iteration $t$. + +In what follows, we consider elements $i$ and $j$ both in $\llbracket 1, n +\rrbracket$ that are updated. At iteration $t$, $t \geq 1$, let +$(Y^0_{ij},a^0_{ij},c^0_{ij})$ be the value of $M_{ij}^t(0)$ at the beginning of +\verb+fetch_values+. If $t$ is equal to $c^0_{ij}+1$ then we execute the +instruction that assigns $Y^0_{ij}$ (\textit{i.e.}, the head value of +\verb+channels[i].sent[j]+) to $Xd_{ji}^t$. In that case, the function +$M_{ij}^t$ is updated as follows: $M_{ij}^{t+1/2}(k) = M_{ij}^{t}(k+1)$ for each +$k$, $0 \le k \le m-2$ and $m-1$ is removed from the domain of $M_{ij}^{t+1/2}$. +Otherwise (\textit{i.e.}, when $t < c^0_{ij}+1$ or when the domain of $M_{ij}$ +is empty) the \verb+skip+ statement is executed and $M_{ij}^{t+1/2} = +M_{ij}^{t}$. + +In the function \verb+diffuse_values+, if there exists some $\tau$, $\tau\ge t$ +such that \mbox{$D^{\tau}_{ji} = t$}, let $c_{ij}$ be defined by $ \min\{l \mid +D^{l}_{ji} = t \} $. In that case, we execute the instruction that adds the +value \verb+Xp[i]+ to the tail of \verb+channels[i].sent[j]+. Then, +$M_{ij}^{t+1}$ is defined as an extension of $M_{ij}^{t+1/2}$ in $m$ such that +$M_{ij}^{t+1}(m)$ is $(\verb+Xp[i]+,t,c_{ij})$. Otherwise (\textit{i.e.}, when $\forall l +\, . \, l \ge t \Rightarrow D^{l}_{ji} \neq t$ is established) the \verb+skip+ +statement is executed and $M_{ij}^{t+1} = M_{ij}^{t+1/2}$. + + +\begin{lemma}[Existence of SPIN Execution]\label{lemma:execution} + For any sequences $(S^t)^{t \in \Nats}$,\linebreak $(D^t)^{t \in \Nats}$, for + any map $F$ there exists a SPIN execution such that for any iteration $t$, $t + \ge 1$, for any $i$ and $j$ in $\llbracket 1, n \rrbracket$ we have the + following properties: + +\noindent If the domain of $M_{ij}^t$ is not empty, then +\begin{equation} + \left\{ + \begin{array}{rcl} + M_{ij}^1(0) & = & \left(X_i^{D_{ji}^{0}}, 0,0 \right) \\ + \textrm{if $t \geq 2$ then }M_{ij}^t(0) & = & + \left(X_i^{D_{ji}^{c}},D_{ji}^{c},c \right) \textrm{, } + c = \min\{l | D_{ji}^l > D_{ji}^{t-2} \} + \end{array} + \right. + \label{eq:Mij0} +\end{equation} +\noindent Secondly we have: +\begin{equation} + \forall t'\, .\, 1 \le t' \le t \Rightarrow Xd^{t'}_{ji} = X^{D^{t'-1}_{ji}}_i + \label{eq:correct_retrieve} +\end{equation} +\noindent Thirdly, for any $k\in S^t$. Then, the value of the computed variable +\verb+Xp[k]+ at the end of the \verb+update_elems+ process is equal to +$X_k^{t}$ \textit{i.e.}, $F_{k}\left( X_1^{D_{k\,1}^{t-1}},\ldots, + X_{n}^{D_{k\,{n}}^{t-1}}\right)$ at the end of the $t^{\text{th}}$ iteration. +\end{lemma} +\begin{Proof} +The proof is done by induction on the number of iterations. + +\paragraph{Initial case:} + +For the first item, by definition of $M_{ij}^t$, we have $M_{ij}^1(0) = \left( + \verb+Xp[i]+, 0,0 \right)$ that is obviously equal to $\left(X_i^{D_{ji}^{0}}, + 0,0 \right)$. + +Next, the first call to the function \verb+fetch_value+ either assigns the head +of \verb+channels[i].sent[j]+ to \verb+Xd[j].v[i]+ or does not modify +\verb+Xd[j].v[i]+. Thanks to the \verb+init+ process, both cases are equal to +\verb+Xp[i]+, \textit{i.e.}, $X_i^0$. The equation (\ref{eq:correct_retrieve}) is then +established. + + +For the last item, let $k$, $0 \le k \le n-1$. At the end of the first +execution\linebreak of the \verb+update_elems+ process, the value of +\verb+Xp[k]+ is\linebreak $F(\verb+Xd[+k\verb+].v[0]+, \ldots, +\verb+Xd[+k\verb+].v[+n-1\verb+]+)$. Thus, by definition of $Xd$, it is equal +to $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Thanks to \Equ{eq:correct_retrieve}, +we can conclude the proof. + + + +\paragraph{Inductive case:} + +Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$. + +First, if domain of definition of the function $M_{ij}^l$ is not empty, by +induction hypothesis $M_{ij}^{l}(0)$ is $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c +\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$. + +At iteration $l$, if $l < c + 1$ then the \verb+skip+ statement is executed in +the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to +$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$ +is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that +$D_{ji}^c > D_{ji}^{l-2}$ and $c=\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$. + +We now consider that at iteration $l$, $l$ is $c + 1$. In other words, $M_{ij}$ +is modified depending on the domain $\dom(M^l_{ij})$ of $M^l_{ij}$: +\begin{itemize} +\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow + D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the + first item of the lemma is established; +\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji} + = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that + is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} = + \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express + $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where + $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to + establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus + $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between + iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has + not updated $M_{ij}$. Formally we have +$$ +\forall t,k \, .\, D_{ji}^c < t < l \land k \geq t \Rightarrow D_{ji}^k \neq +t.$$ + +Particularly, $D_{ji}^{c'} \not \in \{D_{ji}^{c}+1,\ldots,l-1\}$. We can apply +the third item of the induction hypothesis to deduce +$\verb+Xp[i]+=X_i^{D_{ji}^{c'}}$ and we can conclude. + +\item if $\{0,1\} \subseteq \dom(M_{ij}^{l})$ then $M_{ij}^{l+1}(0)$ is + $M_{ij}^{l}(1)$. Let $M_{ij}^{l}(1)= \left(\verb+Xp[i]+, a_{ij} , c_{ij} + \right)$. By construction $a_{ij}$ is $\min\{t' | t' > D_{ji}^c \land + (\exists k \, .\, k \geq t' \land D_{ji}^k = t')\}$ and $c_{ij}$ is $\min\{k | + D_{ji}^k = a_{ij}\}$. Let us show $c_{ij}$ is equal to $\min\{k | D_{ji}^k > + D_{ji}^{l-1} \}$ further referred as $c'$. First we have $D_{ji}^{c_{ij}} = + a_{ij} > D_{ji}^c$. Since $c$ by definition is greater or equal to $l-1$ , + then $D_{ji}^{c_{ij}}> D_{ji}^{l-1}$ and then $c_{ij} \geq c'$. Next, since + $c$ is $l-1$, $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{c} \}$ and then $a_{ij} + \leq D_{ji}^{c'}$. Thus, $c_{ij} \leq c'$ and we can conclude as in the + previous part. +\end{itemize} + + +The case where the domain $\dom(M^l_{ij})$ is empty but the formula $\exists k +\, .\, k \geq l \land D_{ji}^k = l$ is established is equivalent to the second +case given above and then is omitted. + + +Secondly, let us focus on the formula~(\ref{eq:correct_retrieve}). At iteration +$l+1$, let $c'$ be defined as $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Two cases +have to be considered depending on whether $D_{ji}^{l}$ and $D_{ji}^{l-1}$ are +equal or not. +\begin{itemize} +\item If $D_{ji}^{l} = D_{ji}^{l-1}$, since $D_{ji}^{c'} > D_{ji}^{l-1}$, then + $D_{ji}^{c'} > D_{ji}^{l}$ and then $c'$ is distinct from $l$. Thus, the SPIN + execution detailed above does not modify $Xd_{ji}^{l+1}$. It is obvious to + establish that $Xd_{ji}^{l+1} = Xd_{ji}^{l} = X_i^{D_{ji}^{l-1}} = + X_i^{D_{ji}^{l}}$. +\item Otherwise $D_{ji}^{l}$ is greater than $D_{ji}^{l-1}$ and $c$ is thus $l$. + According to \Equ{eq:Mij0} we have proved, we have + $M_{ij}^{l+1}(0)=(X_i^{D_{ji}^{l}},D_{ji}^{l},l)$. Then the SPIN execution + detailed above assigns $X_i^{D_{ji}^{l}}$ to $Xd_{ji}^{l+1}$, which ends the + proof of (\ref{eq:correct_retrieve}). +\end{itemize} + +We are left to prove the induction of the third part of the lemma. Let $k$, $k +\in S^{l+1}$. % and $\verb+k'+ = k-1$. +At the end of the first execution of the \verb+update_elems+ process, we have +$\verb+Xp[+k\verb+]+= F(\verb+Xd[+k\verb+][0]+, +\ldots,\verb+Xd[+k\verb+][+n\verb+-1]+)+$. By definition of $Xd$, it is equal +to $F(Xd^{l+1}_{k\,0}, \ldots,Xd^{l+1}_{k\,n-1})$. Thanks to +\Equ{eq:correct_retrieve} we have proved, we can conclude the proof. +\end{Proof} + + +\begin{lemma} + Bounding the size of channels to $\textit{max} = \delta_0$ is sufficient when + simulating a DDN where delays are bounded by $\delta_0$. +\end{lemma} + +\begin{Proof} + For any $i$, $j$, at each iteration $t+1$, thanks to bounded delays (by + $\delta_0$), element $i$ has to know at worst $\delta_0$ values that are + $X_j^{t}$, \ldots, $X_j^{t-\delta_0+1}$. They can be stored into any channel + of size $\delta_0$. +\end{Proof} + + +\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound} + Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ verifies + the LTL property (\ref{eq:ltl:conv}) under weak fairness property, then + iterations of $\phi$ are universally convergent. +\end{theorem} +\begin{Proof} +% For the case where the strategy is finite, one notice that property +% verification is achieved under weak fairness property. Instructions that +% write or read into \verb+channels[j].sent[i]+ are continuously enabled leading +% to convenient available dates $D_{ji}$. It is then easy to construct +% corresponding iterations of the DDN that are convergent. +% \ANNOT{quel sens donnes-tu a \emph{convenient} ici ?} + + Let us show the contraposition of the theorem. The previous lemmas have shown + that for any sequence of iterations of the DDN, there exists an execution of + the PROMELA model that simulates them. If some iterations of the DDN are + divergent, then they prevent the PROMELA model from stabilizing, \textit{i.e.}, not + verifying the LTL property (\ref{eq:ltl:conv}). +\end{Proof} + + +% \begin{Corol}[Soundness wrt universall convergence property]\label{Theo:sound} +% Let $\phi$ be a DDN model where strategy, $X^(0)$ +% are only constrained to be pseudo-periodic and +% in $E$ respectively. +% Let $\psi$ be its translation. +% If all the executions of $\psi$ converge, +% then iterations of $\phi$ are universally convergent. +% \end{Corol} + + + +\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness} + Let $\phi$ be a DDN model and $\psi$ be its translation. If $\psi$ does not + verify the LTL property (\ref{eq:ltl:conv}) under weak fairness property then + the iterations of $\phi$ are divergent. +\end{theorem} +\begin{Proof} + For models $\psi$ that do not verify the LTL property (\ref{eq:ltl:conv}) it + is easy to construct corresponding iterations of the DDN, whose strategy is + pseudo-periodic since weak fairness property is taken into account. + +% i.e. iterations that are divergent. Executions are +% performed under weak fairness property; we then detail what are continuously +% enabled: +% \begin{itemize} +% \item if the strategy is not defined as periodic, elements $0$, \ldots, $n$ are +% infinitely often updated leading to pseudo-periodic strategy; +% \item instructions that write or read into \verb+channels[j].sent[i]+ are +% continuously enabled leading to convenient available dates $D_{ji}$. +% \end{itemize} +% The simulated DDN does not stabilize and its iterations are divergent. + \end{Proof} + + + +\section{Practical Issues} +\label{sec:spin:practical} +This section first gives some notes about complexity and later presents +experiments. +%\subsection{Complexity Analysis} +%\label{sub:spin:complexity} +\begin{theorem}[Number of states] + Let $\phi$ be a DDN model with $n$ elements, $m$ edges in the incidence graph + and $\psi$ be its translation into PROMELA. The number of configurations of + the $\psi$ SPIN execution is bounded by $2^{m\times(\delta_0+1)+n(n+2)}$. +\end{theorem} +\begin{Proof} + A configuration is a valuation of global variables. Their number only depends + on those that are not constant. + + The variables \verb+Xp+ \verb+X+ lead to $2^{2n}$ states. The variable + \verb+Xs+ leads to $2^{n^2}$ states. Each channel of \verb+array_of_channels+ + may yield $1+2^1+\ldots+2^{\delta_0}= 2^{\delta_0+1}-1$ states. Since the + number of edges in the incidence graph is $m$, there are $m$ non-constant + channels, leading to approximately $2^{m\times(\delta_0+1)}$ states. The + number of configurations is then bounded by $2^{m\times(\delta_0+1)+n(n+2)}$. + Notice that this bound is tractable by SPIN for small values of $n$, + $m$ and $\delta_0$. +\end{Proof} + + + +The method detailed along the line of this article has been applied on the +running example to formally prove its universally convergence. + +First of all, SPIN only considers weak fairness property between processes +whereas above proofs need such a behavior to be established each time a +non-deterministic choice is done. + + +A first attempt has consisted in building the following formula +each time an undeterministic choice between $k$ elements +respectively labeled $l1$, \ldots $lk$ occurs: +$$ +[] <> (l == l0) \Rightarrow +(([] <> (l== l1)) \land \ldots \land ([] <> (l == lk))) +$$ +where label $l0$ denotes the line before the choice. +This formula exactly translates the fairness property. +The negation of such a LTL formula may then be efficiently translated +into a Büchi automata with the tool ltl2ba~\cite{GO01}. +However due to an explosion of the size of the product +between this automata and the automata issued from the PROMELA program +SPIN did not success to verify whether the property is established or not. + +This problem has been practically tackled by leaving spin generating all the (not necessarily fair) computations and verifying convergence property on them. +We are then left to interpret its output with two issues. +If property is established for all the computations, +it is particularly established for fair ones and iterations are convergent. +In the opposite case, when facing to a counter example, an analysis of the SPIN +output is achieved. +\begin{xpl} +Experiments have shown that all the iterations of the running example are +convergent for a delay equal to 1 in less than 10 min. +The example presented in~\cite{abcvs05} with five elements taking boolean +values has been verified with method presented in this article. +Immediately, SPIN computes a counter example, that unfortunately does not +fulfill fairness properties. Fair counter example is obtained +after few minutes. +All the experimentation have been realized in a classic desktop computer. +\end{xpl} + + + + + +%However preliminary experiments have shown the interest of the approach. + + + +% The method detailed along the line of this article has been +% applied on some examples to formally prove their convergence +% (Fig.~\ref{fig:async:exp}). +% In these experiments, Delays are supposed to be bounded by $\delta_0$ set to 10. +% In these arrays, +% $P$ is true ($\top$) provided the uniform convergence property is established, false ($\bot$) otherwise, +% $M$ is the amount of memory usage (in MB) and +% $T$ is the time needed on a Intel Centrino Dual Core 2 Duo @1.8GHz with 2GB of memory, both +% to establish or refute the property. + +% RE is the running example of this article, +% AC2D is a cellular automata with 9 elements taking boolean values +% according their four neighbors +% and BM99 is has been proposed in~\cite{BM99} and consists of 10 process +% modifying their boolean values, but with many connected connection graph. + + + + + +% \begin{figure} +% \begin{center} +% \scriptsize +% \begin{tabular}{|*{13}{c|}} +% \cline{2-13} +% \multicolumn{1}{c|}{ } +% &\multicolumn{6}{|c|}{Mixed Mode} & \multicolumn{6}{|c|}{Only Bounded} \\ +% \cline{2-13} +% \multicolumn{1}{c|}{ } +% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} & +% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\ +% \cline{2-13} +% \multicolumn{1}{c|}{ } +% &P & M & T & +% P & M & T & +% P & M & T& +% P & M & T \\ +% \hline %cline{2-13} +% Running Example & +% $\top$ & 409 & 1m11s& +% $\bot$ & 370 & 0.54 & +% $\bot$ & 374 & 7.7s& +% $\bot$ & 370 & 0.51s \\ +% \hline %\cline{2-13} +% AC2D +% &$\bot$ & 2.5 & 0.001s % RC07_async_mixed.spin +% &$\bot$ & 2.5 & 0.01s % RC07_async_mixed_all.spin +% &$\bot$ & 2.5 & 0.01s % RC07_async.spin +% &$\bot$ & 2.5 & 0.01s \\ % RC07_async_all.spin +% \hline %\cline{2-13} +% BM99 +% &$\top$ & & %BM99_mixed_para.spin +% &$\top$ & & % RC07_async_mixed_all.spin +% &$\bot$ & & % RC07_async.spin +% &$\bot$ & & \\ % RC07_async_all.spin +% \hline %\cline{2-13} +% \end{tabular} +% \end{center} +% \caption{Experimentations with Asynchronous Iterations}\label{fig:async:exp} +% \end{figure} + + + +% The example~\cite{RC07} deals with a network composed of two genes taking their +% values into $\{0,1,2\}$. Since parallel iterations is already diverging, +% the same behavior is observed for all other modes. +% The Figure~\ref{fig:RC07CE} gives the trace leading to convergence property +% violation output by SPIN. +% It corresponds to peridic strategy that repeats $\{1,2\};\{1,2\};\{1\};\{1,2\};\{1,2\}$ and starts with $X=(0,0)$. + + +% In the example extracted from~\cite{BM99}, +% we have 10 processors computing a binary value. +% Due to the huge number of dependencies between these calculus, +% $\delta_0$ is reduced to 1. It nevertheless leads to about $2^{100}$ +% configurations in asynchronous iterations. + +% Let us focus on checking universal convergence of asynchronous iterations +% of example~\cite{BCVC10:ir}. +% With a $\delta_0$ set to 5, SPIN generates an out of memory error. +% However, it succeed to prove that the property is not established even +% with $\delta_0$ set to 1 which is then sufficient. + + +% \begin{figure} +% \begin{center} +% \begin{tiny} +% \begin{tabular}{|*{7}{c|}} +% \cline{2-7} +% \multicolumn{1}{c|}{ } +% &\multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Pseudo-Periodic} \\ +% \cline{2-7} +% \multicolumn{1}{c|}{ }& +% P & M & T& +% P & M & T \\ +% \hline %\cline{2-7} +% Running & +% $\top$ & 2.7 & 0.01s & +% $\bot$ & 369.371 & 0.509s \\ +% \hline %\cline{2-7} +% \cite{RC07} example & +% $\bot$ & 2.5 & 0.001s & % RC07_sync.spin +% $\bot$ & 2.5 & 0.01s \\ % RC07_sync_chao_all.spin +% \hline +% \cite{BM99} example & +% $\top$ & 36.7 & 12s & % BM99_sync_para.spin +% $\top$ & & \\ % BM99_sync_chao.spin +% \hline +% \end{tabular} +% \end{tiny} +% \end{center} +% \caption{Experimentations with Synchronous Iterations}\label{fig:sync:exp} +% \end{figure} + + + + + + +% \begin{tabular}{|*{}{c|}} +% % \hline +% % e \\ +% % +% \hline +% & \multicolumn{6}{|c|}{Synchronous} & \multicolumn{12}{|c|}{Asynchronous}\\ +% \cline{8-19} +% Delay & \multicolumn{6}{|c|}{ } +% & \multicolumn{6}{|c|} +% {Only Bounded} +% & \multicolumn{6}{|c|} +% {Bounded+Mixed Mode}\\ +% Strategy& +% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} & +% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} & +% \multicolumn{3}{|c|}{Parallel} & \multicolumn{3}{|c|}{Chaotic} \\ + + +% \end{tabular} + + +\section{Conclusion and Future Work} +\label{sec:spin:concl} +Stochastic based prototypes have been implemented to generate both +strategies and delays for asynchronous iterations in first in~\cite{BM99,BCV02}. +However, since these research softwares are not exhaustive, they really give an +formal answer when they found a counterexample. When facing convergence, they only convince +the user about this behavior without exhibiting a proof. + +As far as we know, no implemented formal method tackles the problem of +proving asynchronous iterations convergence. +In the theoretical work~\cite{Cha06} Chandrasekaran shows that asynchronous iterations +are convergent iff we can build a decreasing Lyaponov function, +but does not gives any automated method to compute it. + +In this work, we have shown how convergence proof for any asynchronous +iterations of discrete dynamical networks with bounded delays +can be automatically achieved. +The key idea is to translate the network (map, strategy) into PROMELA and +to leave the SPIN model checker establishing the validity +of the temporal property corresponding to the convergence. +The correctness and completeness of the approach have been proved, notably +by computing a SPIN execution of the PROMELA model that have the same +behaviors than initial network. +The complexity of the problem is addressed. It shows that non trivial example +may be addressed by this technique. + +Among drawbacks of the method, one can argue that bounded delays is only +realistic in practice for close systems. +However, in real large scale distributed systems where bandwidth is weak, +this restriction is too strong. In that case, one should only consider that +matrix $S^{t}$ follows the iterations of the system, \textit{i.e.}, +for all $i$, $j$, $1 \le i \le j \le n$, we have$ +\lim\limits_{t \to \infty} S_{ij}^t = + \infty$. +One challenge of this work should consist in weakening this constraint. +We plan as future work to take into account other automatic approaches +to discharge proofs notably by deductive analysis~\cite{CGK05}. + + + + + + diff --git a/sdd.tex b/sdd.tex new file mode 100644 index 0000000..0bd7629 --- /dev/null +++ b/sdd.tex @@ -0,0 +1,255 @@ + + + +\JFC{Chapeau chapitre à faire} + + + +Cette section énonce quelques notions suffisantes +à la compréhension de ce document. +Elle commence par formaliser ce que sont les systèmes dynamiques booléens +(section \ref{sub:sdd}) +et montre comment en extraire leur graphe d'itérations (section~\ref{sub:grIter}) +et d'interactions (section~\ref{sub:sdd:inter}). +Elle se termine en définissant une distance sur l'espace +$\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$ (section~\ref{sub:metric}) +qui permet ensuite (section~\ref{sec:charac}) d'établir la chaoticité des +systèmes dynamiques booléens. + + + + + +\section{Système dynamique booléen}\label{sub:sdd} + +Soit $n$ un entier naturel. Un système dynamique booléen est +défini à partir d'une fonction booléenne: +\[ +f:\Bool^n\to\Bool^n,\qquad x=(x_1,\dots,x_n)\mapsto f(x)=(f_1(x),\dots,f_n(x)), +\] +et un {\emph{schéma des itérations}} qui peuvent être +parallèles, séquentielles ou asynchrones \ldots +Le schéma des itérations parallèles est défini comme suit: +à partir d'une configuration initiale $x^0\in\Bool^n$, la suite +$(x^{t})^{t \in \Nats}$ +des configurations du système est construite à partir de la relation de récurrence +$x^{t+1}=f(x^t)$. Tous les $x_i$, $1 \le i \le n$ +sont ainsi mis à jour à chaque itération. +Le schéma qui ne modifie qu'un élément +$i$, $1 \le i \le n$ à chaque itération +est le schéma \emph{asynchrone}. +Plus formellement, à la $t^{\textrm{ème}}$ itération, seul le $s_{t}^{\textrm{ème}}$ +composant (entre 1 et $n$) est mis à jour. +La suite $s = \left(s_t\right)_{t \in \mathds{N}}$ est une séquence d'indices +de $\llbracket 1;n \rrbracket$ appelée \emph{stratégie}. Formellement, dans +ce mode opératoire, +soit $F_f: \llbracket1;n\rrbracket\times \Bool^{n}$ vers $\Bool^n$ définie par +\[ +F_f(i,x)=(x_1,\dots,x_{i-1},f_i(x),x_{i+1},\dots,x_n). +\] + +Dans le schéma des itérations asynchrones pour une configuration initiale +$x^0\in\Bool^n$ et une stratégie $s\in +\llbracket1;n\rrbracket^\Nats$, les configurations $x^t$ +sont définies par la récurrence +\begin{equation}\label{eq:asyn} +x^{t+1}=F_f(s_t,x^t). +\end{equation} + +Soit alors $G_f$ une fonction de $\llbracket1;n\rrbracket^\Nats\times\Bool^n$ +dans lui même définie par +\[ +G_f(s,x)=(\sigma(s),F_f(s_0,x)), +\] +où $\forall t\in\Nats,\sigma(s)_t=s_{t+1}$. +En d'autres termes la fonction $\sigma$ décale +la stratégie fournie en argument d'un élément vers la gauche en supprimant +l'élément de tête. +Les itérations parallèles de $G_f$ depuis un point initial +$X^0=(s,x^0)$ décrivent la même orbite que les +itérations asynchrones de $f$ induites par $x^0$ et la stratégie +$s$. + +\section{Graphe d'itérations}\label{sub:grIter} + +Soit $f$ une fonction de $\Bool^n$ dans lui-même. +Le {\emph{graphe des itérations asynchrones}} associé à $f$ est le +graphe orienté $\Gamma(f)$ défini ainsi: +l'ensemble de ses sommets est $\Bool^n$ et pour chaque $x\in\Bool^n$ et +$i\in \llbracket1;n\rrbracket$, le graphe $\Gamma(f)$ +contient un arc de $x$ vers $F_f(i,x)$. +La relation entre $\Gamma(f)$ et $G_f$ est claire: il existe un +chemin de $x$ à $x'$ dans $\Gamma(f)$ si et seulement s'il existe une +stratégie $s$ telle que les itérations parallèles $G_f$ à partir +du point $(s,x)$ mènent au point $x'$. + + +Dans ce qui suit, et par souci de concision, le terme \emph{graphe des itérations} +est une abréviation de graphe des itérations asynchrones. +La figure~\ref{fig:xplgraphIter} donne deux exemples de graphes d'itérations +pour les fonctions $g$ et $h$ définies dans $\Bool^2$ qui sont reprises tout au long +de ce document. + + + +\begin{figure}% +\centering +\begin{minipage}{0.40\textwidth} + \begin{center} + \includegraphics[height=4cm]{images/g.pdf} + \end{center} +\caption{$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $}% +\label{fig:g:iter}% +\end{minipage} +\qquad +\begin{minipage}{0.40\textwidth}% + \begin{center} + \includegraphics[height=4cm]{images/h.pdf} + \end{center} +\caption{$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$}% +\label{fig:h:iter}% +\end{minipage}% +\end{figure}% + +% \begin{figure}%[t] +% \begin{center} +% \subfloat[$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $]{ +% \begin{minipage}{0.40\textwidth} +% \begin{center} +% \includegraphics[height=4cm]{images/g.pdf} +% \end{center} +% \end{minipage} +% \label{fig:g:iter} +% } +% \subfloat[$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$]{ +% \begin{minipage}{0.40\textwidth} +% \begin{center} +% \includegraphics[height=4cm]{images/h.pdf} +% \end{center} +% \end{minipage} +% \label{fig:h:iter} +% } \end{center} +% \caption{Graphes d'itérations de fonctions booléennes dans $\Bool^2$} +% \label{fig:xplgraphIter} +% \end{figure} + + + + + + + +\section{Graphe d'interactions}\label{sub:sdd:inter} + +Pour $x\in\Bool^n$ et $i\in\llbracket 1;n\rrbracket$, on nomme +$\overline{x}^i$ la configuration obtenue en niant le +$i^{\textrm{ème}}$ composant de $x$. En d'autres termes +$\overline{x}^i=(x_1,\dots,\overline{x_i},\dots,x_n)$. +Des interactions entre les composants du +système peuvent être mémorisées +dans la {\emph{matrice Jacobienne discrète}} $f'$. +Celle-ci est définie comme étant la fonction qui à chaque +configuration $x\in\Bool^n$ associe la matrice de taille +$n\times n$ +\[ +f'(x)=(f_{ij}(x)),\qquad +f_{ij}(x)=\frac{f_i(\overline{x}^j)-f_i(x)}{\overline{x}^j_j-x_j}\qquad (i,j\in\llbracket1;n\rrbracket). +\] +On note que dans l'équation donnant la valeur de $f_{ij}(x)$, +les termes $f_i(\overline{x}^j)$, $f_i(x)$, +$\overline{x}^j_j$ et $x_j$ sont considérés comme des entiers naturels +égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$. + +En outre, les interactions peuvent se représenter à l'aide d'un +graphe $G(f)$ orienté et signé défini ainsi: +l'ensemble des sommets est +$\llbracket1;n\rrbracket$ et il existe un arc de $j$ à $i$ de signe + $s\in\{-1,1\}$, noté $(j,s,i)$, si $f_{ij}(x)=s$ pour au moins +un $x\in\Bool^n$. +On note que la présence de +deux arcs de signes opposés entre deux sommets donnés +est possible. + + + + + +\begin{figure}% +\centering +\begin{minipage}{0.40\textwidth} + \begin{center} + \includegraphics[height=3cm]{images/gp.pdf} + \end{center} +\caption{$g(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}) $}% +\label{fig:g:inter}% +\end{minipage} +\qquad +\begin{minipage}{0.40\textwidth} + \begin{center} + \includegraphics[height=3cm]{images/hp.pdf} + \end{center} +\caption{$h(x_1,x_2)=(\overline{x_1},x_1\overline{x_2}+\overline{x_1}x_2)$}% +\label{fig:h:inter}% +\end{minipage}% +\caption{Graphes d'interactions de fonctions booléennes dans $\Bool^2$} +\label{fig:xplgraphInter} +\end{figure}% + + + + + + + + + +Soit $P$ une suite d'arcs de $G(f)$ de la forme +\[ +(i_1,s_1,i_2),(i_2,s_2,i_3),\ldots,(i_r,s_r,i_{r+1}). +\] +Alors, $P$ est dit un chemin de $G(f)$ de longueur $r$ et de signe +$\Pi_{i=1}^{r}s_i$ et $i_{r+1}$ est dit accessible depuis +$i_1$. +$P$ est un {\emph{circuit}} si $i_{r+1}=i_1$ et si les sommets +$i_1$,\ldots $i_r$ sont deux à deux disjoints. +Un sommet $i$ de $G(f)$ a une {\emph{boucle}} +positive (resp. négative) , si $G(f)$ a un +arc positif (resp. un arc négatif) de $i$ vers lui-même. + + + + + +\section{Distance sur l'espace $\llbracket 1;n\rrbracket^{\Nats}\times \Bool^n$}\label{sub:metric} +On considère l'espace $\mathcal{X}=\llbracket 1;n\rrbracket^{\Nats}\times +\Bool^n$ et +on définit la distance $d$ entre les points $X=(s,x)$ et +$X'=(s',x')$ de $\mathcal{X}$ par +\[ +d(X,X')= d_H(x,x')+d_S(s,s'),~\textrm{où}~ +\left\{ +\begin{array}{l} +\displaystyle{d_H(x,x')=\sum_{i=1}^n |x_i-x'_i|}\\[5mm] +\displaystyle{d_S(s,s')=\frac{9}{n}\sum_{t\in\Nats}\frac{|s_t-s'_t|}{10^{t+1}}}. +\end{array} +\right.\,. +\] +On note que dans le calcul de $d_H(x,x')$-- +appelée \gls{distanceHamming} (cf. glossaire) entre $x$ et $x'$-- +les termes $x_i$ et $x'_i$ sont considérés comme des entiers naturels +égaux à $0$ ou à $1$ et que le calcul est effectué dans $\Z$. +De plus, la \gls{partieentiere} (cf. glossaire) +$\lfloor d(X,X')\rfloor$ est égale à $d_H(x,x')$ soit la distance +de Hamming entre $x$ et $x'$. +%D'autre part, $d(X,X')-\lfloor d(X,X')\rfloor=d_S(s,s')$ +%mesure la différence entre $s$ et $s'$. +On remarque que la partie décimale est inférieure à $10^{-l}$ si +et seulement si les $l$ premiers termes des deux stratégies sont égaux. +De plus, si la +$(l+1)^{\textrm{ème}}$ décimale +de $d_S(s,s')$ +n'est pas nulle, alors $s_l$ est différent de $s'_l$. + +On peut démontrer que pour toute fonction booléenne $f$, +$G_f$ est continue sur $\mathcal{X}$ (cf annexe~\ref{anx:cont}). + diff --git a/spimufchdr-backpage.eps b/spimufchdr-backpage.eps new file mode 120000 index 0000000..2d8bc36 --- /dev/null +++ b/spimufchdr-backpage.eps @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-backpage.eps \ No newline at end of file diff --git a/spimufchdr-backpage.pdf b/spimufchdr-backpage.pdf new file mode 120000 index 0000000..b0d23e8 --- /dev/null +++ b/spimufchdr-backpage.pdf @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-backpage.pdf \ No newline at end of file diff --git a/spimufchdr-frontpage.eps b/spimufchdr-frontpage.eps new file mode 120000 index 0000000..d2fa809 --- /dev/null +++ b/spimufchdr-frontpage.eps @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-frontpage.eps \ No newline at end of file diff --git a/spimufchdr-frontpage.pdf b/spimufchdr-frontpage.pdf new file mode 120000 index 0000000..b43953c --- /dev/null +++ b/spimufchdr-frontpage.pdf @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-frontpage.pdf \ No newline at end of file diff --git a/spimufchdr-p3-head.eps b/spimufchdr-p3-head.eps new file mode 120000 index 0000000..5058097 --- /dev/null +++ b/spimufchdr-p3-head.eps @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-p3-head.eps \ No newline at end of file diff --git a/spimufchdr-p3-head.pdf b/spimufchdr-p3-head.pdf new file mode 120000 index 0000000..047ded2 --- /dev/null +++ b/spimufchdr-p3-head.pdf @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr-p3-head.pdf \ No newline at end of file diff --git a/spimufchdr.cls b/spimufchdr.cls new file mode 120000 index 0000000..8c0a812 --- /dev/null +++ b/spimufchdr.cls @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/spimufchdr.cls \ No newline at end of file diff --git a/tente.png b/tente.png new file mode 100644 index 0000000..d5b6f24 Binary files /dev/null and b/tente.png differ diff --git a/upmext-spimufchdr.cfg b/upmext-spimufchdr.cfg new file mode 120000 index 0000000..cce34c7 --- /dev/null +++ b/upmext-spimufchdr.cfg @@ -0,0 +1 @@ +latexStyle/tex-templates/hdr/spimufchdr/upmext-spimufchdr.cfg \ No newline at end of file