Dans cette dernière partie, nous allons voire comment utiliser l’API Rodin.

Maintenant que nous savons comment lancer un plug-in dans Rodin il est intéressant de pouvoir manipuler les différentes API mises à notre disposition. Pour commencer, nous allons voir à travers un petit exemple comment, lire une machine, afficher la liste de ses invariants, la liste de ses théorèmes ainsi que la liste des événements et de leurs gardes respectifs.

Pour commencer, nous allons devoir récupérer l’API sous forme d’un ensemble des .jar. Rendez-vous sur wiki.event-b.org cliquez sur Download now puis sélectionnez la version contenant la chaine -dev.

Pour ma part j’ai téléchargé la version portant l’intitulé rodin-2.4-dev.zip. Revenez dans votre projet Eclipse, faites un clic droit sur votre projet Build Path -> Configure Build Path -> Add Externals JARs… et sélectionnez le répertoire contenant les .jar que l’on vient de récupérer.

Il faut maintenant définir dans le fichier MANIFEST.MF les dépendances qui sont nécessaires. Dans notre exemple nous aurons uniquement besoin du package org.eventb.core. Dans l’onglet Dependencies, dans la liste Required Plug-ins, cliquez sur Add. Saisissez eventb puis sélectionnez le package org.eventb.core.

Une fois toutes les dépendances ajoutées pensez à sauvegarder le manifest.

Il est désormais possible de faire appel aux différentes parties de l’API que nous venons d’ajouter. Retournons maintenant dans notre classe SampleAction et ajoutons un peu de code à notre méthode run.

import org.eventb.core.IEvent;
import org.eventb.core.IGuard;
import org.eventb.core.IInvariant;
import org.eventb.core.IMachineRoot;
import org.rodinp.core.IInternalElement;
import org.rodinp.core.IRodinElement;
import org.rodinp.core.IRodinFile;
import org.rodinp.core.IRodinProject;
import org.rodinp.core.RodinCore;
import org.rodinp.core.RodinDBException;
...
public void run(IAction action) {
  IRodinProject project = RodinCore.getRodinDB().getRodinProject("PTest");
  try {
    for (IRodinElement element : project.getChildren()) {
      if (element instanceof IRodinFile) {
        IInternalElement root = ((IRodinFile) element).getRoot();
        if (root instanceof IMachineRoot) {
          for (IInvariant invariant : ((IMachineRoot) root).getInvariants()) {
            if (invariant.isTheorem()) {
              System.out.println("Théoréme : " + invariant.getLabel() + " : " + invariant.getPredicateString());
            } else {
              System.out.println("Invariant : " + invariant.getLabel() + " : " + invariant.getPredicateString());
            }
          }
          for (IEvent event : ((IMachineRoot) root).getEvents()) {
            System.out.println("Événement : "+ event.getLabel());
            for (IGuard garde : event.getGuards()) {
              System.out.println("  Garde : " + garde.getLabel() + " : " + garde.getPredicateString());
            }
          }
        }
      }
    }
  } catch (RodinDBException e) {
    e.printStackTrace();
  }
}

Dans cet exemple le nom du projet et le nom du modèle sont codés en dure. Pour le tester vous allez donc devoir lancer le plug-in. Une fois dans Rodin, Créez un nouveau projet nommé PTest puis créez une nouvelle machine nommée MTest. J’ai ensuite déclarer la machine suivante : MTest.pdf ou PTest.zip. Une fois le projet et la machine mise en place, il ne reste plus qu’à tester le bon fonctionnement du plug-in. Cliquez sur Sample Menu -> Sample Action puis retournez dans la console de Eclipse. Chez moi il affiche cela :

Invariant : inv1 : a ? ?
Théorème : inv2 : a ≥ 0
Événement : INITIALISATION
Événement : int
Garde : grd1 : a < 5

On peut constater un léger problème mais rien de grave. En effet les symboles b, appartient «:» et entier naturel «NAT» apparaissent avec des points d’interrogation. Cela vient en faite de la configuration de Eclipse qui est configurèe par défaut pour tout afficher en ASCII. Pour modifier cela, faites un clique droit sur le projet puis Run As -> Run Configurations… Dans votre configuration sélectionnez l’onglet common puis dans encoding choisissez other : UTF-8. Stoppez l’exécution de Rodin puis relancer le. Cliquez sur Sample Menu -> Sample Action puis retournez dans la console de Eclipse. Chez moi il affiche maintenant cela :

Invariant : inv1 : a ∈ ℕ
Théorème : inv2 : a ≥ 0
Événement : INITIALISATION
Événement : int
Garde : grd1 : a < 5

Si on analyse maintenant se résultat, nous voyons que nous obtenons bien la liste des invariants\ théorèmes avec la différentiation des deux. Puis nous avons la liste des événements avec leurs gardes respectives.