# Generic Instantiation Plug-in User Guide

## Contents

## 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:

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

- In the menu choose
- 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:

- In Rodin open the preferences (
*Window*->*Preferences*or for Mac:*Rodin*->*Preferences*) - Find
*Install/Update*->*Automatic Updates* - 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. |

Error creating thumbnail: Unable to save thumbnail to destination |
Error creating thumbnail: Unable to save thumbnail to destination |

### 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 (<math>P_0</math> ;... ; <math>P_k</math>). The most concrete model <math>P_k</math> matches a generic model (pattern) <math>G_0</math> that is part of a chain of refinement <math>G_0</math> ;... ;<math>G_j</math> ;... ; <math>G_m</math>. By applying generic instantiation we instantiate the pattern <math>G_0</math> according to <math>P_k</math>. That instantiation is a refinement of <math>P_k</math> and it is called <math>GI_0</math>. 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 <math>P_k</math> for free (<math>GI_0</math> corresponds to the instantiation of <math>G_0</math> and <math>GI_n</math> corresponds to the instantiation of <math>G_m</math>). The refinement between <math>GI_0</math> and <math>GI_n</math> 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 <math>GI_n</math> can be further refined to <math>P_{k+n}</math>.