314 lines
12 KiB
TeX
Executable File
314 lines
12 KiB
TeX
Executable File
\documentclass[a4paper,french,12pt]{article}
|
|
\usepackage{geometry}
|
|
\geometry{a4paper, top=2cm, bottom=2.0cm, left=2.4cm, right=2.47cm}
|
|
\usepackage[frenchb]{babel}
|
|
\usepackage[utf8]{inputenc}
|
|
\usepackage[T1]{fontenc}
|
|
\usepackage{amsmath}
|
|
\usepackage{amssymb}
|
|
\usepackage{enumerate}
|
|
\usepackage{centernot}
|
|
\usepackage{multirow}
|
|
\usepackage{graphicx}
|
|
\usepackage{tikz}
|
|
\usetikzlibrary{positioning,calc,chains}
|
|
\def\P{\mathcal{P}}
|
|
\def\GUi{G \cup \{i\}}
|
|
\def\nottransition#1{\stackrel{#1}{\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\simuleobs\gtrapprox
|
|
\let\estsimulepar\gtrsim
|
|
\begin{document}
|
|
|
|
\section{Files d'attente et équivalences}
|
|
\subsection{$B2err\simule B1$}
|
|
|
|
$B2err$ simule $B1$ car~:
|
|
\begin{itemize}
|
|
\item $B2err \simule B1$~:
|
|
\begin{itemize}
|
|
\item $B1\transition{inp} outp;B1$, et il existe $B2err\transition{inp}outp;B2err$.
|
|
\item Il faut donc que $outp;B2err \simule outp;B1$.
|
|
\end{itemize}
|
|
\item $outp;B2err \simule outp;B1$~:
|
|
\begin{itemize}
|
|
\item $outp;B1\transition{outp}B1$, et il existe $outp;B2err\transition{outp}B2err$.
|
|
\item Il faut donc que $B2err \simule B1$, ce qui est notre premier point.
|
|
\end{itemize}
|
|
\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}
|
|
|
|
\subsection{$B2seq \observationnelle B2par$}
|
|
|
|
{\raggedright
|
|
$B2seq$ et $B2par$ sont observationnellement équivalents car~:
|
|
\begin{itemize}
|
|
\item $B2s \observationnelle B2par$~:
|
|
\begin{itemize}
|
|
\item $B2s\transition{inp} B21$,
|
|
et il existe $B2par \Transition{\hat{inp}} (i;B1[inp,i] \ |[i]|\ B1[i,outp])$
|
|
et $B2par \Transition{\hat{inp}} (B1[inp,i] \ |[i]|\ outp;B1[i,outp])$.
|
|
\item Dans l'autre sens,
|
|
$B2par \transition{inp} (i;B1[inp,i] \ |[i]|\ B1[i,outp])$
|
|
et il existe $B2s\transition{inp} B21$.
|
|
\item Il faut donc que $B21 \observationnelle (i;B1[inp,i] \ |[i]|\ B1[i,outp])$.
|
|
\end{itemize}
|
|
\item $B21 \observationnelle (i;B1[inp,i] \ |[i]|\ B1[i,outp])$~:
|
|
\begin{itemize}
|
|
\item $B21 \transition{inp} outp;B21$,
|
|
et il existe
|
|
$(i;B1[inp,i] \ |[i]|\ B1[i,outp]) \Transition{\hat{inp}} (i;B1[inp,i] \ |[i]|\ outp;B1[i,outp])$
|
|
\item $B21 \transition{outp} B2s$, et
|
|
et il existe
|
|
$(i;B1[inp,i] \ |[i]|\ B1[i,outp]) \Transition{\hat{outp}} (B1[inp,i] \ |[i]|\ B1[i,outp])$,
|
|
autrement dit
|
|
$(i;B1[inp,i] \ |[i]|\ B1[i,outp]) \Transition{\hat{outp}} B2par$
|
|
\item Dans l'autre sens,
|
|
$(i;B1[inp,i] \ |[i]|\ B1[i,outp]) \transition{i} (B1[inp,i] \ |[i]|\ outp;B1[i,outp])$,
|
|
mais comme on $\hat{i}$ est le chemin vide, on n'aura rien à vérifier sur $B21$.
|
|
\item Il faut donc que $outp;B21 \observationnelle (i;B1[inp,i] \ |[i]|\ outp;B1[i,outp])$,
|
|
et que $B2s \observationnelle B2par$. Cette deuxième condition est en fait notre premier point.
|
|
\end{itemize}
|
|
\item $outp;B21 \observationnelle (i;B1[inp,i] \ |[i]|\ outp;B1[i,outp])$~:
|
|
\begin{itemize}
|
|
\item $outp;B21 \transition{outp}B21$,
|
|
et il existe
|
|
$(i;B1[inp,i] \ |[i]|\ outp;B1[i,outp]) \Transition{\hat{outp}} (i;B1[inp,i] \ |[i]|\ B1[i,outp])$.
|
|
\item Il faut donc que $B21 \observationnelle (i;B1[inp,i] \ |[i]|\ B1[i,outp])$, ce qui est notre deuxième point.
|
|
\end{itemize}
|
|
\end{itemize}
|
|
}
|
|
|
|
\subsection{$B2ent = B2par$}
|
|
|
|
Étant donné que $B2ent$ et $B2par$ ne commencent pas par l'action
|
|
interne, tester leur égalité au sens de la congruence observationnelle
|
|
revient à tester s'ils sont observationnellement équivalents.
|
|
|
|
On applique donc la même méthode que dans la section précédente, avec
|
|
les équivalences suivantes~:
|
|
|
|
{\raggedright
|
|
\begin{itemize}
|
|
\item Pour que $B2ent = B2par$, il faut qu'après $inp$ (la seule
|
|
action que les systèmes peuvent exécuter dans leurs états respectifs),
|
|
$(outp;B1[inp;outp] ||| B1[inp;outp]) \observationnelle (i;B1[inp;i]\ |[i]|\ B1[i,outp])$.
|
|
\item Pour cela, il faut qu'après $outp$,
|
|
$(B1[inp;outp] ||| B1[inp;outp]) \observationnelle (B1[inp;i]\ |[i]|\ B1[i,outp])$,
|
|
autrement dit $B2ent = B2par$, ce qui est une condition plus faible que le premier point.
|
|
|
|
Il faut aussi qu'après $inp$,
|
|
$(outp;B1[inp;outp] ||| outp;B1[inp;outp]) \observationnelle (i;B1[inp;i]\ |[i]|\ outp;B1[i,outp])$.
|
|
|
|
Dans l'autre sens, on peut ignorer ce qui se passe après le $i$ de
|
|
$(i;B1[inp;i]\ |[i]|\ B1[i,outp])$, car $\hat{i}$ est le chemin vide,
|
|
donc pas de conditions sur $(outp;B1[inp;outp] ||| B1[inp;outp])$.
|
|
\item Occupons-nous de
|
|
$(outp;B1[inp;outp] ||| outp;B1[inp;outp]) \observationnelle (i;B1[inp;i]\ |[i]|\ outp;B1[i,outp])$.
|
|
Dans ces états, les systèmes ne peuvent faire qu'$outp$. Il faut donc qu'après $outp$,
|
|
$(outp;B1[inp;outp] ||| B1[inp;outp]) \observationnelle (i;B1[inp;i]\ |[i]|\ B1[i,outp])$,
|
|
ce qui correspond au deuxième point.
|
|
\end{itemize}
|
|
}
|
|
|
|
\subsection{$B2par \simuleobs B1$}
|
|
|
|
$B2par$ simule observationnellement $B1$ car~:
|
|
|
|
\begin{itemize}
|
|
\item $B1\transition{inp}outp;B1$, et il existe
|
|
$B2par\Transition{\hat{inp}}(i;B1[inp,i]\ |[i]| B1[i;outp])$ et
|
|
$B2par\Transition{\hat{inp}}(B1[inp,i]\ |[i]| outp;B1[i;outp])$.
|
|
Il suffit donc que soit $(i;B1[inp,i]\ |[i]| B1[i;outp]) \simuleobs outp;B1$,
|
|
soit $(B1[inp,i]\ |[i]| outp;B1[i;outp]) \simuleobs outp;B1$. On prend
|
|
\item On prend cette deuxième possibilité.
|
|
$outp;B1 \transition{outp} B1$, et il existe
|
|
$(B1[inp,i]\ |[i]| outp;B1[i;outp])\Transition{\hat{outp}}(B1[inp,i]\ |[i]| B1[i;outp])$,
|
|
autrement dit
|
|
$(B1[inp,i]\ |[i]| outp;B1[i;outp])\Transition{\hat{outp}}B2par$, notre premier point.
|
|
\end{itemize}
|
|
|
|
\subsection{$\not B2par \conf B1$}
|
|
|
|
Pour que $B2par$ soit conforme à $B1$, car pour toute trace $t$ de $B1$,
|
|
$\Acc(B2par) \subset\subset \Ref(B1)$.
|
|
|
|
\begin{itemize}
|
|
\item Pour la trace $\emptyset$, $\Acc(B2par) = \Acc(B1) = \{\{inp\}\}$.
|
|
\item Pour la trace $inp$, $\Acc(B2par) = \{\{\}, \{inp,outp\}\}$, mais $\Acc(B1) = \{\{outp\}\}$.
|
|
\item Pour la trace $inp;outp$, on est revenu aux mêmes états que la trace $\emptyset$.
|
|
\end{itemize}
|
|
Pour le point 2 $\forall X \in \{\{\}, \{inp,outp\}\},\quad \{outp\} \not\subseteq X$, et donc $\neg(B2par \conf B1)$
|
|
|
|
\section{Exercice de l'atelier}
|
|
|
|
\subsection{Question 1}
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=15cm]{question1}
|
|
\end{figure}
|
|
|
|
\subsection{Question 2}
|
|
|
|
\begin{verbatim}
|
|
Maillet[prendM,poseM] := prendM;MailletOcc[prendM,poseM]
|
|
MailletOcc[prendM,poseM] := poseM;Maillet[prendM,poseM]
|
|
\end{verbatim}
|
|
|
|
\subsection{Question 3}
|
|
|
|
\begin{verbatim}
|
|
UtiliseMarteau[ent,sortie,prend,pose,prendM,poseM](travail:TRAVAIL) :=
|
|
prend;sortie!fait(travail);pose;
|
|
Ouvrier[ent,sortie,prend,pose,prendM,poseM]
|
|
\end{verbatim}
|
|
|
|
\begin{verbatim}
|
|
UtiliseMaillet[ent,sortie,prend,pose,prendM,poseM](travail:TRAVAIL) :=
|
|
prendM;sortie!fait(travail);poseM;
|
|
Ouvrier[ent,sortie,prend,pose,prendM,poseM]
|
|
\end{verbatim}
|
|
|
|
\begin{verbatim}
|
|
Commence[ent,sortie,prend,pose,prendM,poseM](travail:TRAVAIL) :=
|
|
[facile(travail)] ->
|
|
sortie!fait(travail);
|
|
Ouvrier[ent,sortie,prend,pose,prendM,poseM]
|
|
[]
|
|
[difficile(travail)] ->
|
|
UtiliseMarteau[ent,sortie,prend,pose,prendM,poseM](travail)
|
|
[]
|
|
[(not(facile(travail)) and not(difficile(travail)))] ->
|
|
UtiliseOutil[ent,sortie,prend,pose,prendM,poseM](travail)
|
|
\end{verbatim}
|
|
|
|
\begin{verbatim}
|
|
Ouvrier[ent,sortie,prend,pose,prendM,poseM] :=
|
|
ent?travail:TRAVAIL;
|
|
Commence[ent,sortie,prend,pose,prendM,poseM](travail)
|
|
\end{verbatim}
|
|
|
|
\begin{verbatim}
|
|
Atelier[ent,sortie] :=
|
|
hide prend,pose,prendM,poseM in
|
|
(
|
|
(
|
|
Marteau[prend,pose]
|
|
|||
|
|
Maillet[prendM,poseM]
|
|
)
|
|
|[prend,pose,prendM,poseM]|
|
|
(
|
|
Ouvrier[ent,sortie,prend,pose,prendM,poseM]
|
|
|||
|
|
Ouvrier[ent,sortie,prend,pose,prendM,poseM]
|
|
)
|
|
)
|
|
\end{verbatim}
|
|
|
|
\subsection{Question 4}
|
|
|
|
Nécessite l'outil \verb!casear!.
|
|
|
|
\subsection{Question 5}
|
|
|
|
\begin{verbatim}
|
|
AtelierV[ent,sortie] :=
|
|
hide e,s in
|
|
Verificateur[ent,sortie,e,s]
|
|
|[e,s]|
|
|
Atelier[e,s]
|
|
\end{verbatim}
|
|
|
|
La composition parallèle générale synchronisant les ouvriers et le
|
|
vérificateur est la synchronisation sur l'ensemble de portes
|
|
$\{ent,sortie\}$ de l'atelier sans vérificateur.
|
|
|
|
On place le vérificateur «entre» les ouvriers et l'environnement~: Si
|
|
un travail est mal fait, le vérificateur le défait et le repasse à
|
|
l'entrée des ouvriers, sinon, il l'envoie vers la sortie de
|
|
l'environnement. À tout moment, il peut récupérer du travail depuis
|
|
l'environnement, et le passer aux ouvriers. Nous avons choisi de ne
|
|
pas limiter le nombre de fois que le vérificateur peut laisser les
|
|
ouvriers obtenir du travail depuis l'environnement, puisque nous ne
|
|
savons pas combien de travaux peuvent être sur les tapis roulants
|
|
$ent$ et $sortie$ sans que le vérificateur y ait encore eu accès.
|
|
|
|
\begin{verbatim}
|
|
Verificateur[ent,sortie,e,s] :=
|
|
(
|
|
s?produit:PRODUIT;
|
|
[not(correct(produit))] ->
|
|
e!defait(produit);Verificateur[ent,sortie,e,s]
|
|
[]
|
|
[correct(produit)] ->
|
|
sortie!produit;Verificateur[ent,sortie,e,s]
|
|
)
|
|
[]
|
|
(
|
|
ent?travail:TRAVAIL;
|
|
e!travail;
|
|
Verificateur[ent,sortie,e,s]
|
|
)
|
|
\end{verbatim}
|
|
|
|
\subsection{Question 6}
|
|
|
|
$Assemble$ n'est pas observationnellement équivalent à $Atelier$, car
|
|
après avoir exécuté l'action $ent$, $Atelier$ peut encore exécuter
|
|
$ent$ (puisqu'il y a deux ouvriers, qui peuvent accepter deux
|
|
travaux), tandis que $Assemble$ ne pourra exécuter que $sortie$.
|
|
|
|
{\raggedright
|
|
\begin{itemize}
|
|
\item $Atelier[\dots] \transition{ent} (\dots) \ |[\dots]|\ (Commence[\dots] ||| Ouvrier[\dots])$,
|
|
et il existe
|
|
$Assemble[\dots] \transition{ent} Assembler[\dots]$. Il faudrait que
|
|
$(\dots) \ |[\dots]|\ (Commence[\dots] ||| Ouvrier[\dots]) \observationnelle Assembler[\dots]$.
|
|
\item Mais
|
|
$(\dots) \ |[\dots]|\ (Commence[\dots] ||| Ouvrier[\dots]) \not\observationnelle Assembler[\dots]$
|
|
car $(\dots) \ |[\dots]|\ (Commence[\dots] ||| Ouvrier[\dots]) \transition{ent} (\dots) \ |[\dots]|\ (Commence[\dots] ||| Commence[\dots])$
|
|
tandis que $Assembler[\dots] \nottransition{ent}$.
|
|
\end{itemize}
|
|
}
|
|
\subsection{Question 7}
|
|
|
|
Nécessite l'outil \verb!aldebaran!.
|
|
|
|
\end{document}
|