Présentation de B2RODIN
B2RODIN permet d'importer dans la plateforme Rodin des
modèles B textuels, développés avec l'Atelier B ou B4Free. Une colonne compète
de raffinement peut être importée en une seule étape. B2RODIN se charge de
générer les modèles et les contextes associés.
Comment installer B2RODIN ?
L'installation de B2RODIN utilise
la fonctionnalité « UpdateSite » d'Eclipse. Pour ce faire, il
faut :
-
Activer, dans le menuHelp / Software Updates, la fonctionnalité « Find and Install » ;
-
Sélectionner « Search for a new feature to install »;
-
Cliquer sur le bouton"New Remote Site .";
-
Dans la fenêtre dedialogue qui est apparue, saisir :
-
Cliquer sur le bouton« Finish » pour installer le plugin b2rodin.
L'aide en ligne permet de
comprendre comment mettre en ouvre cet outil.
Comment utiliser B2RODIN ?
Les modèles B à importer doivent être compatibles avec le B
événementiel, c'est-à-dire que les opérations doivent être de la forme :
Il faut par ailleurs ajouter aux modèles B textuels des
informations relatives à la sémantique du B événementiel (voir l'aide en ligne
de l'outil à ce propos pour plus de détails), en indiquant notamment comment
les événements sont raffinés : introduction de nouveaux événements,
combinaison d'événements, éclatement d'événement.
Il est possible enfin de valuer les constantes du modèle
textuel, afin de l'animer avec Brama.
Pour importer une colonne de raffinement en une seule fois,
il faut indiquer le dernier raffinement de la colonne que l'on veut importer/
B2RODIN se charge alors d'importer de manière itérative les abstractions de ce
raffinement.
Historique des Versions de Brama
-
Ajout
d'un mode permettant de ne pas sur-parentheser les composants générés.
Ce mode n'est pas activé par défaut, car il n'a pas été beaucoup testé.
-
Dans le cas ou aucun pragma include n'est donné dans la machine B, B2rodin traduit dorénavant tous les
événements. Le comportement précédent était de ne rien traduire.
-
Correction d'un bug lorsque de la traduction d'expressions parenthesées.
-
Correction d'un problème d'installation sous macos X: le fichier b2rodin n'était pas rendu
exécutable lors de l'installation.
