imported>Asiehsalehi |
|
Line 1: |
Line 1: |
− | == Introduction ==
| + | General diagram for the sluice controller example |
− | The Generic Instantiation (GI) Feature plug-in allows to instantiate and reuse generic developments in other formal developments..
| |
− | | |
− | See the [http://wiki.event-b.org/index.php/Generic_Instantiation 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 Feature'' feature under the ''Utilities'' 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''
| |
− | # Restart Rodin as suggested.
| |
− | | |
− | [[Image:GI_Install.jpg|center]]
| |
− | | |
− | 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 [http://wiki.event-b.org/index.php/Generic_Instantiation_Release_History Generic Instantiation Feature Release History].
| |
− | | |
− | == Instantiating ==
| |
− | | |
− | The example followed here to demonstrate the GI plug-in is from [[Image:Supporting_Reuse_of_Event-B_Developments_through_Generic_Instantiation.pdf | Supporting Reuseof Event-B Developments through Generic Instantiation]]
| |
− | === Running the Instantiate Action ===
| |
− | The <tt>Instantiate</tt> 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.
| |
− | |-
| |
− | | valign="top" | [[Image:Ins_Explorer.jpg|center]]
| |
− | | valign="top" | [[Image:Ins_Contextual.jpg|center]]
| |
− | |}
| |
− | | |
− | === 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.
| |
− | | |
− | [[Image:GI_Wizard.jpg|center]]
| |
− | | |
− | === 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.
| |
− | | |
− | [[Image:Replace_Set_Constant.jpg|center]]
| |
− | | |
− | === Renaming Variables and Events ===
| |
− | | |
− | Variables and events (also event parameters) can be renamed.
| |
− | | |
− | [[Image:Rename_Var_Eve.jpg|center]]
| |
− | | |
− | == The HTML Editor ==
| |
− | | |
− | The HTML tab editor provides an overall view of the instantiation.
| |
− | | |
− | [[Image:GI_HTML.jpg|center]]
| |
− | | |
− | == 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 re�finements. Considering the below figure, suppose we have a development (problem) containing several re�nement levels (P0; ...; Pk). The most concrete model Pk matches a generic model (pattern) G0 that is part of a chain of refi�nements G1; ...; Gj; ...;Gm. 10. By applying generic instantiation we instantiate the pattern G0 according to Pk. That instantiation is a re�finement of Pk and it is called GI0. In addition we can extend the instantiation to one of the re�finement layers of the pattern and apply it to the problem development. As an outcome we get a further refinement layer for Pk for free (GI0 corresponds to the instantiation of G0 and GIn corresponds to the instantiation of Gm). The re�finement between GI0 and GIn does not introduce re�finement 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 GIn can be further refined to Pk+n.
| |
− | | |
− | [[Image:GI_Refinement.jpg|center]]
| |