Difference between pages "Generic Instantiation Plug-in User Guide" and "File:SluiceController.png"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Asiehsalehi
 
(Maintenance script uploaded File:SluiceController.png)
 
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]]
 

Latest revision as of 20:50, 30 April 2020

General diagram for the sluice controller example