TPs Modèles Temporels - TP TINA / TP UPPAAL

Support de Cours       Revisions (Videos + Annale)

Pour faciliter la démonstration, vous ouvrirez une visio zoom directement via votre navigateur et vous vous connecterez en utilisant l'ID suivant : 98327490725

TINA :

• Home Page
• Readme
• FAQ

Executer la commande source ~vernadat/.bashrc pour positionner les variables d'environnement TINA.

LTL :

• Rappels
• Manuel SELT

2 Prise en main de Tina

• Recopiez l'exemple du bit alterné abp.ndr vu en cours slides
• 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
• En utilisant SELT, vérifiez les propriétés décrites dans le fichier abp.ltl

3 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 réseau de Petri pour chacun. Vous travaillerz au choix en textuel (.net) ou en graphique (.ndr). Vous les simulerez 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 ( all.tpn ) et simulez l'ensemble. Trouvez un scenario permettant à John et à Fred de se rendre à leur travail en respectant les contraintes temporelles du jour. Vous sauvegarderez le scenario et obteiendrez un échéancier en utilisant l' outil plan (voir Manuel Plan)
• Ajoutez les contraintes temporelles du jour spécifique directement sur la composition : vous procèderez contrainte par contrainte et vous vous assurrerez par simulation que le résultat obtenu correspond bien à ce que vous attendiez ! Une fois que chaque contrainte est validée vous la définirez dans un nouveau réseau (contraintes.ndr) qui contiendra toutes les contraintes temporelles du jour. Votre modélisation vous semble-t-elle correcte ? En utilisant le simulateur, trouvez une scenario où John et Fred arrivent à l'heure au travail.
• Si ce n'a pas déjà été fait, 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 ! et on ne peut le verifier par simulation !!! :
  Pour pouvoir le verifier, vous pouvez utiliser la techniques des observateurs vue en 4E année :
  • Vous ajouterez une nouvelle transition (tobs1) qui est tirable si et seulement si : 1) John et Fred sont effectivement arrives à l'heure 2) John a pris le bus et Fred le covoiturage.
  • Vous reconstruirez l'espace d'etats par la commande : tina compo.tpn compo.ktz
  • Pour s'assurer que la transition tobs1 est morte vous executerez la commande suivante :
    selt "compo".ktz -f '[] - tobs'
  
  On peut aussi utiliser cette technique pour obtenir un scenario et un echeancier decrivant une situatiopn d'accesibilite specifique : par exemple un scenario ou John et Fred ont pris leur voiture et sont arrive à l'heure :
  • a) vous ajouterez une nouvelle transition (tobs2) qui est tirable si et seulement si : 1) John et Fred sont effectivement arrives à l'heure 2) John et Fred ont pris leur voiture
  • Vous reconstruirez l'espace d'etats par la commande : tina compo.tpn compo.ktz
  • Pour obtenir un scenario incluant la transition (tobs2), vous executerez la commande suivante
    selt "compo".ktz -f '[] - tobs2' -S scenobs2.scn
  • Pour obtenir l'echeancier associe, vous executerez la commande suivante :
    plan scenobs2.scn compo.tpn -S Echscen2
  
  
  Pour les étudiants IDM, une approche plus directe/moderne consiste à utiliser la logique temporelle et SELT.

4 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.

5 Exemple de réseau temporel chronométré (Stopwatch TPN)

Recopiez le modèle suivant correspondant à une abstraction très simple d'un système de tâches ordonnancé par un round-robin. Simulez le système, observez les différences par rapport à la simulation d'un réseau de Petri temporel simple.

6 Modélisation d'une machine à café

On se propose de modéliser le fonctionnement d'une machine à café, garantie conforme à la norme AFNOR MC007, qui indique la nécessité pour les machines à café à usage privé de se mettre en veille en cas de réservoir vide. La machine peut délivrer du café ou du thé suivant le type de capsule et de tasse insérées dans les logements prévus à cet effet. Un bouton poussoir permet de sélectionner thé ou café et déclenche le fonctionnement approprié de la machine en même temps. La délivrance d'un café prend 20 secondes et réclame 10cl d'eau, et celle d'un thé prend 40 secondes et réclame 20cl d'eau, quantités qui prennent en compte l'évaporation causée par le chaufage. Un réservoir de 2 litres permet d'alimenter manuellement la machine en eau. La machine ne peut être utilisée par 2 personnes en même temps, le bouton poussoir étant inhibé pendant tout le temps de service d'un utilisateur. La machine se met d'elle même en veille si elle reste inutilisée plus de 5 minutes, auquel cas elle a besoin d'un temps de chauffe de 90s avant de pouvoir fonctionner à nouveau. Ce préchauffage est déclenché lorsque le nouvel utilisateur presse le bouton poussoir, et occasionne une perte d'eau par évaporation de 5 cl. Le fonctionnement de la machine est matérialisé par un voyant lumineux qui change de couleur suivant qu'elle est : en veille, en manque d'eau, prète à fonctionner, ou en service.

1. Modéliser cette machine sous forme d'automates communiquants
2. Vérifier la conformité de la machine à la norme AFNOR MC007