Résumé
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.
Travail demandé
Vous aurez à programmer dans le langage de votre choix (avec une préférence
pour le Common Lisp) 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, et la génération automatique de treillis classiques.
Le programme devra offrir plusieurs façons d'afficher un treillis,
y compris des affichages avec perte d'informations (par exemple n'afficher
que la hauteur du treillis et son nombre de sommets, ou bien sa projection
sur un plan ou une droite) car certains treillis manipulés seront très
volumineux.
Vous devrez fournir un moyen de spécifier un algorithme de calcul de
points fixes et les équations à résoudre. Cela pourra être codé en dur
dans le programme, mais devra être très aisément modifiable par
l'utilisateur.
Enfin, et c'est là le but de votre programme, vous devrez animer par exemple
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.
Matériels et logiciels nécessaires
Une bibliothèque d'affichage graphique et un interprète/compilateur pour le
langage choisi. Exemples de tandems : Qt/C++, Swing/Java, CLX/SBCL.