Transformation patterns: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Ilya.lopatkin
mNo edit summary
imported>Ilya.lopatkin
mNo edit summary
Line 46: Line 46:


| 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.
| 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'''.
'''input*''' 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:String):Machine
Line 73: Line 73:


|Ask user to choose an Event-B machine/context/event/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.
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 '''input*''' 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.
If '''fileName''' is specified, then the machine/context with the given name is loaded and the dialog is not shown.
|-
|-
Line 154: Line 154:


Context addAxiom(name, predicate: 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:
|Add a child element with the given '''name''' (and '''predicate''' where appropriate) and return the parent element. If '''id''' is specified, then also add to the cache. Equivalent to '''new*''' operations, the 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 = ...;
  var m:Machine = ...;
  m.addVariable("stop")
  m.addVariable("stop")
Line 162: Line 162:
     .addAction("fail_act", "fail:=TRUE")
     .addAction("fail_act", "fail:=TRUE")
     .addAction("stop_act", "stop:=TRUE");
     .addAction("stop_act", "stop:=TRUE");
Note how different elements can be added into the model without introducing unnecessary variables.
Note how different elements can be added to the model without introducing unnecessary variables.
|-
|-
|Machine addRefines(name:String):Machine
|Machine addRefines(name:String):Machine
Line 177: Line 177:


Machine getSees(): Context
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.
|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 check the cache.
|}
|}

Revision as of 12:10, 29 June 2011

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:

  1. 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.

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.

input* 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 input* 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) and return the parent element. If id is specified, then also add to the cache. Equivalent to new* operations, the 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 to 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 check the cache.