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 (Soton) feature under the Composition and Decomposition 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

The above example describes generic instantiation applied to individual machines. Although it is already an interesting way of reusing, in a large model it would be more interesting to instantiate a chain of machines, or in other words instantiate a chain of refinement. Considering the below figure, suppose we have a development (problem) containing several refinement levels ($P_0$ ;... ; $P_k$). The most concrete model $P_k$ matches a generic model (pattern) $G_0$ that is part of a chain of refinement $G_0$ ;... ;$G_j$ ;... ; $G_m$. By applying generic instantiation we instantiate the pattern $G_0$ according to $P_k$. That instantiation is a refinement of $P_k$ and it is called $GI_0$. In addition we can extend the instantiation to one of the refinement layers of the pattern and apply it to the problem development. As an outcome we get a further refinement layer for $P_k$ for free ($GI_0$ corresponds to the instantiation of $G_0$ and $GI_n$ corresponds to the instantiation of $G_m$). The refinement between $GI_0$ and $GI_n$ does not introduce refinement proof obligations since the proof obligations were already discharged in the pattern chain. This follows from the instantiated machines where it is avoided the re-proof of pattern proof obligations. Afterwards $GI_n$ can be further refined to $P_{k+n}$.