Plateforme TouIST

Responsables :  Dominique LONGIN et   Frédéric MARIS

La plateforme TouIST propose un langage de haut niveau pour modéliser en logique divers problèmes de manière très compacte en faisant appel à des solveurs. Elle se compose : d’une interface graphique permettant la saisie interactive du modèle visé ; d’un module de traduction (compilateur) du langage d’entrée de TouIST vers un langage directement compréhensible par différents solveurs ; d’un module de visualisation des modèles calculés par les solveurs. Actuellement, TouIST peut faire appel à trois types de solveurs différents : solveurs SAT (logique propositionnelle ou logique des prédicats sur domaine fini), QBF (autorisant la quantification sur les formules propositionnelles), SMT (pour le traitement de problèmes faisant appel à des calculs numériques sur nombres entiers ou rationnels).

Le but de la plateforme est de permettre à l’usager de se concentrer sur la modélisation d’un problème donné sans se préoccuper des détails techniques liés à l’utilisation de solveurs : traduction des formules en forme normale conjonctive, puis traduction dans le langage DIMACS, QDIMACS ou SMT-LIB (langages utilisés de manière standard en entrée des solveurs mais se prêtant peu à une manipulation directe aisée). TouIST peut aussi être utilisé entièrement en ligne de commande de manière à s’interfacer avec des architectures d’agent intelligent capable de raisonner et de planifier des actions : typiquement par exemple, vérifier la validité d’un argument, déterminer les actions exécutables, vérifier qu’un plan est valide ou même calculer un plan complet d’actions pour satisfaire un but, etc.

TouIST est actuellement utilisé à la fois pour l’enseignement et la recherche. En enseignement, nous l’utilisons à l’Université Toulouse 3 – Paul Sabatier en Licence (pour présenter une utilisation concrète de la logique en vue de modéliser certains problèmes, ce qui concerne environ 450 étudiants par an) et en Master (pour la modélisation de problèmes de satisfaction de contraintes et de planification). En recherche, TouIST est l’occasion de recherches permanentes concernant à la fois :

  • le développement de son langage d’entrée où le but est d’obtenir un langage logique de haut niveau le plus expressif possible tout en permettant une traduction qui reste très compacte vers le langage d’entrée de chacun des types de solveur utilisable, et en faisant en sorte que le problème traduit dans ce langage puisse être traité le plus efficacement possible par le solveur considéré ;
  • l’extension à d’autres fonctionnalités (extension de l’interface graphique d’entrée et de sortie, prise en compte de plug-ins dédiés au traitement de problèmes spécifique comme par exemple, des extensions du langage spécialisées pour les problèmes d’argumentation ou de planification, la prise en compte d’opérateurs modaux et de leur traduction en logique classique, etc.).

De plus, TouIST est également utilisé au sein de projets du département. Par exemple, dans le projet ANR CoPains sur le développement d’un agent persuasif d’aide aux personnes âgées, il est utilisé par l’architecture pour vérifier la validité des plans d’actions conversationnelles de l’agent artificiel. Par ailleurs, le département IA développe depuis plusieurs années le démonstrateur LoTReC pour les logiques modales. Il est basé sur une construction des modèles de Kripke à base de mondes possibles d’une formule modale, et est capable de traiter potentiellement n’importe quelle logique (mono- ou multi-) modale. Une réflexion est actuellement menée afin d’utiliser TouIST pour vérifier la cohérence des mondes possibles des modèles construits, ce qui optimiserait grandement l’exécution de LoTReC et réduirait considérablement certains problèmes mémoire inhérents à la construction de tels modèles, rapidement de très grande taille.

À l’ENS et à l’IRISA de Rennes, Hintikka’s World est un programme permettant de décrire de manière visuelle les mondes possibles associés à des agents artificiels (dans une démarche de logiques épistémiques), et un module d’interfaçage a été développé afin de rendre possible l’utilisation de TouIST par leur programme, grâce auquel sont calculés de manière beaucoup plus efficace les modèles à afficher.

Au niveau international, TouIST est utilisé notamment par l’Université de Séville pour l’enseignement en Licence (selon une approche similaire à celle utilisée à l’Université Toulouse 3).

Positionnement de la plateforme par rapport aux plateformes existantes (locales et nationales)

À notre connaissance, il n’existe aucun équivalent à TouIST en France ou ailleurs dans le monde. Les recherches sont focalisées sur le développement des solveurs eux-mêmes afin de les rendre le plus efficace possible, et non sur leur utilisabilité. D’autres langages, tel Isabel, permettent de réécrire une interface telle que TouIST. L’avantage de ce dernier est d’offrir un produit simple, léger, utilisable directement pour faire de la modélisation logique, libre de droit.

Description technique, organisationnelle, taux d’utilisation

TouIST se présente sous la forme d’un programme exécutable en ligne de commande (développé en OCAML) et d’une interface graphique (développée en JAVA) dont l’utilisation n’est pas obligatoire. Il intègre actuellement 3 solveurs par défaut (SAT, QBF, SMT) mais peut s’interfacer avec n’importe quel solveur prenant en entrée les langages standards DIMACS, QDIMACS ou SMT-LIB, ce qui permet à TouIST de bénéficier automatiquement des performances des solveurs les plus récents.

Le programme peut être téléchargé librement depuis le web (https://www.irit.fr/touist/), et des tutoriels ont été développés afin de faciliter en toute autonomie sa prise en main. Localement, environ 450 étudiants l’utilisent chaque année, en plus des chercheurs et enseignants-chercheurs extérieurs.