Generic Instantiation Plug-in User Guide

Introduction

The Generic Instantiation (GI) Feature plug-in allows to instantiate and reuse generic developments in other formal developments..

See the Generic Instantiation page for technical details.

Installing and Updating

Setup

The following steps will guide you through the setup process:

1. Download Rodin for your platform.
2. Extract the downloaded zip file.
3. Start Rodin from the folder where you extracted the zip file in the previous step.
4. Install the Generic Instantiation Feature plug-in:
   1. In the menu choose Help -> Install New Software...
   2. In the Work with dropdown list, choose the location URL: Rodin
   3. Select the Generic Instantiation Feature feature under the Utilities category, then click the check box
   4. Click Next, after some time, the Install Details page appears
   5. Click Next and accept the license
   6. Click Finish
   7. A Security Warning window may appear: click OK
5. Restart Rodin as suggested.

Now you are ready to use the Generic Instantiation Feature plug-in.

Update

The following steps will guide you through the update process:

1. In Rodin open the preferences (Window -> Preferences or for Mac: Rodin -> Preferences)
2. Find Install/Update -> Automatic Updates
3. Select Automatically find new updates and notify me

As soon as Rodin finds a new update it will ask you if you would like to install it.

Release Notes

See the Generic Instantiation Feature Release History.

Instantiating

The example followed here to demonstrate the GI plug-in is from File:Supporting Reuse of Event-B Developments through Generic Instantiation.pdf

Running the Instantiate Action

The Instantiate action launches the instantiation wizard, which will perform the generic instantiation according to the preferences. It is available:

1. Either from the toolbar of the Event-B explorer.	2. Or from the contextual menu, when right-clicking on a machine.

Selecting the Pattern Machine and Problem Machine

• Pattern machine is the machine to be instantiated and reuse.
• Problem machine (optional) is the machine to be refined by the instantiating machine. In other words, the instantiating machine is a refinement of the problem machine.

Replacing Sets and Constants

All sets and constants from the pattern context must be replaced by the available sets and constants in the context seen by instantiating machine.

Renaming Variables and Events

Variables and events (also event parameters) can be renamed.

The HTML Editor

The HTML tab editor provides an overall view of the instantiation.

Refinement Instantiation