MSC II : Automates communicants -- UPPAAL
Support de cours
Zoom :
Pensez svp à ouvrir au début de chaque TP une session Zoom
via votre navigateur
(Pas besoin d'installation de client ni de compte -- accès anonyme via "Join from Your Browser")
Zoom : 98327490725
Uppaal
Les Tps utilisent le logiciel UPPAAL
développé conjointement par le Department of Information Technology de l'université
d'Uppsala et le Department of Computer Science de l'université d´Aalborg.
Uppaal est librement téléchargeable ici
Fichiers Uppaal
Les systèmes Uppaal sont décrits par :
- un fichier fic.xta (xta : extended time automata)
décrivant l'ensemble du système,
accompagné par un fichier (optionnel)
fic.ugi décrivant uniquement la partie graphique (celui-ci est généré après édition).
- (optionnel mais conseillé) un fichier fic.q (query) décrivant les propriétés
A savoir
- L'édition des modèles ou des propriétés peut se faire via l'interface graphique
ou en textuel en utilisant son éditeur favori.
Une aide en ligne est disponible (onglet help)
- Les fichiers xta et ugi doivent être cohérents. Dans le doute, effacez le fichier .ugi.
- Les messages du "compilateur" sont parfois rudimentaires.
Quelques erreurs pas toujours bien diagnostiquées :
- Les identificateurs sont de la forme [a-zA-Z_]([a-zA-Z0-9_])*.
Bannir les accents et les espaces dans les noms.
- Ne pas oublier de déclarer tous les états.
- Ne pas hésiter à verifier fréquemment son code via la touche F7
(onglet Tools / Check syntax).
- Etats urgents La notion d'urgence intervient dans la partie temporisée
(non abordée en 4IR).
Par défaut, déclarez tous les états comme urgent.
Invocation d'Uppaal :
Idéalement dans le directory contenant le fichier xta.
Appel via "uppaal nom_du_systeme"
Accès alternatif au model-checker
Il est possible de vérifier un ensemble de queries Uppaal en ligne de commande
via l'appel suivant : "verifyta fic.xta spec.q"
Il faut préalablement ajouter le chemin d'accès à verifyta
export PATH="/usr/local/insa/uppaal/bin-Linux:$PATH"
dans son fichier ~/.bashrc
et mettre à jour son environnement
dans un terminal via la commande source ~/.bashrc
Ressources
- L'ensemble des sources pour les les 3 séances est disponible via :
- En local, en exécutant la commande suivante "cp -r ~vernadat/TpUppaalIR24 ."
- A distance, en sauvant l'archive suivante TpUppaalIR24.zip
Le répertoire est constitué par 3 répertoires (un par TP), chacun de ceux-ci étant subdivisés
en autant de sous-répertoires que de questions.
- Support de cours
- Annales : 2022 / 2023
Lien video correction Mot de passe Kpk?yx3J
nb: Le résultat n'est pas idéal. Augmentez la vitesse de défilement