Generic Instantiation Plug-in User Guide

From Event-B
Jump to navigationJump to search

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.
GI Install.jpg

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.
Ins Explorer.jpg
Ins Contextual.jpg

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.
GI Wizard.jpg

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.

Replace Set Constant.jpg

Renaming Variables and Events

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

Rename Var Eve.jpg

The HTML Editor

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

GI HTML.jpg

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}.

GI Refinement.jpg