Warning: include(../../include/menu-fr.php) [function.include]: failed to open stream: No such file or directory in /homepages/5/d101319127/htdocs/atelierb.eu/ressources/evt2b/evt2b-fr.php on line 34
Warning: include() [function.include]: Failed opening '../../include/menu-fr.php' for inclusion (include_path='.:/usr/lib/php5') in /homepages/5/d101319127/htdocs/atelierb.eu/ressources/evt2b/evt2b-fr.php on line 34
EVT2B - Traducteur B Evénementiel vers B
Développé par ClearSy dans le cadre du projet Européen MATISSE, cet outil permet de convertir des modèles B évènementiels vers des modèles B utilisables par l'Atelier B. EVT2B est en version beta, il est utilisé dans le cadre d'un certain nombre de projets industriels.
Pré-Requis
- Système d'exploitation : Windows, Linux
- Atelier B 3.7
Téléchargement
- krt : logic solver (déjà inclu dans l'Atelier B)
Windows - Linux
- evt2b.kin : fichier compilé du langage de théorie
Télécharger evt2b.kin
Archives
Documents
- Manuel de référence du langage (pdf)
- Manuel utilisateur (non maintenu depuis la version 3.6 de l'Atelier B) (pdf)
Utilisation
L'exécution d'EVT2B nécessite l'utilisation du "logic solver" krt (intégré à l'AtelierB), du fichier evt2b.kin (fichier compilé du langage de théorie) et d'un modèle B événementiel (fichiers .sys).
Assurez vous de renommer le fichier evt2b.kin.<plateforme>.<version_de_l'AtelierB> en evt2b.kin.
Placez-vous dans le répertoire contenant votre modèle B événementiel (fichiers .sys).
Pour chaque colonne de raffinement, vous devez créer un fichier de configuration contenant le texte suivant :
-
LoadComponent(<Machine>) & Analysis & WriteComponents où <Machine> est le nom de la machine la plus détaillée de la colonne.
Il vous reste à exécuter pour chaque fichier de configuration la commande suivante :
- Sous Linux : krt -p rmcomm -b evt2b.kin <fichier_de_configuration>
- Sous Windows : krt.exe -p rmcomm -b evt2b.kin <fichier_de_configuration>
où <fichier_de_configuration> est le nom du fichier de configuration à traiter.
EVT2B va générer le modèle B équivalent : un fichier .mch et
plusieurs fichiers .ref par colonne de raffinement.