www

bonavero-duperon.tex (11863B)

---

 \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}