Dans la partie précédente, nous avons vue comment utiliser Rodin comme plateforme d’exécution. Dans cette article, nous allons voire un exemple d’utilisation simple de l’API de Rodin. Avec la version 3.0 de Rodin, cette étape as été grandement simplifiée. [toc]

Dépendances

Le fichier MANIFEST.MF permet de configurer différentes informations relatives à notre plug-in. Pour utiliser les API de Rodin, rendez-vous dans l’onglet dependences en bas à gauche puis, dans la section Required plug-ins cliquez sur le bouton Add…. et sélectionnez le package org.eventb.core. De la même manière, ajoutez le package org.rodinp.core.

Capture d’écran 2012-03-30 à 10.27.40

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

Ouvrez maintenant la 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.