Outil B - RODIN

L'interface de l'Atelier B et/ou de B4free permet de saisir des modèles dans un éditeur de texte. Avec Rodin, la saisie est spécialisée: on ne saisit plus le modèle complet, mais des variables, des invariants, des événements, des assertions, .).

Les conseils qui suivent devraient vous permettre de faciliter vos premiers pas au sein de cette interface de modélisation.

Dans le reste du document, il est supposé que la perspective utilisée est la perspective Event-B de la plateforme Rodin.

• Pour créer un projet, localiser la vue Project Explorer et cliquer sur le bouton Create new project. Une fenêtre apparaît : elle permet de saisir le nom du projet. Cliquer sur Finish pour créer effectivement le projet.

• Avec Rodin, les constantes, les ensembles abstraits et les ensembles énumérés, ainsi que leurs propriétés, sont regroupés dans des composants appelés contextes. Les variables et événements sont regroupés dans des composants appelés modèles.

• Pour créer un contexte, sélectionner dans la vue Project Explorer le projet précédemment créé, puis cliquer sur le bouton Create new component. Une fenêtre apparaît : elle permet de saisir le nom du composant ainsi que son type : Machine (modèle) ou Context. Machine est la valeur sélectionnée par défaut. Sélectionner Context puis cliquer sur Finish pour créer effectivement le contexte. Un éditeur de contexte apparaît alors.

• Pour créer le premier modèle d'une chaîne de raffinement, sélectionner dans la vue Project Explorer le projet précédemment créé, puis cliquer sur le bouton Create new component. Une fenêtre apparaît : elle permet de saisir le nom du composant ainsi que son type : Machine (modèle) ou Context. Cliquer sur Finish pour créer effectivement le contexte. Un éditeur de modèle apparaît alors. Pour utiliser (avoir accès aux constantes et ensembles) d'un ou plusieurs contextes, cliquer le bouton, en bas à droite de la fenêtre de l'éditeur de modèle,  représentant une flèche vers le bas et situé juste à gauche du bouton Add. Une liste déroulante apparaît, contenant les contextes définis dans le projet. Choisissez le contexte à utiliser puis cliquer sur Add pour ajouter ce contexte dans la liste de visibilité.

• Pour créer un raffinement d'un modèle existant, sélectionner ce modèle dans la vue Project Explorer puis faites clic-droit pour voir apparaître un menu contextuel : sélectionner alors Refine. Une fenêtre apparaît, vous invitant à saisir le nom du composant à créer. Cliquer sur OK pour créer effectivement le modèle raffiné, contenant toutes les variables et événements définis dans le modèle abstrait.

Pour créer un ensemble abstrait, dans un contexte donc, sélectionner l'éditeur du contexte. Localiser le bouton New Carrier Set Wizard situé au dessus de l'éditeur de contexte (il a la forme d'un S majuscule jaune). Cliquer dessus. Une fenêtre apparaît alors, vous permettant de saisir un ou plusieurs noms. Cliquer sur OK pour créer tous les ensembles abstraits déclarés.

• Pour créer un ensemble énuméré, sélectionner l'éditeur du contexte. Localiser le bouton New Enumerated Set Wizard situé au dessus de l'éditeur de contexte (il a la forme d'un S majuscule rouge). Cliquer dessus. Une fenêtre apparaît alors, vous permettant de saisir le nom de l'ensemble ainsi les différentes valeurs. Cliquer sur OK pour créer l'ensemble énuméré ainsi défini. Attention ! L'ensemble énuméré n'est pas un des types de base de Rodin : il est défini en terme de constantes dont les éléments constituants sont distincts deux à deux. Ces axiomes sont générés par le wizard. Pour modifier la définition d'un ensemble énuméré, il est alors nécessaire de modifier manuellement les constantes créées par le wizard ainsi que les axiomes associés.

• Pour créer une variable, dans un modèle donc, sélectionner l'éditeur du modèle. Localiser le bouton New Variable Wizard situé au dessus de l'éditeur de modèle (il a la forme d'un v minuscule jaune).

Une fenêtre apparaît alors, vous permettant de saisir le nom de la variable, son initialisation et son invariant. Toute modification du nom de la variable est répercutée dans l'initialisation et l'invariant.

• Pour créer un événement,  sélectionner l'éditeur du modèle. Localiser le bouton New Event Wizard situé au dessus de l'éditeur de modèle (il a la forme d'un e minuscule noir).

Une fenêtre apparaît alors, vous permettant de saisir le nom de l'événement, la liste des variables locales (3 champs intitulés variable name(s)), des gardes et des actions (substitutions).

• Le langage mathématique a été simplifié et clarifié :
• Les opérateurs + et - sont uniquement des opérateurs arithmétiques. La différence ensembliste se note \ et le produit cartésien s'obtient en tapant **.
• Il n'y a plus de séquences dans Rodin.
• L'ensemble des parties finies d'un ensemble ne fait plus partie du langage. Pour indiquer qu'un ensemble S est fini, écrire finite(S).
• Dans un prédicat quantifié, la liste des variables ne doit plus être parenthésée. Avec l'Atelier B, on écrit !(x1,x2).(P(x1, x2)). Avec Rodin, on écrit !x1,x2.P(x1,x2).