imported>Son |
imported>Son |
| Line 1: |
Line 1: |
| − | [[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
| + | The plug-in is developed by Hitachi Ltd. and ETH Zurich. |
| | {{TOCright}} | | {{TOCright}} |
| | | | |
| Line 7: |
Line 7: |
| | | | |
| | == Installing and Updating == | | == Installing and Updating == |
| − | The plug-in is available through the main Rodin Update Site under '''Composition and Decomposition''' category. | + | The plug-in is available through the following Eclipse update site. |
| | + | http://sourceforge.net/projects/gen-inst/updates |
| | | | |
| − | == News ==
| + | More information is on the [http://sourceforge.net/projects/gen-inst/files/examples/GI_Plugin_UserGuide_1_0_2.pdf User Guide]. |
| − | * 11.05.2012: Version 0.2.2 released for Rodin 2.5.*
| |
| | | | |
| − | == Technical References ==
| + | The project is hosted on sourceforge at [https://sourceforge.net/p/gen-inst/ Project homepage] |
| − | | |
| − | == Usage ==
| |
| − | We use a small example to illustrate the usage of the Generic Instantiation plug-in. The archive of the example is available
| |
| − | [http://www.example.com here], which can be imported into the Rodin platform. The archive contains to projects called ''Channel'' and ''Negotiation''. ''Channel'' is the abtract base project. ''Negotiation'' is the concrete target project: models of ''Channel'' will be instantiated within the contexts of ''Negotiation''. | |
| − | | |
| − | The ''Channel'' project contains the following components:
| |
| − | * Context ''message_ctx'' contains carrier set ''MESSAGE'' representing the set of possible messages exchanged.
| |
| − | [[Image:GenInst-message_ctx.jpg|Context ''message_ctx'']]
| |
| − | | |
| − | * Machine ''channel'' sees ''message_ctx''. The machine specifies transfering of some messages from a sender to a receiver.
| |
| − | | |
| − | * Context ''size_ctx'' contains constant ''channel_size'' representing the maximum number messages allowed in a channel.
| |
| − | [[Image:GenInst-size_ctx.jpg|Context ''size_ctx'']]
| |
| − | | |
| − | * Machine ''EO'' sees ''message_ctx'', ''size_ctx'' and refines ''channel''. The machine specifies that the messages are sent ''exactly-one''.
| |
| − | | |
| − | * Machine ''EOIO'' sees ''message_ctx'', ''size_ctx'' and refines ''EO''. The machine specifies that messages are sent ''exactly-one'' and ''in-order''.
| |
| − | | |
| − | The ''Negotiation'' project contains the following contexts:
| |
| − | * Context ''bandwidth_ctx'' contains constant ''bandwidth'' representing the bandwidth of the connection between partners
| |
| − | [[Image:GenInst-bandwidth_ctx.jpg|Context ''bandwidth_ctx'']]
| |
| − | | |
| − | * Context ''proposal_ctx'' contains carrier set ''PROPOSAL'' representing the proposals sending between partners, constant ''proposal_size'' representing the size of each proposal, and constant ''package_size'' respresenting the maximum number of proposals within each message.
| |
| − | | |
| − | [[Image:GenInst-proposal_ctx.jpg|Context ''proposal_ctx'']]
| |
| − | | |
| − | === Instantiation ===
| |
| − | We are going to instantiate the development in ''Channel'', in particular the refinement up to ''EOIO'' by instantiating the abstract carrier set ''MESSAGE'' and abstract constant ''channel_size''. Each message contains a number of proposals (no more than ''package_size''), each proposal has the size specified by ''proposal_size''. As a result, we instantiate ''MESSAGE'' by ''POW(PROPOSAL)'' and ''channel_size'' by ''bandwidth / (proposal_size * package_size)''. The instantiation is done via a wizard as follows.
| |
| − | | |
| − | * Open the New Wizard Dialog (File/New/Other) and choose Event-B Generic Instantiation.
| |
| − | [[Image:GenInst-wizard.jpg | Event-B Generic Instantiation]]
| |
| − | | |
| − | * The first page of the wizard is for choosing the different components for instantiation.
| |
| − | # Base machine: The abstract base machine. Choose ''Channel'' as the base project and ''EOIO'' as the base machine.
| |
| − | # Seen contexts: The contexts in the target projects that will be used. Choose ''Negotiation'' as the target project, and select both ''bandwidth_ctx'' and ''proposal_ctx''. Select ''Next'' to go to the next page.
| |
| − | [[Image:GenInst-wizard1.jpg | Choosing components]]
| |
| − | | |
| − | * The second page of the wizard is for entering instantiation for carrier sets and constants.
| |
| − | # Enter ''POW(PROPOSAL)'' for ''MESSAGE''
| |
| − | # Enter ''bandwidth / (proposal_size * package_size)'' for ''channel_size''
| |
| − | The expressions will be translated to Event-B mathematical expressions.
| |
| − | | |
| − | [[Image:GenInst-wizard2.jpg | Event-B Generic Instantiation]]
| |
| − | | |
| − | Select ''Next'' to go to the next page.
| |
| − | | |
| − | * The third page of the wizard is for saving the instantiation information for later use. We save the information into a file named ''GenInst''.
| |
| − | [[Image:GenInst-wizard3.jpg | Save information]]
| |
| − | | |
| − | Select ''Finish'' to complete the wizard.
| |
| − | | |
| − | * The following components are generated by the wizard.
| |
| − | # A generic instantiation file named ''GenInst''.
| |
| − | # A context named ''GenInst''.
| |
| − | # A machine named ''channel''.
| |
| − | # A machine named ''EO''.
| |
| − | # A machine named ''EOIO''.
| |
| − | The machines are copied of the original abstract machines in ''Channel'' with replacement appropriately of the carrier set and constant.
| |
| − | | |
| − | [[Image:GenInst-Result1.jpg | Generated components]]
| |
| − | | |
| − | All machines see the new context ''GenInst''. The context is as followed where the axioms of the original abstract context are instantiated accordingly and specified as theorems of the new context. At the moment the original abstract thoerems are instantiated and specified as thoerems of the new context, but the proof obligations associated with these instantiated theorems can be ignored.
| |
| − | | |
| − | [[Image:GenInst-Result2.jpg | Generated components]]
| |
| − | | |
| − | == Explanations for some warning and error messages ==
| |
| − | * '''Undefined based project'''. No based project is chosen.
| |
| − | [[Image:GenInst-UndefinedBasedProject.jpg | Undefined based project]]
| |
| − | | |
| − | * '''Undefined based machine'''. No based machine is chosen.
| |
| − | [[Image:GenInst-UndefinedBasedMachine.jpg | Undefined based machine]]
| |
| − | | |
| − | * '''Undefined target project'''. No target project is chosen.
| |
| − | [[Image:GenInst-UndefinedTargetProject.jpg | Undefined target project]]
| |
| − | | |
| − | * '''All seen carrier sets must be instantiated'''
| |
| − | [[Image:GenInst-InstantiateAllSets.jpg | All seen carrier sets must be instantiated]]
| |
| − | | |
| − | * '''All seen constants must be instantiated'''
| |
| − | [[Image:GenInst-InstantiateAllConstants.jpg | All seen constants must be instantiated]]
| |
| − | | |
| − | * ''Instantiation file existed''. The choices are to overwrite the existing file or not.
| |
| − | [[Image:GenInst-ExistingFile.jpg | Instantiation file exists]]
| |
| − | | |
| − | == Additional features to be investigated/implemented ==
| |
| − | * There is currently no sanity checking for the instantiation. Users need to make sure that their instantiated model can be analysed and proved by Rodin.
| |
| − | * Supressing proof obligations for instantiated theorems.
| |
| − | * Often ones instantiate a small part of the context rather than the whole context. Idealy, the tool should take the some minimum input and instantiate the model accordingly.
| |
