cours.tex (14618B)
1 \documentclass[a4paper,french,9pt]{article} 2 \usepackage[reset]{geometry} 3 \geometry{a4paper, top=2cm, bottom=2.0cm, left=4.4cm, right=4.47cm} 4 \usepackage[frenchb]{babel} 5 \usepackage[utf8]{inputenc} 6 \usepackage[T1]{fontenc} 7 \usepackage{amsmath} 8 \usepackage{amssymb} 9 \usepackage{centernot} 10 \usepackage{multirow} 11 \usepackage{tikz} 12 \usetikzlibrary{positioning,calc,chains,intersections} 13 \def\P{\mathcal{P}} 14 \def\GUi{G \cup \{i\}} 15 \def\nottransition#1{\stackrel{#1}{\centernot\longrightarrow}} 16 \def\transition#1{\stackrel{#1}{\longrightarrow}} 17 \def\Transition#1{\stackrel{#1}{\Longrightarrow}} 18 \def\forte{\sim} 19 \def\observationnelle{\approx} 20 \def\conf{\ \text{conf}\ } 21 \DeclareMathOperator{\Tr}{Tr} 22 \DeclareMathOperator{\Acc}{Acc} 23 \DeclareMathOperator{\Ref}{Ref} 24 \def\si{\quad\text{si}\quad} 25 \let\simule\gtrsim 26 \let\estsimulepar\gtrsim 27 \begin{document} 28 29 \section{Définitions} 30 31 \begin{description} 32 \item[LTS] (Labeled Transition System = Système de transitions étiquetées) : $$P = \langle\P,A,\rightarrow,P\rangle$$ 33 \begin{description} 34 \item[$\P$]: États. $\P = \{P, Q, R, \dots\}$. 35 \item[$A$]: Actions (étiquettes que l'on mettra sur les transitions). $A \subseteq \GUi$. $G$ est l'ensemble des actions observables. $i$ 36 est l'action interne que le système peut faire de lui-même. 37 \item[$\rightarrow$]: Transitions. $\rightarrow \in \P\times A\times\P$. $P\transition{a}Q$~: le système se tranforme, passe de $P$ à $Q$ 38 en exécutant $a$. 39 \item[$P$]: Nom du LTS, et aussi son premier état (donc $P \in \P$). 40 \end{description} 41 \item[Trace]: Ensemble des listes d'actions que l'on peut exécuter. La trace vide est notée $\varepsilon$. 42 \begin{center} 43 \begin{tikzpicture}[node distance=5mm] 44 \node (p) {P}; 45 \node[above right= of p] (q) {Q}; 46 \node[below right= of p] (r) {R}; 47 \node[right= of q] (stop1) {Stop}; 48 \node[right= of r] (stop2) {Stop}; 49 \draw[->] (p) -- node[above,near start] {a} (q); 50 \draw[->] (p) -- node[below,near start] {a} (r); 51 \draw[->] (q) -- node[above] {b} (stop1); 52 \draw[->] (r) -- node[above] {c} (stop2); 53 \end{tikzpicture} 54 \end{center} 55 $$\Tr(P) = \{\varepsilon, a, ab, ac\}$$ 56 \item[Chemin]: Si $P\transition{a_1}P_1\transition{a_2}\cdots\transition{a_n}P_n$ où $a_i \in \GUi$, on note $P\transition{t}P_n$ avec $t = 57 a_1; a_2; \dots; a_n$. $(a_3,a_4)$ est un sous-chemin de $P$. 58 \item[Exécution] Une exécution partielle de $P$ est un chemin de $P$ partant de l'état initial $P$. Une exécution complète de $P$ est une q 59 exécution partielle de $P$ que l'on ne peut pas compléter (j'ai pas compris là…). 60 \item[Chemin observable] On note $P_1\Transition{a}P_2$ avec $a \neq i$ si $P_1\transition{i^*}Q\transition{a}R\transition{i^*}P_2$. $i^*$ q 61 signifie 0 ou plusieurs exécutions de l'action interne. 62 63 Si $P\Transition{a_1}P_1\Transition{a_2}\cdots\Transition{a_n}P_n$ où $a_i \neq i$, on note $P\Transition{t}P_n$ avec $t = a_1; a_2; 64 \dots; a_n$. 65 66 $\hat{t}$ est le chemin obtenu en enlevant toutes les actions internes de $t$. Si $P\transition{t}Q$ alors $P\Transition{\hat{t}}Q$. 67 \item[Trace observable] Une trace observable de $P$ est une exécution partielle observable. 68 \end{description} 69 70 \section{LOTOS} 71 72 \def\fakerowspace{&&&&\\} 73 \hspace{-2.75cm} 74 \begin{tabular}{|lllcl|} 75 \hline 76 % 77 \fakerowspace 78 \multirow{1}{2cm}{Action prefix} & \multirow{1}{*}{$;:A\times P \rightarrow P$} 79 & $\text{ACT}$ & $\frac{\vphantom{P\transition{a}P'}}{a;P\transition{a}P}$ & $a \in \GUi$ \\ 80 \fakerowspace 81 \hline 82 % 83 \fakerowspace 84 \multirow{3}{2cm}{Choice} & \multirow{3}{*}{$[]:P\times P \rightarrow P$} 85 & $\text{CHOICE}_1$ & $\frac{P\transition{a}P'}{P[]Q\transition{a}P'}$ & $a \in \GUi$ \\ 86 \fakerowspace 87 & & $\text{CHOICE}_2$ & $\frac{Q\transition{a}Q'}{P[]Q\transition{a}Q'}$ & $a \in \GUi$ \\ 88 \fakerowspace 89 \hline 90 % 91 \fakerowspace 92 \multirow{3}{2cm}{Composition parallèle indépendante} & \multirow{3}{*}{$|||:P\times P \rightarrow P$} 93 & $\text{COM}_1$ & $\frac{P\transition{a}P'}{P|||Q\transition{a}P'|||Q}$ & $a \in \GUi$ \\ 94 \fakerowspace 95 & & $\text{COM}_2$ & $\frac{Q\transition{a}Q'}{P|||Q\transition{a}P|||Q'}$ & $a \in \GUi$ \\ 96 \fakerowspace 97 \hline 98 % 99 \fakerowspace 100 \multirow{5}{2cm}[-2mm]{Synchro totale} & \multirow{5}{*}[-2mm]{$||:P\times P \rightarrow P$} 101 & $\text{COMP}_1$ & $\frac{P\transition{a}P'\;\wedge\; Q\transition{a}Q'}{P||Q\transition{a}P'||Q'}$ & $a \in \GUi$ \\ 102 \fakerowspace 103 & & $\text{COMP}_{i1}$ & $\frac{P\transition{i}P'}{P||Q\transition{i}P'||Q}$ & \\ 104 \fakerowspace 105 & & $\text{COMP}_{i2}$ & $\frac{Q\transition{i}Q'}{P||Q\transition{i}P||Q'}$ & \\ 106 \fakerowspace 107 \hline 108 % 109 \fakerowspace 110 \multirow{5}{2cm}[-2mm]{Synchro sur un ensemble $S \subseteq G$ de portes visibles} & \multirow{5}{*}[-2mm]{$|[S]|:P\times\mathcal{P}(G)\times P \rightarrow P$} 111 & $\text{SYNC}_1$ & $\frac{P\transition{a}P'}{P|[S]|Q\transition{a}P'|[S]|Q}$ & $a \in G, a \not\in S, a \neq i$ \\ 112 \fakerowspace 113 & & $\text{SYNC}_2$ & $\frac{P\transition{a}P'}{P|[S]|Q\transition{a}P'|[S]|Q}$ & $a \in G, a \not\in S, a \neq i$ \\ 114 \fakerowspace 115 & & $\text{SYNC}_3$ & $\frac{P\transition{a}P'\;\wedge\; Q\transition{a}Q'}{P|[S]|Q\transition{a}P'|[S]|Q'}$ & $a \in S, a \neq i$ \\ 116 \fakerowspace 117 \hline 118 % 119 \fakerowspace 120 \multirow{3}{2cm}{Rendre une action invisible} & \multirow{3}{*}{$\text{\small hide}\dots\text{\small{}in}:\mathcal{P}(G)\times P \rightarrow P$} 121 & $\text{HIDE}_1$ & $\frac{P\transition{a}P'}{(\text{\small hide }a\text{\small{} in }P)\transition{i}(\text{\small hide }a\text{\small{} in }P')}$ & $a \in G, a \neq i$ \\ 122 \fakerowspace 123 & & $\text{HIDE}_2$ & $\frac{P\transition{i}P'}{(\text{\small hide }a\text{\small{} in }P)\transition{i}(\text{\small hide }a\text{\small{} in }P')}$ & $a \in G, a \neq i$ \\ 124 \fakerowspace 125 \hline 126 % 127 \fakerowspace 128 \multirow{1}{2cm}{Renommage} & \multirow{1}{*}{$P[\dots]:P\times G \times G \rightarrow P$} 129 & $\text{REN}$ & $\frac{P[a]\transition{a}P'[a]}{P[p]\transition{b}P'[b]}$ & $\begin{array}{ll}a \in G,& a \neq i\\b \in G,& b \neq i\end{array}$ \\ 130 \fakerowspace 131 \hline 132 % 133 \end{tabular} 134 135 \clearpage 136 \section{Comparaison de LTS} 137 138 \subsection{Équivalence forte $\forte$} 139 140 Def. $P \forte Q\si \forall a \in \GUi,\quad \left(P \transition{a} P'\right) \Rightarrow \left(\exists\, Q \transition{a} Q' \;\wedge\; P' \forte Q'\right)$, et vice versa de $Q$ vers $P$~: $\left(Q \transition{a} Q'\right) \Rightarrow \left(\exists\, P \transition{a} P' \;\wedge\; P' \forte Q'\right)$ 141 142 En français ça donne~: quand $P$ fait une action, $Q$ sait la faire aussi, et vice versa, donc $Q$ est capable de simuler $P$, et $P$ est 143 capable de simuler $Q$. On appelle ça la bisimulation. 144 145 Si $P$ évolue en interne, $Q$ \emph{doit} évoluer en interne. 146 147 L'équivalence forte permet de tester si deux processus ont le même degré d'indéterminisme externe. 148 149 \subsection{Équivalence observationnelle $\observationnelle$} 150 151 Def. $P \observationnelle Q\si \forall a \in \GUi,\quad \left(P\transition{a}P'\right) \Rightarrow \left(\exists\, 152 Q\Transition{\hat{a}}Q' \;\wedge\; P' \observationnelle Q'\right)$ et vice vesa de $Q$ vers $P$~: $\left(Q\transition{a}Q'\right) 153 \Rightarrow \left(\exists\, P\Transition{\hat{a}}P' \;\wedge\; P' \observationnelle Q'\right)$. 154 155 Si $P$ évolue en interne, $Q$ \emph{peut ne pas} évoluer en interne. 156 157 Si $P$ fait une action, $Q$ peut faire beaucoup de $\transition{i}$, mais doit faire l'action. 158 159 L'équivalence observationnelle ne détecte pas tous les livelock. $P$ et $Q$ sont observationnellement équivalents alors que Q peut refuser 160 $b$ indéfiniment et toujours faire i. 161 162 $$P\transition{a}\transition{b} \quad\observationnelle\quad Q\transition{a}\tikz[remember picture]{\node[coordinate] (ab) {};}\transition{b}$$ 163 \begin{tikzpicture}[remember picture, overlay] 164 \node[coordinate,yshift=1mm] (abs) at (ab) {}; 165 \draw (abs) edge[->,out=45,in=135,looseness=1,loop,distance=0.8cm,shorten <=1mm, shorten >=1mm] node[fill=white,inner sep=1.5pt] {\scriptsize $i$} (abs); 166 \end{tikzpicture} 167 168 \subsection{Congruence opérationnelle $=$} 169 170 Def. $P=Q \si \forall a \in \GUi,\quad \left(P\transition{a}P'\right) \Rightarrow \left(\exists\, Q\Transition{a}Q' 171 \;\wedge\; P' \observationnelle Q'\right)$ et vice versa de $Q$ vers $P$~: $\left(Q\transition{a}Q'\right) \Rightarrow \left(\exists\, 172 P\Transition{a}P' \;\wedge\; P' \observationnelle Q'\right)$. 173 174 La différence avec l'équivalence opérationnelle est le $Q\Transition{a}Q'$ au lieu de $Q\Transition{\hat{a}}Q'$. Il est à noter qu'une fois 175 qu'on a vérifié que la première transition n'était pas l'action invisible, on utilise l'équivalence observationnelle. 176 177 Cela a pour but d'avoir $\transition{a}\transition{b}\neq\transition{i}\transition{a}\transition{b}$, mais 178 $\transition{a}\transition{b}=\transition{a}\transition{i}\transition{b}$. 179 180 Cependant, comme pour l'équivalence observationnelle, on ne détecte pas tous les livelock (même exemple que ci-dessus). 181 182 183 \subsection{Simulation} 184 185 Def. $P \simule Q \si \forall a \in \GUi,\quad \left(Q\transition{a}Q'\right) \Rightarrow \left(\exists\, P\transition{a}P' \;\wedge\; P' 186 \simule Q'\right)$. On dit \og $P$ simule $Q$\fg. 187 188 Attention, la bisimulation $P \forte Q$ n'est pas $\left(P \simule Q \;\wedge\; P \estsimulepar Q\right)$, car dans simul, à la fin on a $P' 189 \simule Q'$, alors que dans la bisimulation on a $P' \forte Q'$. La bisimulation $P \forte Q$ est donc une condition plus forte que la 190 simulation mutuelle de P et Q $\left(P \simule Q \;\wedge\; P \estsimulepar Q\right)$. 191 192 \subsection{Force des comparaisons} 193 194 $$ P \forte Q \Rightarrow P = Q \Rightarrow P \observationnelle Q $$ 195 196 \clearpage 197 \subsection{Conformité $\conf$} 198 199 Les comparaisons des sections précédentes ne détectent pas tous les livelock, et nécessitent une description complète de la spécification, 200 car ces relations sont symmétriques. On cherche donc une relation assymétrique de conformité, $P\conf S$ qui nous permettra de dire que $P$ 201 est une implantation correcte de $S$. 202 203 \begin{description} 204 \item[must] On écrit $S\text{ must }A\text{ after }t$ pour dire que $S$ doit accepter les actions de l'ensemble $A$ après le chemin $t$. 205 206 Def. $Q\text{ must }A\text{ after }t \si \forall Q \Transition{t} Q',\quad \forall a \in A, \quad Q'\transition{a}Q"$. 207 208 $\Acc(P,t)$ est l'ensemble des actions que $P$ doit accepter après $t$. 209 210 Def. $\Acc(P,t) = \left\{X \subseteq G | \exists P', P \Transition{t} P', \forall x \in X, P' \transition{x} P"\right\} $ 211 \item[may refuse] On écrit $P\text{ may refuse }A\text{ after }t$ pour dire que $P$ peut refuser une des actions de $A$\footnote{\dots ou 212 toutes les actions de $A$, selon d'autres définitions, mais pas ici.} après le chemin $t$. 213 214 Def. $Q\text{ may refuse }A\text{ after }t \si \forall Q \Transition{t} Q',\quad \exists a \in A, \quad Q'\nottransition{a}$. 215 216 $\Ref(P,t)$ est l'ensemble des actions que $P$ peut (doit?) refuser après $t$. 217 218 Def. $\Ref(P,t) = \left\{X \subseteq G | \exists P', P \Transition{t} P', \forall x \in X, P' \nottransition{x}\right\} $ 219 \end{description} 220 221 \def\myfnote{\footnote{Je ne sais pas trop si c'est $\forall A \subseteq G$ ou $\forall A \subseteq \GUi$.}}% 222 $$ 223 P \conf S\si\forall A \subseteq G\myfnote,\quad S\text{ must }A\text{ after }t \Rightarrow P\text{ must }A\text{ after }t 224 $$ 225 226 En prennant la contraposée, on obtient un test de conformité (équivalent à la définition ci-dessus)~: 227 228 $$ 229 P \conf S\si\forall t \in \Tr(S),\quad P\text{ may refuse }A\text{ after }t \Rightarrow S\text{ may refuse }A\text{ after }t 230 $$ 231 232 Autrement dit, 233 234 $$ 235 P \conf S\si\forall t \in \Tr(S),\quad \Ref(P,t) \subseteq \Ref(S,t) 236 $$ 237 238 Encore une formulation~: $\forall p, p \in \text{vivacité}(S) \Rightarrow p \in \text{vivacité}(P)$, c'est-à-dire $P$ préserve les 239 propriétés de vivacité de $S$, c'est-à-dire $S\text{ doit accepter }A\text{ après }t \Rightarrow P\text{ doit accepter }A\text{ après }t$, 240 c'est-à-dire $P \conf S$ (P conforme à S). 241 242 Par rapport aux autres relations (attention, ce sont des implications, pas forcément vraies dans l'autre sens)~: 243 \begin{gather*} 244 P = Q \Rightarrow P \conf Q \;\wedge\; Q \conf P\\ 245 P = Q \Rightarrow \Tr(P) = \Tr(Q)\\ 246 \end{gather*} 247 248 \subsection{En français…} 249 250 $P\conf Q$ signifie~: 251 \begin{itemize} 252 \item P est plus déterministe que Q 253 \item P se bloque moins souvent que Q 254 \item P refuse moins souvent que Q 255 \end{itemize} 256 257 \section{Raffine} 258 259 \begin{gather*} 260 S_1\text{ raffine } S_0\si \forall I \in \text{ Implémentations},\quad \left(I \conf S_1 \Rightarrow I \conf S_0\right)\\ 261 \text{red} = \conf \cap \subseteq_{\Tr}\\ 262 \text{ext} = \conf \cap \supseteq_{\Tr} 263 \end{gather*} 264 265 \begin{figure} 266 \centering 267 \begin{tikzpicture}[scale=0.5] 268 \draw (0,0) circle (6); 269 \node at (0,-4) {$\conf$}; 270 \draw (-1.5,1) circle (2); 271 \node at (-2.5,1) {red}; 272 \draw (1.5,1) circle (2); 273 \node at (2.5,1) {ext}; 274 \draw (1.5,1) circle (3); 275 \draw (1.5,-1.5) -- (6,-5); 276 \node[anchor=west] at (6,-5) {confrest = raffinement}; 277 \draw (0,1) -- (6,-3); 278 \node[anchor=west] at (6,-3) {te = équivalence de test}; 279 \end{tikzpicture} 280 \end{figure} 281 282 \section{Autres notes} 283 284 \begin{description} 285 \item[Vivacité] L'airbag \emph{doit} se déclencher en cas de choc. 286 \item[Sûreté] Les portes \emph{ne doivent pas} s'ouvrir si la cabine d'ascenceur n'est pas là. 287 \end{description} 288 289 Principe d'\emph{équité}~: «Une action qui se propose infiniment souvent finira par être acceptée». 290 291 \section{Exemples de LTS} 292 293 \begin{figure}[h] 294 \centering 295 \begin{tikzpicture}[node distance=5mm] 296 \node (b0) {$B_0$}; 297 \node[below=of b0] (b1) {$B_1$}; 298 \node[below=of b1] (b2) {$B_2$}; 299 \node[below=of b2] (b1p) {$B_1'$}; 300 \node[below=of b1p] (b2p) {$B_2'$}; 301 \node[at=(b0), xshift=1.5cm, coordinate] (b0r) {}; 302 303 \draw[->] (b0) -- node[right] {$\text{inp}_1$} (b1); 304 \draw[->] (b1) -- node[right] {$\text{inp}_2$} (b2); 305 \draw[->] (b2) -- node[right] {$\text{outp}_1$} (b1p); 306 \draw[->] (b1p) -- node[right] {$\text{inp}_1$} (b2p); 307 308 \draw[->] (b1) edge[bend left] node[left] {$\text{outp}_1$} (b0); 309 \draw[->] (b2p) edge[bend left] node[left] {$\text{outp}_2$} (b1); 310 311 \draw[->] (b1p) -| node[below] {$\text{outp}_2$} (b0r) -- (b0); 312 % \draw[->] (p) -- node[right,near start] {a} (r); 313 % \draw[->] (q) -- node[above] {b} (stop1); 314 % \draw[->] (r) -- node[above] {c} (stop2); 315 \end{tikzpicture} 316 \caption{File d'attente à deux places} 317 \end{figure} 318 319 \end{document}