Developed by ClearSy in the context of the European MATISSE project, this tool lets you convert Event B models into B models that can be used with Atelier B. EVT2B is in Beta version and is used in the context of a number of industrial projects.
- Operating system: Windows, Linux
- Atelier B 3.7
- krt : logic solver (already included in Atelier B)Windows – Linux
- evt2b.kin : compiled theory language file
EVT2B execution requires the use of the “logic solver” krt (integrated into Atelier B), the evt2b.kin file (compiled file of the theory language) and a B event model (.sys files).
Make sure you rename the evt2b.kin.<plateforme>.<version_de_l’AtelierB> file with evt2b.kin.
Go to the directory that has your B event model (.sys files).
For each refinement column, you need to create a configuration file that includes the following text:
- LoadComponent(<Machine>) & Analysis & WriteComponents where <Machine> is the name of the machine in the column that has the most details.
Now, simply execute the following command for each configuration file:
- With Linux: krt -p rmcomm -b evt2b.kin <fichier_de_configuration>
- With Windows: krt.exe -p rmcomm -b evt2b.kin <fichier_de_configuration>
where <fichier_de_configuration> is the name of the configuration file to be processed.
EVT2B will generate the equivalent B model: a .mch file and a number of .ref files per refinement column.