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)
Pourquoi cette distinction ne peut pas apparaitre
dans le graphe de classes construit par défaut par Tina
(option -W) ?
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.