Getting Started
- State Machines -
1. Creating an Event-B Project
Create an Event-B project using the ‘folder’ button at the top of the Event-B Explorer view.
2. Creating an Event-B Machine
Create a machine inside the project using the file button at the top of the Event-B Explorer view.
4. Adding a UML-B State-machine
Right click on the UML-B container and use the Add Statemachine context menu item to add a state-machine. Give the state-machine a name in the pop up dialog.
5. Opening the diagram editor
A state-machine will appear in the contents of the UML-B in the Event-B Explorer view. Double click on it to open the diagram.
6. Drawing states
To draw a state click on the tool in the palette, (let go,) and then click on the canvas where you want to place the item. First draw an initial and then draw a state. States are given default names. Change the name of the state by selecting it and typing in the properties fields below the diagram.
7. Drawing transitions
To draw a transition, select the transition tool in the palette, click on the starting node (do not let go) and then drag to the target node and let go. (When drawing transitions, it is sufficient to click the mouse anywhere in the start/end node. It is not necessary to click on the boundaries). You can not name transitions. They have a label that is automatically constructed from the name of the event(s) that they ‘elaborate’ (as described in the next step).
8.Linking to an existing event
To link a transition to an existing event, select the transition, and then click on the ‘Link Event’ button in the properties view. Select an event from the list in the pop-up dialog and click OK. In our example, the only event in the machine is the INITIALISATION event. (We refer to this linking as ‘elaborates’).
The transition is automatically labelled with the elaborated event INITIALISATION.
9. Linking to a new event
Add another state and a transition starting from the previous state. Select the transition but this time use the Create & Link button. Give a name for the event and click ok.
Note that this is a convenience to save you having to edit the machine to add an event. As soon as the diagram is saved, the event will appear in the machine even though the diagram has not been translated into Event-B.
10. Translating to Event-B
With the diagram selected (as focus), click the UML-B translate toolbar button (orange gears) to generate the Event-B for the diagram into the machine. The corresponding Event-B should appear in the machine.
11. Changing the translation
An alternative translation is available which is sometimes more elegant. To change the translation, select the diagram canvas and then change the Translation property from ‘Variables’ to ‘Enumeration’. Save the diagram and then re-generate the Event-B. A context is automatically generated to define the Statemachine states as an enumeration and the generated Event-B in the machine changes accordingly.