Generic Instantiation User Guide: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Son m →Usage |
imported>Son m →Usage |
||
| Line 19: | Line 19: | ||
The ''Channel'' project contains the following components: | The ''Channel'' project contains the following components: | ||
* Context ''message_ctx'' contains carrier set ''MESSAGE'' | * Context ''message_ctx'' contains carrier set ''MESSAGE'' representing the set of possible messages exchanged. | ||
[[Image:GenInst-message_ctx.jpg|Context ''message_ctx'']] | [[Image:GenInst-message_ctx.jpg|Context ''message_ctx'']] | ||
* Machine ''channel'' sees ''message_ctx''. | * Machine ''channel'' sees ''message_ctx''. | ||
* Context ''size_ctx'' contains constant ''max_size'' | * Context ''size_ctx'' contains constant ''max_size'' representing the maximum number messages allowed in a channel. | ||
[[Image:GenInst-size_ctx.jpg|Context ''size_ctx'']] | [[Image:GenInst-size_ctx.jpg|Context ''size_ctx'']] | ||
| Line 31: | Line 31: | ||
* Machine ''EOIO'' sees ''message_ctx'', ''size_ctx'' and refines ''EO''. | * Machine ''EOIO'' sees ''message_ctx'', ''size_ctx'' and refines ''EO''. | ||
The '' | The ''Negotiation'' project contains the following contexts: | ||
* Context ''bandwidth_ctx'' contains constant ''bandwidth'' | * Context ''bandwidth_ctx'' contains constant ''bandwidth'' representing the bandwidth (in terms of number of messages) of the connection between partners | ||
[[Image:GenInst-bandwidth_ctx.jpg|Context ''bandwidth_ctx'']] | [[Image:GenInst-bandwidth_ctx.jpg|Context ''bandwidth_ctx'']] | ||
* Context ''proposal_ctx'' contains carrier set ''PROPOSAL''. | * Context ''proposal_ctx'' contains carrier set ''PROPOSAL'' representing the proposals sending between partners. | ||
[[Image:GenInst-proposal_ctx.jpg|Context ''proposal_ctx'']] | [[Image:GenInst-proposal_ctx.jpg|Context ''proposal_ctx'']] | ||
== Additional features to be investigated/implemented == | == 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. | * 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. | ||
Revision as of 16:12, 14 May 2012
User:Son at ETH Zurich is in charge of the plug-in.
Introduction
The Generic Instantiation plug-in provides supports for instantiating an Event-B Models by providing concrete values for carrier sets and constants.
Installing and Updating
The plug-in is available through the main Rodin Update Site under Composition and Decomposition category.
News
- 11.05.2012: Version 0.2.2 released for Rodin 2.5.*
Technical References
Usage
We use a small example to illustrate the usage of the Generic Instantiation plug-in. The archive of the example is available 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.
- Machine channel sees message_ctx.
- Context size_ctx contains constant max_size representing the maximum number messages allowed in a channel.
- Machine EO sees message_ctx, size_ctx and refines channel.
- Machine EOIO sees message_ctx, size_ctx and refines EO.
The Negotiation project contains the following contexts:
- Context bandwidth_ctx contains constant bandwidth representing the bandwidth (in terms of number of messages) of the connection between partners
- Context proposal_ctx contains carrier set PROPOSAL representing the proposals sending between partners.
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.
