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.
What it is
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, provides simple user interface for choosing Event-B elements such as machines, events, variables etc, and caches the user input (see later).
User input cache
The plugin provides 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 in enterString(..), enterEvent(..) etc. The operations starting with input do the following:
- check the cache for existing objects, and return if the object is in the cache
- if there is no object in the cache with the given id, then ask user to enter the object
- 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.
Full list of provided operations
enterString(userMessage:String):String
enterString(userMessage, _default:String):String enterInt(userMessage:String):Integer enterInt(userMessage:String, _default:Integer):String inputString(id:String):String inputString(id, userMessage:String):String inputString(id,userMessage,_default:String):String inputInt(id:String):Integer inputInt(id,userMessage:String):Integer inputInt(id,userMessage:String, _default:Integer):Integer |
Operations that provide input of basic strings and integers from user. Present a simple dialog using userMessage as a description of what the user is supposed to enter. If specified, _default gives a default value for the dialog input field.
inputX operations additionally check the input cache. If the cache contains an object with the key id then the object is returned and no dialog is shown. Otherwise the user enters the requested object, and the operation puts the latter into the cache under the key id. |
inputMachine(id:String):Machine
inputMachine(id,userMessage:String):Machine inputMachine(id,userMessage,fileName:String):Machine inputContext(id:String):Context inputContext(id,userMessage:String):Context inputContext(id,userMessage,fileName:String):Context Machine enterEvent(userMessage:String):Event Machine enterVariable(userMessage:String):Variable Machine inputEvent(id:String):Event Machine inputEvent(id,userMessage:String):Event Machine inputVariable(id:String):Variable Machine inputVariable(id,userMessage:String):Variable |
Ask user to choose an Event-B machine/context/event/variable.
The dialogs present a list of appropriate elements: machines and contexts are from the current project, events and variables are from the specified machine. The inputX operations check the input cache against a given id key, and put the chosen elements into the cache. If fileName is specified, then the machine/context with the given name is loaded and the dialog is not shown. |
Machine findEvent(name: String): Event
Event findWitness(name: String): Witness Event findParameter(name: String): Parameter Event findGuard(name: String): Guard Event findAction(name:String):Action Machine findVariable(name: String): Variable Machine findInvariant(name: String): Invariant Context findConstant(name: String): Constant Context findSet(name: String): CarrierSet Context findAxiom(name: String): Axiom |
Return the child element with the given name if it exists. Return null otherwise.
Example: m.findEvent("send") will return the event named "send" of the machine m if it exists, or null. |
Machine newEvent(name: String) : Event
Machine newEvent(name,id: String) : Event Event newWitness(name, predicate: String): Witness Event newParameter(name: String): Parameter Event newGuard(name, predicate: String):Guard Event newAction(name, predicate: String): Action Machine newVariable(name: String) : Variable Machine newVariable(name,id:String) : Variable Machine newInvariant(name, predicate: String): Invariant Context newConstant(name: String) : Constant Context newSet(name: String): CarrierSet Context newAxiom(name, predicate: String): Axiom |
Create and return new child element within a given element. If the element with name already exists, then return the existing one. For witnesses, guards, actions, invariants and axioms, a predicate must be specified. If id is specified, then add to the cache. |
Machine inputOrNewEvent(id,userMessage:String):Event
Machine inputOrNewVariable(id,userMessage:String):Variable |
Ask user to enter event/variable, or creates a new one based on user input. If there are no events/variables in the machine or a user clicks Cancel during the first dialog, operations ask user to enter a name for the new element and create it.
Uses the input cache as in other operations. |
Machine addEvent(name:String):Machine
Machine addEvent(name,id:String):Machine Event addWitness(name, predicate: String): Event Event addParameter(name: String): Event Event addGuard(name, predicate: String) : Event Event addAction(name, predicate: String) : Event Machine addVariable(name: String):Machine Machine addVariable(name,id: String):Machine Machine addInvariant(name, predicate: String): Machine Context addConstant(name: String): Context Context addSet(name: String): Context Context addAxiom(name, predicate: String): Context |
Add a child element with the given name (and predicate where appropriate). If id is specified, then add to the cache. Equivalent to new* operations, the only difference is that add* operations return the parent object as opposed to the newly created one. This allows structuring multiple creations in a better way:
var m:Machine = ...; m.addVariable("stop") .addInvariant("stop_inv", "fail=TRUE => stop=TRUE") .newEvent("stop") .addGuard("stop_grd", "error=TRUE") .addAction("fail_act", "fail:=TRUE") .addAction("stop_act", "stop:=TRUE"); Note how different elements can be added into the model without introducing unnecessary variables. |
Machine addRefines(name:String):Machine
Machine addRefines(machine:Machine):Machine Machine addSees(name:String):Machine Machine addSees(context:Context):Machine |
Add machine/context to the appropriate list of refined machines / seen contexts. Can be also given by their names. Return the container machine. |
Machine getRefines(): Machine
Machine getSees(): Context |
Return the first machine in the list of refined machines, and context in the list of seen contexts. If the according list is empty, then ask user for a machine/context and add the entered object in the appropriate list. Does not cache. |