Transformation patterns

The Transformation patterns plugin allows users to write transformation scripts in EOL (simple object-based imperative language) and easily run them over models within the same project. Editing is done in a simple text editor with syntax coloring. No compilation is needed to run transformations.

The plugin is essentially a wrapper around the Epsilon framework of interoperatable programming languages which are used to operate over the given EMF models (Event-B in our case). The plugin performs the necessary setup for running the transformations, and provides a simple library handling user input of Event-B elements such as machines, events, variables etc.

Syntax example

The following is a simple example showing a syntax of patterns when using the provided library. The pattern implements the atomicity refinement of an abstract event:

import "system.eol";
import "util.eol";

var machine: Machine = inputMachine("target");
var abstractMachine: Machine = machine.getOrInputRefines();
var absEvent: Event = abstractMachine.inputEvent("av", "Abstract event");
var counter: Variable = machine.inputOrNewVariable("cnt", "Counter variable");
var num: Integer = enterInt("Number of events");

for (i:Integer in Sequence{1..num})
{
    machine.newEvent(absEvent.name + "_ref_" + i)
             .addGuard("grd_cnt", counter.name + " = " + i)
             .addAction("act_cnt", counter.name + " := " + counter.name + "+1");
}

machine.newEvent(absEvent.name + "_ref_" + num).addRefines(absEvent);

The plugin is currently tested using EOL only, however it is theoretically possible to import and use files written in other Epsilon languages. The description of syntax and facilities provided by Epsilon can be found in the first few sections of The Epsilon Book. The full list of operations for handling user input and modifying Event-B elements can be found in Transformation_patterns/Reference

How to run a pattern

The files in the project folder with the extension .ptrn are considered to be runnable patterns. They can import .eol files (libraries) and use the operations declared there. Libraries can import other libraries etc. The tool does not give user the ability to run .eol libraries directly (although this can possibly be done through standard Epsilon tools). The suggested scenario of usage is to write the actual transformation code in .eol files as EOL operations, and call them from short .ptrn files which would look like the following:

import "system.eol";
import "my_library.eol";

var m: Machine = inputMachine("target");
m.myTransformationPattern();

All the .ptrn files would appear under the context menu (right click) of the target machine -> Run ->

On the code above, inputMachine("target") returns an EMF model of the machine upon which the pattern is run.

Pattern files are text files. To create/rename/delete them use standard Eclipse wizards and explorer.

User input cache

The plugin contains a cache of objects (EMF elements and strings) entered by a user (or external program). If during the execution a pattern requires to enter an object more than once, then at the first time the user will be asked for input, and the result will be cached. All subsequent requests will return the cached object unless the record about the object is erased.

The cache can be accessed directly from within the scripts, and used as a means to pass the objects between different transformations without them knowing the actual source of input. Thus, the input can be extended to other domain-specific EMF models.

A cache is a map from keys to values where a key consists of a type of object and its identifier, and the value is the actual cached object. The types of objects are handled by the utility library, while the identifiers must be supplied by script developer.

The operations which request input from the user without caching it all start with enter, such as enterString(..), enterEvent(..) etc. The operations starting with input do the following:

1. they check the cache for existing objects, and return if the object is in the cache
2. if there is no object in the cache with the given id, then ask user to enter the object
3. put the entered object into the cache and return to caller

The parameter id is optional. If id=null then an input* operation degenerates into enter*.

Example. If two operations request objects with the same id then only the first operation would initiate a dialog with user:

//the first operation will cache the event with id="myid"
machine.first();
//the second operation will read the event from cache if called after the first
machine.second();

operation Machine first()
{
   self.inputEvent("myid", "Choose the first event").addGuard("grd1", "stop=false");
}

operation Machine second()
{
   self.inputEvent("myid", "Choose the second event").addGuard("grd2", "q>3");
}

The second operation is also safe to call from elsewhere. In that case the cache would not contain the requested event, and the user would be asked for input.

How to install

To use the transformation pattern plugin the following are required:

1. Install the Epsilon framework from http://download.eclipse.org/modeling/gmt/epsilon/updates/
2. Install the pattern plugin from http://rodinmodeftview.sourceforge.net/
3. Copy file http://rodinmodeftview.sourceforge.net/patterns/system.eol to your project folder

Samples

atomic.ptrn

extendAll.ptrn

fmea_generate_abstract.ptrn

Good things missing

Will be added in next versions:

• Public entry point to run transformation scripts from other plugins programmatically
• Support for predicates as syntax trees. For now they're strings only

References

• Epsilon site
• The Epsilon Book
• Transformation patterns plugin update site: http://rodinmodeftview.sourceforge.net/
• Reference for provided operations: Transformation_patterns/Reference
• Developer's email: ilya.lopatkin@ncl.ac.uk