Difference between revisions of "Generic Instantiation User Guide"

From Event-B
Jump to: navigation, search
m (Usage)
m (Usage)
Line 15: Line 15:
  
 
== Usage ==
 
== Usage ==
# Abstract model.
+
We use a small example to illustrate the usage of the Generic Instantiation plug-in. The archive of the example is available
* Context ''message_ctx''
+
[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.
[[Image:GenInst-message_ctx.jpg|alt=Alt|Context message_ctx]]
 
 
 
* Machine ''channel''
 
[[Image:GenInst-channel.jpg|alt=Alt|Machine channel]]
 
 
 
* Context ''size_ctx''
 
[[Image:GenInst-size_ctx.jpg|alt=Alt|Context size_ctx]]
 
 
 
* Machine ''EO''
 
[[Image:GenInst-EO.jpg|alt=Alt|Machine EO]]
 
 
 
* Machine ''EOIO''
 
[[Image:GenInst-EOIO.jpg|alt=Alt|Machine EOIO]]
 
  
 
== 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:51, 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.

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.