Generic Instantiation User Guide

From Event-B
Revision as of 02:25, 18 August 2014 by Son (talk | contribs) (Change logs for version 1.0.3)
Jump to: navigation, search

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


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:

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 for 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

Change logs for version 1.0.3

Compatibility upgrade

  1. Compatibility upgrade for Rodin 3.0.x

Change logs for 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.