Introduction aux Réseaux de Petri (4IS)
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).
A faire en fin de série de Tps s'il vous reste du temps.
III. Allocations de Ressource 2 Clients + 2 Gestionnaires de Ressource
On ajoute au système décrit à la premiè
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 pouvez-vous vous en assurer en analysant le graphe des marquages ?
- Pour s'en assurer de facon automatique: complétez le réseau inital
(cf slide 37 du support de cours)
avec une seule transition d'observation qui sera tirable si et seulement si cette propriété d'exclusion
est violée.
Procédez de la même façon pour vous assurer que chaque ressource est utilisée
en exclusion mutuelle.