Difference between revisions of "Generic Instantiation User Guide"

From Event-B
Jump to: navigation, search
m (Usage)
m (Usage)
Line 22: Line 22:
 
[[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''. The machine specifies transfering of some messages from a sender to a receiver.
  
* Context ''size_ctx'' contains constant ''max_size'' representing the maximum number messages allowed in a channel.
+
* Context ''size_ctx'' contains constant ''channel_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'']]
  
* Machine ''EO'' sees ''message_ctx'', ''size_ctx'' and refines ''channel''.
+
* 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''.
+
* 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:
 
The ''Negotiation'' project contains the following contexts:

Revision as of 09:51, 15 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.
Error creating thumbnail: Unable to save thumbnail to destination
  • 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.
Error creating thumbnail: Unable to save thumbnail to destination
  • 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 (in terms of number of messages) of the connection between partners
Error creating thumbnail: Unable to save thumbnail to destination
  • Context proposal_ctx contains carrier set PROPOSAL representing the proposals sending between partners.
Error creating thumbnail: Unable to save thumbnail to destination

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.