MSC I : Réseaux de Petri
Support de cours
TP 3
I Token-ring
On utilise un protocole d'anneau à jeton pour résoudre le problème de l'exclusion mutuelle. Chaque site est composé d'une station et d'un client. La station s'occupe de la circulation du jeton et d'offrir un service d'exclusion mutuelle à son client.
Le client i est régi par trois états:
- idle_i : Client i oisif
- wait_i : Client i en attente de la CS
- work_i : Client i en CS
Le jeton est régi par deux ensembles indexés d'états:
- token_i : Le jeton est disponible sur la station i
- after_i : Le jeton est en transit entre la station i et la station i+1
Architecture de la solution :
Le système est constitué par k sites communicant
de facon asynchrone (cf place partagée : after_i).
Chaque site est composé par une station et un client communicant de facon synchrone : chaque station est en charge des interactions synchrones avec son client (cf transitions partagées : i_work, i_rel) et de la communication asynchrone avec ses stations adjacentes (cf transitions : i_entry, i_exit). Voir details dans la forme textuelle
compo.net
A) Simulation et compréhension du modèle proposé
Le réseau tk4.ndr propose un modèle Petri pour un anneau composé par 4 sites.
Chargez le sous nd.
- Simulez le avec le stepper.
- Son comportement vous semble-t-il a priori correct ?
La solution proposée ne garantit pas l'absence de famine :
un client peut rester indéfiniment en attente pour travailler
(le service fourni par la station devrait assurer qu'il travaillera au bout d'un temps fini et ce n'est pas le cas).
La solution proposée comporte deux erreurs :
(E1) : une station peut être trop égoiste (ne penser qu'à son client) et empêcher de travailler les autres clients.
(E2) : les stations peuvent aussi être trop altruistes et donner toujours la priorité aux autres stations.
- Retrouvez par simulation ces deux comportements.
B) Analyse structurelle du réseau (onglet tools Structural analysis)
- Donnez une interprétation aux invariants de place (P-Semiflows)
Quelles propriétés permettent-ils de déduire ? Peut-on ainsi vérifier
la propriété d'exclusion mutuelle ?
- Donnez une interprétation aux invariants de transitions (T-Semiflows)
Permettaient-ils de prédire les comportements de type (E1) e/ou (E2) ?
Notons une nouvelle fois qu'un invariant de transitions n'assure en rien l'existence d'une séquence
de franchissement de même support.
C) Correction du modèle
Proposez les modifications du comportement des stations de facon à interdire
les comportements pathologiques révélés par les propriétés.
Vous traiterez d'abord E1 puis E2.
Pour E1, vous apporterez la même correction sur chacune des stations.
Pour E2, vous apporterez une correction spécifique
sur chacune des stations.
Pour mettre au point vos corrections, vous travaillerez directement sur la forme graphique de la composition (tk4.ndr).
Vous vous aiderez de la simulation et de l'analyse structurelle pour valider vos corrections.
Indication Quelques extensions utiles pour résoudre cette question
- Un arc inhibiteur permet d'interdire la sensibilisation d'une transition
si sa place d'entree est marquée
(Sous nd, pour obtenir un arc inhibiteur, tracer un arc entre une place et une transition
et choisir l'option inhibitor)
- Il est possible de spécifier des priorités entre des transitions
(Sous nd, il suffit de tracer un arc entre deux transitions)
Expérimentez ces extensions et utilisez les pour obtenir une variante
de la solution que vous aviez initialement proposée.
D) Génération automatique du RdP du Token-Ring
Pour permettre une modélisation paramétrée du
problème, on peut utiliser un programme auxilliaire pour
générer le réseau de Petri correspondant. Le
fichier ctk0 est un script tcl permettant
de générer le réseau associé à une
configuration à k sites.
Le fichier compo.net donne le résultat de ce script pour k =3. Le script utilise la possibilité de travailler de facon compositionelle: on utilise le fait qu'en textuel deux transitions portant le même nom seront fusionnées. On trouve des transitions spécifiques du client, des transistions de la station et des transitions communes à un client et à sa station.
Pour générer un réseau à 8 sites : chargez le script ctk et
exécutez la commande suivante :
./ctk0 8 > ctk0_8.net (ne pas oublier de rendre exécutable le script par la commande chmod +x).
II Réseau de Petri Puzzle à base d'arcs inhibiteurs
et de priorités
Regardez et simulez la solution proposée dans puzzle.ndr
Donnez une interprétation aux transitions t3 et t4 ainsi qu'aux places nbMax et frozen
Quel problème du modèle précédent peut-on ainsi résoudre ?
Proposez une version "équivalente" sans arc inhibiteur.
III Modélisation d'un système paramétré: le diner des philosophes
N philosophes sont assis autour d'une table ronde. Ils sont dans trois états
(pense, attente, dine). Chaque philosophe a besoin de
deux fourchettes pour manger, mais il n'y a qu'une
fourchette par assiette. Ainsi pour manger un philosophe doit prendre la fourchette se trouvant à sa gauche et la fourchette se trouvant à sa droite en deux étapes distinctes. Ainsi à tout moment deux philosophes qui sont l'un à coté de l'autre ne peuvent pas manger simultanément.
En vous inspirant du script fourni, modélisez le diner des
philosophes ; il faut bien sur faire disparaitre l'anneau mais on gardera
un esprit compositionnel en distinguant le comportement du philosophe
(qui ne changera pas durant tout l'exercice) et de son disciple en charge
d'aller chercher et rendre les fourchettes.
Vous simplifierez le problème en supposant que les N
disciples disposent d'un ensemble de N fourchettes banalisées dans
lequel peuvent piocher les deux fourchettes simultanément (V0),
ils piochent les fourchettes l'une après l'autre (V1), les fourchettes
sont individualisées et sont prises séquentiellement (V2).
Note: Pour les versions V0 et V1, on autorisera 2 philosophes
voisins à manger en même temps.
Pour les versions V0 et V1 :
- Proposez une modélisation compositionnelle
des disciples et du tas de fourchettes
- Ecrire le script associé.
(Vous ne chercherez pas à garantir l'absence de famine)
(Optionnel) Proposez une solution pour la version V2.