 |
TIme petri |
 |
| Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
Exemples de modélisation
Partage de Ressources
Deux processus (banalisés) partagent deux ressources (A et B). L'un des processus se procure d'abord A (OqpA), puis se procure B (OqpAB), il travaille (WorkAB) puis il retourne (en même temps) au repos et libère (FreeAB) les ressources A et B. L'autre processus procède dans l'ordre inverse: obtention de B puis de A.Réseau associé
Contôleur de Base de données
Lecteurs et écrivains en concurrence pour accéder à un e (abstraction) de base de données. Modélisation d' un arbitre (contrôleur) permettant de synchroniser les lecteurs et les écrivains.Réseau associé
La journée d'un planteur de bananes
Le planteur est initialement au champ où il cueille des bananes (en quantité supposé infinie). Il cesse son travail et se met à table pour manger quelques bananes. A la fin du repas, il passe au jardin et jette quelques unes des peaux de bananes mangées. Il part ensuite dormir.Réseau associé
Une histoire de pont
Un groupe de 4 personnes (A,B,C,D) se situe sur la rive gauche d'un fleuve et doit se rendre sur la rive droite.Pour ce faire, ils doivent emprunter un pont mal éclairé qui ne peut supporter qu'une charge de deux personnes.
Le groupe dispose d'une seule lampe de poche.
Chaque traversée du pont nécessite la possession de la lampe. Il est donc nécessaire de ramener la lampe de l'autre coté pour permettre une nouvelle traversée.
Les 4 personnes marchent à une vitesse différente. Les temps de traversée pour chacun des individus est respectivement de 10 min pour A, 5 min pour B, 2 min pour C et 1 min pour D.
-- Ce réseau modélise ce problème. Donnez une interprétation aux différentes places et transitions. Simulez-le. Il comporte une "petite erreur" de modélisation, laquelle ?
-- Quel est le temps minimal pour faire passer les 4 personnes sur la rive droite ?
Une histoire de piscine
Une piscine comporte c cabines pour se changer et p paniers pour déposer ses vétements.-- On n'entre dans le piscine que si une cabine est libre. On attends un panier pour se changer et déposer ses vètements. On libère la cabine et on pénètre dans le bassin.
-- On ne quitte le bassin que si une cabine est libre. On se change et on restitue cabine et panier. On quitte enfin la piscine.
-- Ce réseau modélise le protocole décrit ci-dessus. Voir la légende des places et des transitions ci-dessous. Le protocole choisi pour accéder à la piscine peut conduire à un blocage - et ce indépendamment du nombre de cabines et de paniers. Exhibez une séquence conduisant à un blocage.
|
|