66 lines
2.6 KiB
TeX
Executable File
66 lines
2.6 KiB
TeX
Executable File
\documentclass[a4paper,french,9pt]{article}
|
|
\usepackage[reset]{geometry}
|
|
\geometry{a4paper, top=2cm, bottom=2.0cm, left=4.4cm, right=4.47cm}
|
|
\usepackage[frenchb]{babel}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath}
|
|
\usepackage{amssymb}
|
|
\usepackage{enumerate}
|
|
%\usepackage{centernot}
|
|
\usepackage{multirow}
|
|
\usepackage{tikz}
|
|
\usetikzlibrary{positioning,calc,chains,intersections}
|
|
\def\P{\mathcal{P}}
|
|
\def\GUi{G \cup \{i\}}
|
|
\def\nottransition#1{\stackrel{#1}{\not\longrightarrow}}%\centernot\longrightarrow}}
|
|
\def\transition#1{\stackrel{#1}{\longrightarrow}}
|
|
\def\Transition#1{\stackrel{#1}{\Longrightarrow}}
|
|
\def\forte{\sim}
|
|
\def\observationnelle{\approx}
|
|
\def\conf{\ \text{conf}\ }
|
|
\DeclareMathOperator{\Tr}{Tr}
|
|
\DeclareMathOperator{\Acc}{Acc}
|
|
\DeclareMathOperator{\Ref}{Ref}
|
|
\def\si{\quad\text{si}\quad}
|
|
\let\simule\gtrsim
|
|
\let\estsimulepar\gtrsim
|
|
\begin{document}
|
|
|
|
\section{Files d'attente et équivalences}
|
|
\subsection{$B2err\simule B1$}
|
|
|
|
\begin{itemize}
|
|
\item $B1\transition{inp} outp;B1$, et il existe $B2err\transition{inp}outp;B2err$
|
|
\item $outp;B1\transition{outp}B1$, et il existe $outp;B2err\transition{outp}B2err$
|
|
\item et on retourne sur $B1$ et $B2err$.
|
|
\end{itemize}
|
|
|
|
\subsection{$\neg\ B2err\conf B1$}
|
|
$B2err$ n'est pas conforme à $B1$ car $Ref(B2err, inp) = \{\{inp\}, \{outp\}\}$, alors que $Ref(B1,inp) = \{\{outp\}\}$,
|
|
et donc on n'a pas $Ref(B2err, inp) \subseteq Ref(B1, inp)$.
|
|
|
|
\subsection{$B2par$ respecte-t-il la spécification $B_20$ ?}
|
|
$B2par$ respecte la spécification $B_20$~:
|
|
\begin{enumerate}[i)]
|
|
\item Un message émis a toujours été reçu : pour qu'un message soit
|
|
émis par la porte $outp$ du $B1$ de droite, il faut qu'il ait été
|
|
reçu par la porte $mid$ du $B1$ de droite, synchronisé sur la porte
|
|
$mid$ du $B1$ de gauche. Pour que le message soit émis sur la porte
|
|
$mid$ du $B1$ de gauche, il faut qu'il ait au préalable été reçu sur
|
|
la porte $inp$ du $B1$ de gauche.
|
|
\item Lorsqu'un $B1$ reçoit un message, il refuse les $inp$ jusqu'à ce
|
|
qu'il ait effectué un $outp$. Comme la porte $outp$ du $B1$ de
|
|
gauche est synchronisée sur la porte $inp$ du $B1$ de droite, cela
|
|
signifie que si les deux $B1$ «contiennent» un message, celui de
|
|
droite n'accepera pas d'$inp$ tant qu'il n'aura pas effectué
|
|
d'$outp$, et en cascade, celui de gauche ne pourra pas faire
|
|
d'$outp$ tant que celui de droite n'aura pas été «vidé», et donc
|
|
celui de gauche refusera les $inp$. On ne pourra donc pas effectuer
|
|
un $inp$ sur le $B1$ de gauche tant que les deux $B1$ «contiendront»
|
|
un message, et il ne pourra donc pas y avoir plus de deux messages
|
|
dans la file.
|
|
\end{enumerate}
|
|
|
|
\end{document}
|