Transformation patterns/Reference - Revision history

imported>Ilya.lopatkin at 16:38, 29 June 2011

2011-06-29T16:38:58Z

← Older revision		Revision as of 16:38, 29 June 2011
Line 53:		Line 53:
	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.		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.

			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		\|Machine findEvent(name: String): Event
Line 149:		Line 153:

	Machine addSees(context:Context):Machine		Machine addSees(context:Context):Machine
	\|Add '''machine'''/'''context''' to the appropriate list of refined machines / seen contexts. Can be also given by their '''name'''s. Return the container 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 '''name'''s. Return the container machine/event.

	\|-		\|-
Line 155:		Line 163:

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

imported>Ilya.lopatkin at 13:21, 29 June 2011

2011-06-29T13:21:05Z

@@ Line 1: / Line 1: @@
-== Full list of operations provided in system.eol ==
+== List of operations provided in system.eol ==
 {|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"
@@ Line 156: / Line 156: @@
 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.
 |}

imported>Ilya.lopatkin at 12:52, 29 June 2011

2011-06-29T12:52:21Z

← Older revision		Revision as of 12:52, 29 June 2011
Line 1:		Line 1:
	== Full list of provided ~~operations~~ ==		== Full list of operations provided in system.eol ==

	{\|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"		{\|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"

imported>Ilya.lopatkin: New page: == Full list of provided operations == {|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%" |- | enterString(userMessage:String):String enterString(userMessage, _de...

2011-06-29T12:18:45Z

New page: == Full list of provided operations == {|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%" |- | enterString(userMessage:String):String enterString(userMessage, _de...

New page

== Full list of provided operations ==

{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"
|-
| 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.
|-
|style=white-space:nowrap|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 '''name'''s. 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.
|}