title: "Atelier B" subtitle: "Installation Guide" date: "Atelier B 4.7.1 Community Edition" version: "Atelier B 4.7.1 Community Edition" copyright: "© 2023 by CLEARSY" licence: | Licensed under Attribution-NonCommercial-ShareAlike 4.0 International. To view a copy of this license, visit \url{http://creativecommons.org/licenses/by-nc-sa/4.0/}. licence-logo: "images/by-nc-sa.png" doccode: "ATB-IG-CE-4.7.1" colorlinks: true header-includes:
- |
\usepackage{awesomebox} \usepackage[utf8]{inputenc} \usepackage[french]{babel}
pandoc-latex-environment: importantblock: [requirement] noteblock: [note]
...
This guide provides installation instructions for Atelier B 4.7.1 Community Edition, available from www.atelierb.eu.
Atelier B and bbatch are integrated development environements (IDE) for the B method and Event-B. Atelier B provides a graphical user interface (GUI) and bbatch is a command-line interface (CLI).
This guide provides installation guidelines for Atelier B and bbatch.
There is one chapter for each supported platform: Linux, macOS and Windows. Projects and workspaces are a source of confusion for new users, a chapter is dedicated to them. Finally a lexicon is provided to help the reader to understand the terminology used in this guide.
These instructions correspond to a successful install in a Linux Mint 21 Vanessa environment (base Ubuntu 22.04) and assume that the package "atelierb-free-4.7.1p1-linux_x64.deb" has been downloaded.
Open a terminal and issue the following command:
sudo dpkg -i atelierb-free-4.7.1p1-linux_x64.debEnter the password to gain root access. The software is installed in the following directory:
/opt/atelierb-free-4.7.1p1To open Atelier B GUI, issue the following command:
/opt/atelierb-free-4.7.1p1/startABAtelier B is now open
To open bbatch CLI, issue the following command:
/opt/atelierb-free-4.7.1p1/startBBThese instructions correspond to a successful install in a Linux Mint 21 Vanessa environment (base Ubuntu 22.04) and assume that the package "atelierb-free-4.7.1p1-linux_x64.tar.gz" has been downloaded.
Issue the following command to unpack the archive:
tar xf atelierb-free-4.7.1p1-linux_x64.tar.gzThis creates a directory named "atelierb-free-4.7.1p1-linux_x64opt/atelierb-free-4.7.1p1" in the current directory.
You may move this directory to a location of your choice, say "$HOME/local/AB-4.7.1".
To open Atelier B GUI, issue the following command:
$HOME/local/AB-4.7.1/startABAtelier B is now open
To open bbatch CLI, issue the following command:
$HOME/local/AB-4.7.1/startBB:::note The bbatch CLI is not available on macOS for this version of the software. :::
These instructions correspond to a successful install in a macOS 14.0 (Sonoma) environment. They should be applicable to other versions of macOS.
Control-click on the installer file to start the installation process (double-clicking will not work as the publisher is not white-listed in this environment).
This displays the license agreement dialog.
Read carefully and click on "Agree" to proceed.
A finder window is opened, it contains a shortcut to the application folder and the Atelier B icon.
Drag the Atelier B icon to drop it into the "Applications" folder.
Et voilà! Atelier B is now installed in the "Applications" folder.
The first time Atelier B is opened, use the control click combo, as otherwise macOS will deny the execution right to the application. macOS warns you that it does not know the software developer. Click on "Open" to proceed.
Atelier B is now open.
These instructions correspond to a successful install in a Windows 10 environment. They should be applicable to other versions of Windows.
Double-click on the installer file to start the installation process.
Windows warns you that it does not know the software publisher. Click on "Yes" to proceed.
This opens the installer setup dialog.
Click on "Next" to proceed. The license agreement dialog is displayed.
Click on "I Agree" to proceed (otherwise do not use the software). The installation folder dialog is displayed.
Choose a directory with full access rights (in this setup, we stick with the default location). Click on "Next" to proceed. The startup menu folder dialog is displayed.
You may safely leave the default value. Click on "Install" to proceed. A progress dialog appears. When the installation is finished, the following dialog is displayed.
Click on "Finish": installation is complete and the software is ready to use. The startup menu folder now contains two entries for Atelier B: one for the GUI and one for the CLI.
If you double-click on the "Atelier B 4.7.1" entry, the GUI is started.
If you double-click on the "Atelier B Batch interface (4.7.1)" entry, the CLI is started.
You may encounter errors due to access controls on the directories that the tools need to access. If this is the case, read through carefully the chapter on projects and workspaces.
::: note When you install and use Atelier B and bbatch, you must be make sure to have read/write access to worskpace(s) and project(s) directories. :::
In both Atelier B and bbatch, developments are organized in so-called B projects. Each B project has a data base directory (bdp) and a language directory (lang).
-
The data base directory (bdp) contains all the internal artifacts necessary for Atelier B and bbatch to work.
-
The language directory (lang) contains the files in a programming language, such as C, that are produced from the B components of the project.
The B project is made up of a number of source files.
Source files are either B / Event-B components.
The list of the source files of a B project is stored in the bdp in an XML file with the extension db.
For each B component, there is a corresponding PMM file with the same name and the extension pmm,
containing proof rules and proof tactics for this component. The PMM file shall be stored in the same directory
as the corresponding source file.
::: note It is good practice to store the source files of a B project in a single directory. :::
Atelier B lets the user have several workspaces, each workspace being a collection of projects.
In practice, a workspace is associated to a project data base directory (bdb), where each file ending with the
desc extension corresponds to a project. Actually, the contents of the desc file is only the
path to the bdp and lang directories of the project.
bbatch does not have the concept of workspace. It is the user's responsibility to provide the path to the bdb of some workspace.
A fresh install creates an empty workspace named "local" and associates it with a directory (bdb) located in the user's home directory.
To know what is the bdb of a workspace, right-click on the workspace in Atelier B and select "Properties". This opens the workspace properties dialog.
The dialog has four tabs, and initially presented with the "bbatch" tab. There, the following information is displayed:
- the name of the workspace (in this case, "local"),
- the path of the installation of Atelier B,
- the path to the bdb of the workspace (namely, the workspace database directory),
- a checkbox to indicate whether the workspace is the default workspace.
It is currently not possible to change the path to the bdb of a workspace from the GUI. You may change the path to the bdb of a workspace by editing directly the settings of the tool.
-
On Linux: The settings are stored in the .config directory as plain text files and may be edited with any text editor.
-
On macOS: The settings are stored in file "~/Library/Preferences/com.clearsy.AtelierB free 4.7.1.plist" and may be edited with the Xcode application.
-
On Windows: the settings are stored in the registry and may be viewed and edited with RegEdit. If you cannot change the path to the bdb of a workspace, you may create a new workspace (menu "Atelier B | New | Workspace").
See Workspace.
The bdp of a project is a directory that stores all the internal files necessary for the management of the project.
The bdp of a project is a directory that stores all the files resulting from the translation to a programming language of B components.
A file containing proof rules and proof tactics for a B component.
A project is a collection of B components and PMM files. It is referenced from a workspace thanks to a desc file.
It contains a data base directory (bdp) and a language directory (lang).
A workspace is a collection of projects. It is a directory containing a collection of desc files. Atelier B stores
the workspaces in its settings (in registry on Windows, under the $HOME/.config directory on Linux and macOS).