B Tools - RODIN
 User Manual – First Steps with the RODIN
Platform
The Atelier B and/or B4free interface lets you
enter models in a text editor. With Rodin, entries are specialized: the full
model is no longer entered, just the variables, invariants, events and
assertions.
The following
recommendations should ease your first steps within this modelling interface.
It is assumed in the rest
of the document that the perspective used is the Rodin platform Event-B
perspective.
- To create a project, locate the Project
Explorer screen and click on Create new project. A window will appear:
enter the name of the project. Click on Finish to complete the
creation of the project.
- With Rodin, the constants, abstract sets
and enumerated sets, as well as their properties, are grouped within
components called contexts. The variables and events are grouped in
components called models.
- To create a context, select the project
you just created in Project Explorer, then click on Create new
component. A window will appear: this will allow you to enter the name
and type of the component: Machine (model) or Context. Machine
is the default value. Select Context, then click on Finish
to effectively create the context. A context editor will then appear.
- To create the first model in a refinement
chain, in Project Explorer, select the project you just created,
then click on Create new component. A window appears: this will
allow you to enter the name and type of the component: Machine
(model) or Context. Click on Finish to complete the creation
of the context. A model editor will then appear. To use (have access to
the constants and sets) one or more contexts, click on the button at the
bottom right of the model editor window in the form of an arrow facing
downwards that is located just left of the Add button. A dropdown
list will appear that sets out the contexts defined in the project. Select
the context you want to use, then click on Add to add this context to
the view list.
- To create the refinement of an existing
model, select this model in the Project Explorer window, then
right-click to open a pop-up menu: then select Refine. A window
will appear inviting you to enter the name of the component you want to
create. Click on OK to create the refined model that contains all
the variables and events defined in the abstract model.
To create an abstract set in a context, select
the context editor. Locate the New Carrier Set Wizard button located
above the context editor (in the form of a yellow capital "S"). Click
on it. A window will appear that allows you to enter one or more names. Click
on OK to create all the declared abstract sets.
- To create an enumerated set, select the
context editor. Locate the New Enumerated Set Wizard button located
above the context editor (in the form of a red capital "S").
Click on it. A window will then appear that allows you to enter the name
of the set and the various values. Click on OK to create the
enumerated set you have defined. Note! The enumerated set is not one of
the Rodin base types: it is defined in terms of constants, the
constituting elements of which are distinguished two by two. These axioms
are generated by the wizard. To change the definition of an enumerated
set, you must manually change the constants the wizard has created, as
well as the related axioms.
- To create a variable in a model, select
the model editor. Locate the New Variable Wizard button located
above the model editor (in the form of a yellow small "v").
A window
will then appear allowing you to enter the name of the variable, its
initialization and its invariant. Any change of the name of the variable is
repeated in the initialization and invariant.
- To create an event, select the model
editor. Locate the New Event Wizard button located above the model
editor (in the form of a black small "e").
A
window will then appear allowing you to enter the name of the event, the list
of local variables (three fields entitled variable name(s)), guards and
actions (substitutions).
|
