Ecole temps réel (ETR) 2015

Rennes, 24 au 28 août 2015


tina logo

TIme petri
Net Analyzer

laas logo
Chemins d'acces : source /share/ETR2015/TINA/envTINA

Prise en mains Exemples Exos Struct Exos LTL Exos CTL TP Atemporel TP Temporel
TINA : TP1

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 ?