MSC I : Réseaux de Petri
Support de cours
TINA : TP1
TP 1
I Allocations de Ressource 1 Client + 2 Gestionnaires de Ressource
Un client (C1) a besoin pour travailler de posséder de manière mutuellement exclusive
deux ressources (R_1,R_2) qui sont
distantes et gérées individuellement par
deux gestionnaires (G_1,G_2).
La communication entre client et gestionnaire
est régie par les messages suivants:
- Req - demande d'accès à la ressource,
- Ack - autorisation d'accès à la ressource,
- Lib - libération de la ressource
Client C1: C1 demande séquentiellement les deux
ressources. Plus précisément, il demande d'abord la ressource R_1, et
lorsqu'il l'a obtenue, il demande la ressource R_2. Il entre en
section critique lorsqu'il possède les deux ressources. Il libère
ensuite en même temps les deux ressources et retourne à son état initial.
Gestionnaire G_j:
A la réception d'un message Req envoyé par le client Ci,
G_j alloue exclusivement la ressource à Ci
(i.e envoi du message Ack à Ci si la ressource est libre,
sinon la requête reste en attente.
A la réception du message Lib, la ressource est libérée.
- Modélisez ce système par un réseau e Petri.
- Le fichier cl1.net représente le comportement commenté du client 1.
Il est décrit sous un format textuel. Sauvez le et ouvrez-le avec nd. Vous pouvez le dessiner via l'ongler edit.
- En vous inspirant du réseau associé au client, modélisez le comportement du gestionnaire 1 (resp 2) dans
un fichier gest1.net (resp gest2.net)
-
Le système global peut etre obtenu en composant les 3 fichiers .net
en un seul fichier en utilisant le format tpn (voir exemple dans
composition.tpn ).
En cas d'erreur de compilation utilisez la commande tina -p
composition.tpn pour voir les erreurs.
- Simulez le système global résultant de la composition à l'aide
du Stepper.
- Construisez son graphe des marquages.
- Assurez vous qu'il est exempt de blocage.
- Assurez vous qu'il est réinitialisable (ici une seule composante fortement connexe
contenant tous les marquages).
II Composition par fusion de transitions
On considère de nouveau le système de la question I.
Proposez une modélisation compositionnelle (avec 3 composants
spécifiques : 1 client et deux gestionnaires) équivalente en terme de
fonctionnement à celle réalisée en I (le réseau obtenu à cette question 3 doit être identique
à celui obtenu à la question 1) mais telle que la
communication entre les trois composants se fasse uniquement par
fusion de transitions (vous n'avez donc plus la possibilité
d'utiliser des places partagées).
III. Allocations de Ressource 2 Clients + 2 Gestionnaires de Ressource
On ajoute au système décrit à la première
question un second client (C2) dont le comportement est décrit ci-dessous:
Client C2: C2 demande séquentiellement les deux
ressources. Plus précisément, il demande d'abord la ressource R_2, et
lorsqu'il l'a obtenue, il demande la ressource R_1. Il entre en
section critique lorsqu'il possède les deux ressources. Il libère
ensuite en même temps les deux ressources et retourne à son état initial.
- Modélisez de façon compositionnelle ce système.
- Simulez-le à l'aide du Stepper.
- A l'aide du stepper, trouvez des scenarios démontrant la possibilité
- d'interblocage.
- de famine (i.e un scenario infini (cyclique) pour lequel un des clients est toujours en attente
- Propriétés d'exclusion mutelle
A titre d'exemple, l'exclusion mutuelle au niveau client peut s'exprimer ainsi :
Pout tout marquage accessible m, m(Cl1_work) + m(Cl2_work) <= 1
- Pourquoi la simulation ne peut pas vous garantir la satisfaction de cette propriété ?
- Comment pourriez-vous vous en assurer en analysant le graphe des marquages ?
- Pour s'en assurer de facon automatique, on va utiliser la technique des
"Observateurs". En vous inspirant de l'exemple vu en cours
(cf Réseau #3 - slide 55/111 du support de cours). Vous ajouterez un nouveau composant (rdp) composé par une seule transition d'observation
( tr pb_mutex Cl1_work Cl2_work -> Cl1_work Cl2_work ) qui sera tirable si et
seulement si cette propriété d'exclusion
est violée.
La propriété d'exclusion mutuelle sera vérifiée ssi
la transition pb_mutex est morte. Pour s'en assurer il suffit donc de construire le graphe des marquages (output verbose) et de vérifier que la transition d'observation est morte.
A faire en fin de série de Tps s'il vous reste du temps.
Procédez de la même façon pour vous assurer que chaque ressource est utilisée en exclusion mutuelle :
- Vous traiterez chaque ressource séparément.
- Vous exprimerez en premier la propriété avec les places du réseau (en fait les places du gestionnaire concerné)
- Vous introduirez la transition d'observation et vous vous assurerez qu'elle est bien morte.