https://wiki.event-b.org/index.php?title=Transformation_patterns/Reference&feed=atom&action=history
Transformation patterns/Reference - Revision history
2024-03-28T13:32:43Z
Revision history for this page on the wiki
MediaWiki 1.33.3
https://wiki.event-b.org/index.php?title=Transformation_patterns/Reference&diff=10439&oldid=prev
imported>Ilya.lopatkin at 16:38, 29 June 2011
2011-06-29T16:38:58Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 16:38, 29 June 2011</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l53" >Line 53:</td>
<td colspan="2" class="diff-lineno">Line 53:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>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.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>If '''fileName''' is specified, then the machine/context with the given name is loaded and the dialog is not shown.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>If '''fileName''' is specified, then the machine/context with the given name is loaded and the dialog is not shown.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">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:</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"> var m:Machine = inputMachine("target");</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|-</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|-</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|Machine findEvent(name: String): Event</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|Machine findEvent(name: String): Event</div></td></tr>
<tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l149" >Line 149:</td>
<td colspan="2" class="diff-lineno">Line 153:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Machine addSees(context:Context):Machine</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Machine addSees(context:Context):Machine</div></td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>|Add '''machine'''/'''context''' to the appropriate list of refined machines / seen contexts. Can be also given by their '''name'''s. Return the container machine.</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">Event addRefines(name:String):Event</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div> </div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins class="diffchange diffchange-inline">Event addRefines(event:Event):Event</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>|Add '''machine'''/'''context<ins class="diffchange diffchange-inline">'''/'''event</ins>''' to the appropriate list of refined machines / seen contexts <ins class="diffchange diffchange-inline">/ refined events</ins>. Can be also given by their '''name'''s. Return the container machine<ins class="diffchange diffchange-inline">/event</ins>.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|-</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|-</div></td></tr>
<tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l155" >Line 155:</td>
<td colspan="2" class="diff-lineno">Line 163:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Machine getSees(): Context</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Machine getSees(): Context</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|Return the first machine in the list of refined machines, and context in the list of seen contexts.</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|Machine getOrInputRefines():Machine</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">Machine getOrInputSees():Context</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|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.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|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.</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|}</div></td></tr>
</table>
imported>Ilya.lopatkin
https://wiki.event-b.org/index.php?title=Transformation_patterns/Reference&diff=10438&oldid=prev
imported>Ilya.lopatkin at 13:21, 29 June 2011
2011-06-29T13:21:05Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 13:21, 29 June 2011</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>== <del class="diffchange diffchange-inline">Full list </del>of operations provided in system.eol ==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== <ins class="diffchange diffchange-inline">List </ins>of operations provided in system.eol ==</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"</div></td></tr>
<tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l156" >Line 156:</td>
<td colspan="2" class="diff-lineno">Line 156:</td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Machine getSees(): Context</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>Machine getSees(): Context</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|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.</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|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.</div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|}</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">== List of operations provided in util.eol ==</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|Machine addGuardToAll(name, predicate: String): Machine</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|Add a guard specified by its '''name''' and '''predicate''' to all events of the machine except initialisation</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|-</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|Machine addTypingInvariant(v: Variable, type:String): Machine</ins></div></td></tr>
<tr><td colspan="2"> </td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">|Add an invariant specifying the variable '''v''' having the type '''type'''</ins></div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|}</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>|}</div></td></tr>
</table>
imported>Ilya.lopatkin
https://wiki.event-b.org/index.php?title=Transformation_patterns/Reference&diff=10437&oldid=prev
imported>Ilya.lopatkin at 12:52, 29 June 2011
2011-06-29T12:52:21Z
<p></p>
<table class="diff diff-contentalign-left" data-mw="interface">
<col class="diff-marker" />
<col class="diff-content" />
<col class="diff-marker" />
<col class="diff-content" />
<tr class="diff-title" lang="en-GB">
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Older revision</td>
<td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revision as of 12:52, 29 June 2011</td>
</tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td></tr>
<tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>== Full list of provided <del class="diffchange diffchange-inline">operations </del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Full list of <ins class="diffchange diffchange-inline">operations </ins>provided <ins class="diffchange diffchange-inline">in system.eol </ins>==</div></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr>
<tr><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"</div></td><td class='diff-marker'> </td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"</div></td></tr>
</table>
imported>Ilya.lopatkin
https://wiki.event-b.org/index.php?title=Transformation_patterns/Reference&diff=10436&oldid=prev
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
<p>New page: == Full list of provided operations == {|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%" |- | enterString(userMessage:String):String enterString(userMessage, _de...</p>
<p><b>New page</b></p><div>== Full list of provided operations ==<br />
<br />
{|border="1" cellpadding="10" cellspacing="0" align="center" width = "70%"<br />
|-<br />
| enterString(userMessage:String):String<br />
<br />
enterString(userMessage, _default:String):String<br />
<br />
enterInt(userMessage:String):Integer<br />
<br />
enterInt(userMessage:String, _default:Integer):String<br />
<br />
inputString(id:String):String<br />
<br />
inputString(id, userMessage:String):String<br />
<br />
inputString(id,userMessage,_default:String):String<br />
<br />
inputInt(id:String):Integer<br />
<br />
inputInt(id,userMessage:String):Integer<br />
<br />
inputInt(id,userMessage:String, _default:Integer):Integer<br />
<br />
| 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.<br />
'''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'''.<br />
|-<br />
|inputMachine(id:String):Machine<br />
<br />
inputMachine(id,userMessage:String):Machine<br />
<br />
inputMachine(id,userMessage,fileName:String):Machine<br />
<br />
inputContext(id:String):Context<br />
<br />
inputContext(id,userMessage:String):Context<br />
<br />
inputContext(id,userMessage,fileName:String):Context<br />
<br />
Machine enterEvent(userMessage:String):Event<br />
<br />
Machine enterVariable(userMessage:String):Variable<br />
<br />
Machine inputEvent(id:String):Event<br />
<br />
Machine inputEvent(id,userMessage:String):Event<br />
<br />
Machine inputVariable(id:String):Variable<br />
<br />
Machine inputVariable(id,userMessage:String):Variable<br />
<br />
|Ask user to choose an Event-B machine/context/event/variable.<br />
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.<br />
If '''fileName''' is specified, then the machine/context with the given name is loaded and the dialog is not shown.<br />
|-<br />
|Machine findEvent(name: String): Event<br />
<br />
Event findWitness(name: String): Witness<br />
<br />
Event findParameter(name: String): Parameter<br />
<br />
Event findGuard(name: String): Guard<br />
<br />
Event findAction(name:String):Action<br />
<br />
Machine findVariable(name: String): Variable<br />
<br />
Machine findInvariant(name: String): Invariant<br />
<br />
Context findConstant(name: String): Constant<br />
<br />
Context findSet(name: String): CarrierSet<br />
<br />
Context findAxiom(name: String): Axiom<br />
|Return the child element with the given '''name''' if it exists. Return null otherwise.<br />
Example:<br />
m.findEvent("send")<br />
will return the event named "send" of the machine m if it exists, or null.<br />
|-<br />
|Machine newEvent(name: String) : Event<br />
<br />
Machine newEvent(name,id: String) : Event<br />
<br />
Event newWitness(name, predicate: String): Witness<br />
<br />
Event newParameter(name: String): Parameter<br />
<br />
Event newGuard(name, predicate: String):Guard<br />
<br />
Event newAction(name, predicate: String): Action<br />
<br />
Machine newVariable(name: String) : Variable<br />
<br />
Machine newVariable(name,id:String) : Variable<br />
<br />
Machine newInvariant(name, predicate: String): Invariant<br />
<br />
Context newConstant(name: String) : Constant<br />
<br />
Context newSet(name: String): CarrierSet<br />
<br />
Context newAxiom(name, predicate: String): Axiom<br />
|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.<br />
|-<br />
|style=white-space:nowrap|Machine inputOrNewEvent(id,userMessage:String):Event<br />
<br />
Machine inputOrNewVariable(id,userMessage:String):Variable<br />
|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.<br />
Uses the input cache as in other operations.<br />
|-<br />
|Machine addEvent(name:String):Machine<br />
<br />
Machine addEvent(name,id:String):Machine<br />
<br />
Event addWitness(name, predicate: String): Event<br />
<br />
Event addParameter(name: String): Event<br />
<br />
Event addGuard(name, predicate: String) : Event<br />
<br />
Event addAction(name, predicate: String) : Event<br />
<br />
Machine addVariable(name: String):Machine<br />
<br />
Machine addVariable(name,id: String):Machine<br />
<br />
Machine addInvariant(name, predicate: String): Machine<br />
<br />
Context addConstant(name: String): Context<br />
<br />
Context addSet(name: String): Context<br />
<br />
Context addAxiom(name, predicate: String): Context<br />
|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:<br />
var m:Machine = ...;<br />
m.addVariable("stop")<br />
.addInvariant("stop_inv", "fail=TRUE => stop=TRUE")<br />
.newEvent("stop")<br />
.addGuard("stop_grd", "error=TRUE")<br />
.addAction("fail_act", "fail:=TRUE")<br />
.addAction("stop_act", "stop:=TRUE");<br />
Note how different elements can be added to the model without introducing unnecessary variables.<br />
|-<br />
|Machine addRefines(name:String):Machine<br />
<br />
Machine addRefines(machine:Machine):Machine<br />
<br />
Machine addSees(name:String):Machine<br />
<br />
Machine addSees(context:Context):Machine<br />
|Add '''machine'''/'''context''' to the appropriate list of refined machines / seen contexts. Can be also given by their '''name'''s. Return the container machine.<br />
<br />
|-<br />
|Machine getRefines(): Machine<br />
<br />
Machine getSees(): Context<br />
|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.<br />
|}</div>
imported>Ilya.lopatkin