 |
TIme petri |
 |
| Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
TP0
Prise en Mains de TINA
I 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.
Chargez le réseau associé interblocage.ndr
- Exécutez la commande nd interblocage.ndr
- Lancez le simulateur pas à pas (onglet tools: stepper)
- Simulez le fonctionnement du système et retrouvez la situation d'interblocage.
- Quittez le simulateur (onglet file: return to editor)
- Construire le graphe des marquages (onglet tools: reachabilty / marking graph - output verbose)
- Visualisation du graphe des marquages (onglet tools: reachabilty / marking graph - output automaton)
- Ouvril l'automate résultant sous TINA (clic droit - open file in nd)
- Faites apparaitre la barre d'outils de TINA (clic droit dans la fenetre)
- Dessinez le (onglet edit : option draw). Plusieurs heuristiques de placement sont proposées (neato, draw, circo, ...) essayez les. Vous devez d'abord repasser en forme textuelle (onglet edit : option textify).
II 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.
Chargez le fichier planteur.net
- Exécutez la commande nd planteur.net. Le réseau apparait mais sous forme textuelle.
- Lancez le simulateur pas à pas (onglet tools: stepper)
- Simulez le fonctionnement du système
- Quittez le simulateur (onglet file: return to editor)
- Dessinez le réseau (onglet edit : option draw). Vous pouvez améliorer l'esthétique à votre guise.
- Lancez le simulateur pas à pas (onglet tools: stepper)
- Simulez le fonctionnement du système. "Persuadez-vous" qu'il est non borné (i.e, trouvez une séquence répétitive croissante)
- Quittez le simulateur (onglet file: return to editor)
- Construisez le graphe de couverture du réseau (onglet tools: reachabilty /coverabilty graph - output verbose).
- Regardez le fichier résultat. Les places non bornées sont celles qui apparaissent avec un poids = w.
- Dessinez le graphe de couverture (onglet tools: reachabilty /coverabilty graph - output automaton). ...
III Edition du réseau de Petri suivant
- Entrez le réseau en utilisant la forme textuelle
- Entrez le réseau directement en graphique.
- Construisez et dessinez son graphe des marquages.
- Le réseau est-il réinitialisable, quasi-vivant, vivant ?
- Les marquages accessibles présentent une "similitude" .. laquelle ?