 |
TIme petri |
 |
| Prise en mains | Exemples | Exos Struct | Exos LTL | Exos CTL | TP Atemporel | TP Temporel | |||||||||||
1 Bit Alterné
-
On considère l'exemple du bit alterné représenté ci-dessous
- Recopiez les sources du bit alterné abp.ndr
- Simulez le via nd (nd abp.ndr) en mode atemporel
- Simulez le en mode temporel
- Construisez son graphe des classes en mode verbose (positionner l'option "stopping test" a` none)
- Visulalisez le graphe des classes : il est suffisament petit pour comprendre le fonctionnement global du protocole.
- En utilisant SELT, vérifiez les propriétés décrites dans le fichier abp.ltl
2 John et Frédéric
John va au travail soit en voiture (entre 30 et 40 minutes), ou en bus (au moins 60 minutes). Frédéric part travailler en voiture (entre 20 et 30 minutes), ou en covoiturage (entre 40 et 50 minutes). Aujourd'hui john quitte la maison entre 7H10 et 7H20, et Frédéric arrive au travail entre 8H00 et 8H10. On sait aussi que John arrive au travail entre 10 et 20 minutes après que Frédéric quitte sa maison.- Faire une modélisation séparée des comportements de "tous les jours" de John et Frédéric : un fichier .net pour chacun des composants. Vous simulerez chacun d'eux via le stepper.
- Faire une modélisation d'une horloge représentant les données temporelles absolues du problème. Vous la simulerez via le stepper.
- Faire une modélisation d'une horloge représentant les données temporelles relatives du problème. Vous la simulerez via le stepper.
- Composez les 4 entités (vois all.tpn ) et simulez l'ensemble.
- Ajoutez les contraintes temporelles du jour spécifique directement sur la composition. Votre modélisation vous semble-t-elle correcte ? En utilisant le simulateur, trouvez une scenario où John et Fred arrivent à l'heure au travail.
- Regroupez les differentes contraintes que vous aviez ajoutées directement sur la composition dans un nouveau réseau (contrainte.net).
- Est-il possible que John prenne le bus et Frédéric utilise le covoiturage ? A priori non ! : pour en être sûr, vous pouvez utiliser la techniques des observateurs, une approche plus directe consiste à utiliser la logique temporelle et SELT ( Elements de solution)
3 Propriétés de Branchement
On considère le réseau suivant .Partant de l'état initial, on s'intéresse aux différentes dates de tir de la transition t1. Sans chercher à calculer le graphe des classes de ce réseau, montrez que l'intervalle de tir de t1 ([0,4]) peut-être partitionné en 3 sous-intervalles I1, I2 et I3 de telle façon que lorsque l'on considère Theta, la date de tir de t1:
- Si Theta in I1 alors t2 doit être tirée avant t3.
- Si Theta in I3 alors t3 doit être tirée avant t2.
- Si Theta in I2 alors t3 et t2 sont temporellement indépendantes (t3 et t2 peuvent avoir lieu dans n'importe quel ordre)
En déduire que l'on ne peut pas vérifier avec cette construction des propriétés type CTL (propriétés de branchement)
L'option -A permet d'obtenir précisément des abstractions préservant les propriétés de branchement (et donc CTL).
Regardez le resultat fourni sur cet exemple.