Difference between revisions of "Generic Instantiation User Guide"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Son
m
 
(34 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'' represent 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''.
+
=== Version 1.0.0 ===
−
 
+
==== (Initial) features ====
−
* Context ''size_ctx'' contains constant ''max_size'' represent 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''.
+
# 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 ''Negotiatino'' project contains the following contexts:
 
−
* Context ''bandwidth_ctx'' contains constant ''bandwidth''.
 
−
[[Image:GenInst-bandwidth_ctx.jpg|Context ''bandwidth_ctx'']]
 
−
 
 
−
* Context ''proposal_ctx'' contains carrier set ''PROPOSAL''.
 
−
[[Image:GenInst-proposal_ctx.jpg|Context ''proposal_ctx'']]
 
−
 
 
−
== 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.
 

Latest revision as of 01:40, 18 August 2014

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

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 following Eclipse update site: http://gen-inst.sourceforge.net/updates

More information about the plug-in can be found in the User Guide.

The project is hosted on sourceforge at the project homepage

Change logs

Version 1.1.0

New features

  1. Proof of Obligation integration to Generic Instantiation file:
    Axiom replacement
    Well-Definedness
  2. PO coloring:
    Gray scale coloring of already proven PO’s as part of the instantiated Machines
  3. Navigation functionality for GI file
  4. Pretty print for GI file

Version 1.0.3

Compatibility upgrade

  1. Compatibility upgrade for Rodin 3.0.x

Version 1.0.0

(Initial) features

  1. Generic Instantiation (GI) files for storing information about generic instantiation.
  2. Wizard for creating GI files.
  3. Editor for GI files.
  4. Static checker for GI files.
  5. Performing generic instantiation by creating a new project based on a source project and generic instantiation files.
Retrieved from ‘https://wiki.event-b.org/index.php?title=Generic_Instantiation_User_Guide&oldid=5431’