Responsable : Aymeric Vincent
Téléphone : 05 4000 35 09
E-mail : vincent@labri.fr
Contexte et objectifs du projet :
La vérification de modèles utilise le calcul de points fixes pour calculer des propriétés de graphes, par exemple l'ensemble des états accessibles d'un système. Lorsqu'on imbrique des calculs de points fixes, on peut exprimer par exemple des propriétés d'équité. L'imbrication de plusieurs points fixes rend la compréhension du résultat du calcul très difficile et fait appel à des algorithmes exponentiels dans le nombre d'alternances. Il est donc utile d'étudier ces algorithmes, et le but de ce projet est de permettre de visualiser ces calculs de manière graphique.
Vous aurez à programmer dans le langage de votre choix (vraisemblablement Java ou C++) une interface graphique permettant de visualiser plusieurs treillis côte-à-côte. Vous pourrez ou non proposer l'édition graphique de ces treillis, le chargement de descriptions textuelles de treillis, ou la génération automatique de treillis classiques.
Vous devrez fournir un moyen de spécifier un algorithme de calcul de points fixes et des équations à résoudre. Cela pourra être codé en dur dans le programme Java, mais devra être très aisément changeable par l'utilisateur.
Enfin, et c'est là le but de votre programme, vous devrez animer les couleurs des sommets des treillis de manière judicieuse pour permettre de visualiser la façon dont l'algorithme procède pour effectuer ses calculs successifs.
Ce projet doit comporter une part importante de réflexion sur le papier pour concevoir une interface graphique simple mais très fonctionnelle. Vous serez sans doute amenés à utiliser des bibliothèques de manipulation de graphes (pour représenter graphiquement les treillis) déjà existantes, et disponibles sur l'Internet.
Mots-clés : Treillis, points fixes, mu-calcul