Transformation patterns/Reference

List of operations provided in system.eol

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.

List of operations provided in util.eol

Machine addGuardToAll(name, predicate: String): Machine	Add a guard specified by its name and predicate to all events of the machine except initialisation
Machine addTypingInvariant(v: Variable, type:String): Machine	Add an invariant specifying the variable v having the type type