imported>Son |
imported>Son |
| (14 intermediate revisions by the same user not shown) |
| Line 1: |
Line 1: |
| − | [[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
| + | Generic Instantiation tool is developed by Yokohama Research Laboratory, Hitachi Ltd. (YRL), ETH Zurich (ETHZ) and Hitachi India Pvt. Ltd (HIL) for Event-B as a Plug-in for the RODIN platform |
| | {{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://gen-inst.sourceforge.net/updates''' |
| | | | |
| − | == News ==
| + | More information about the plug-in can be found in 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 the [https://sourceforge.net/p/gen-inst/ project homepage] |
| | | | |
| − | == Usage == | + | == Change logs == |
| − | We use a small example to illustrate the usage of the Generic Instantiation plug-in. The archive of the example is available
| + | === Version 1.1.0 === |
| − | [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''.
| + | ==== New features ==== |
| | + | # Proof of Obligation integration to Generic Instantiation file:<br>Axiom replacement<br>Well-Definedness<br> |
| | + | # PO coloring:<br>Gray scale coloring of already proven PO’s as part of the instantiated Machines |
| | + | # Navigation functionality for GI file |
| | + | # Pretty print for GI file |
| | | | |
| − | The ''Channel'' project contains the following components:
| + | === Version 1.0.3 === |
| − | * Context ''message_ctx'' contains carrier set ''MESSAGE'' representing the set of possible messages exchanged.
| + | ==== Compatibility upgrade ==== |
| − | [[Image:GenInst-message_ctx.jpg|Context ''message_ctx'']]
| + | # Compatibility upgrade for Rodin 3.0.x |
| | | | |
| − | * Machine ''channel'' sees ''message_ctx''. The machine specifies transfering of some messages from a sender to a receiver.
| + | === Version 1.0.0 === |
| − | | + | ==== (Initial) features ==== |
| − | * Context ''size_ctx'' contains constant ''channel_size'' representing the maximum number messages allowed in a channel.
| + | # Generic Instantiation (GI) files for storing information about generic instantiation. |
| − | [[Image:GenInst-size_ctx.jpg|Context ''size_ctx'']]
| + | # Wizard for creating GI files. |
| − | | + | # Editor for GI files. |
| − | * Machine ''EO'' sees ''message_ctx'', ''size_ctx'' and refines ''channel''. The machine specifies that the messages are sent ''exactly-one''.
| + | # Static checker for GI files. |
| − | | + | # Performing generic instantiation by creating a new project based on a source project and generic instantiation files. |
| − | * 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 carrier sets must be instantiated'''
| |
| − | [[Image:GenInst-InstantiateAllSets.jpg | All carrier sets must be instantiated]]
| |
| − | | |
| − | == 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.
| |
