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 using EOL. The description of syntax and facilities provided by Epsilon can be found in the first few sections of The Epsilon Book.

User input cache

The plugin contains a cache of objects (Event-B EMF elements and strings) entered by a user. 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");
}

If the second operation represents a separate pattern then it is safe to call it from elsewhere as the input will be redirected from cache to user.