Rodin User’s Handbook v.2.8: Wizards

3.1.6 Wizards

In addition to being able to directly enter modelling elements in the editor, it is also possible to add them by using wizards. You can activate the different wizards by using the buttons in the tool bar as shown in Figure 3.19 and in Figure 3.20 or via the Event-B menu (the menu will only provide the wizards that you need for creating your machine components or context components). The next sections explain how to use the wizards.

$\includegraphics{img/reference/ref_01_eventb_editor12.png}$

Figure 3.19: Wizards for context specific elements located in the tool bar

$\includegraphics{img/reference/ref_01_eventb_editor13.png}$

Figure 3.20: Wizards for machine specific elements located in the tool bar

3.1.6.1 New Carrier Sets Wizard

To activate the New Carrier Sets Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newset_edit.png}$ button located in the tool bar. Pressing the button bring up the window shown in Figure 3.21.

$\includegraphics{img/reference/ref_01_eventb_editor4.png}$

Figure 3.21: New Carrier Sets Wizard

You can enter as many carrier sets as you want by pressing the More button. When you are finished, press the OK button.

3.1.6.2 New Enumerated Set Wizard

To activate the New Enumerated Set Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newenuset_edit.png}$ button located in the tool bar. Pressing the button bring up the window shown in Figure 3.22.

$\includegraphics{img/reference/ref_01_eventb_editor5.png}$

Figure 3.22: New Enumerated Set Wizard

Enter the name of the new enumerated set as well as the names of its elements. By pressing the More Elements button, you can enter additional elements. When you’re finished, press the OK button. The benefit of using this wizard is that in addition to creating the set and its elements, the wizard automatically creates the axiom that is necessary for the context to work. For example, when you add the new carrier set COLOUR and the three constants red, green, and orange, the wizard automatically creates the following axiom

$partition(COLOUR , \{ red\} , \{ green\} , \{ orange\} )$

3.1.6.3 New Constants Wizard

To activate the New Constants Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newcst_edit.png}$ button located in the tool bar. Pressing the button will bring up the window shown in Figure 3.23.

$\includegraphics{img/reference/ref_01_eventb_editor6.png}$

Figure 3.23: New Constants Wizard

You can then enter the names of a constant and an axiom which can be used to define the constant’s type. By pressing the More Axm. button you can enter additional axioms. To add more constants, press the Add button. When you have finished, press the OK button.

3.1.6.4 New Axioms Wizard

To activate the New Axioms Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newaxm_edit.png}$ button located in the tool bar. Pressing the button brings up the window shown in Figure 3.24.

$\includegraphics{img/reference/ref_01_eventb_editor7.png}$

Figure 3.24: New Axioms Wizard

You can then enter the axioms you want. If more axioms are needed, press the More button. When you are finished, press the OK button.

Check the “Theorem" checkbox if the corresponding axiom that you created should be marked as a a theorem.

3.1.6.5 New Variable Wizard

To activate the New Variable Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newvar_edit.png}$ button located in the tool bar. Pressing the button brings up the window shown in Figure 3.25.

$\includegraphics{img/reference/ref_01_eventb_editor14.png}$

Figure 3.25: New Variable Wizard

You can then enter the names of the variable, what its state at initialisation should be, and an invariant which defines its type. By pressing button More Inv., you can enter additional invariants. To add more variables, press the Add button. When you’re finished, press the OK button.

3.1.6.6 New Invariants Wizard

To activate the New Invariants Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newinv_edit.png}$ button located in the tool bar. Pressing the button bring up the window shown in Figure 3.26.

$\includegraphics{img/reference/ref_01_eventb_editor15.png}$

Figure 3.26: New Invariants Wizard

You can then enter the invariants you want. If more invariants are needed, press the More button. Check the Theorem checkbox to indicate that the corresponding invariant should be marked as a theorem.

3.1.6.7 New Event Wizard

To activate the New Events Wizard, press the $\includegraphics[height=2ex]{img/icons/rodin/newevt_edit.png}$ button located in the tool bar. Pressing this button brings up the window shown in Figure 3.27.

$\includegraphics[width=0.7\textwidth ]{img/reference/ref_01_eventb_editor16.png}$

Figure 3.27: New Event Wizard

You can then enter the events that you want. As indicated, the following elements can be entered: name, parameters, guards, and actions. More parameters, guards and actions can be entered by pressing the corresponding buttons. If more events are needed, press the Add button. Press the OK button when you’re finished.

Note that an event with no guard is considered to the guard $true$ . Also, an event with no action is considered to have the action $skip$ .

Rodin Handbook