Transformation patterns/Reference

From Event-B
Jump to navigationJump to search

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.

The machine upon which the current script is running is put in the cache under the id target. So one should use the following to retrieve the target machine:

var m:Machine = inputMachine("target");
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

Event addRefines(name:String):Event

Event addRefines(event:Event):Event

Add machine/context/event to the appropriate list of refined machines / seen contexts / refined events. Can be also given by their names. Return the container machine/event.
Machine getRefines(): Machine

Machine getSees(): Context

Return the first machine in the list of refined machines, and context in the list of seen contexts.
Machine getOrInputRefines():Machine

Machine getOrInputSees():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