Difference between pages "AnimB" and "Atomicity Decomposition Plug-in User Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
 
imported>Asiehsalehi
 
Line 1: Line 1:
[[Image:AnimB.png|100px]]
+
== Introduction ==
== Animator of B system model in the Rodin platform. ==
+
The Atomicity Decomposition (AD) plug-in allows an explicit representation of control flow and explicit representation of refinement relationships between an abstract event and the corresponding concrete events.  
  
----
+
See the [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page for technical details.
AnimB is an animator for the Rodin platform. It allows animation of complete model (all refinements), and can be used to create a complex animation with graphical interface.
+
 
----
+
Currently the AD diagrams can be defined in an EMF tree structure included in an Event-B machine which is opened by Rose editor. After defining the control flow and refinement relationships via AD diagrams, the AD diagrams can automatically transformed to the Event-B notation.
* [[AnimB_install|Install Instructions]]
+
 
* [[AnimB_start|Start an Animation]]
+
== Installing and Requirements ==
* [[AnimB Flash Tutorial|Flash Animation Tutorial]]
+
 
[[Category:User Documentation]]
+
=== Setup ===
[[Category:AnimB]]
+
The following steps will guide you through the setup process:
 +
# Start Rodin.
 +
# In the menu choose ''Help'' -> ''Install New Software...''.
 +
# In the ''Work with'' dropdown list, choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
 +
# Select the ''Atomicity Decomposition'' feature under the ''Atomicity Decomposition'' category, then click the check box.
 +
# Click ''Next'', after some time, the ''Install Details'' page appears.
 +
# Click ''Next'' and accept the license.
 +
# Click ''Finish''.
 +
# A ''Security Warning'' window may appear: click ''OK''.
 +
# Restart Rodin as suggested.
 +
 
 +
=== Requirements ===
 +
The AD plug-in requires [http://wiki.event-b.org/index.php/Rose_(Structured)_Editor Rose Editor Plug-in] and [http://wiki.event-b.org/index.php/EMF_framework_for_Event-B EMF Plug-in].
 +
 
 +
== Creating Flow Diagrams ==
 +
 
 +
First you need to open the machine in the Rose editor by right-clicking on the machine.
 +
 
 +
[[Image:machine_rose.jpg]]
 +
 
 +
Then a flow can be created:
 +
{|
 +
|-
 +
|1. Either for an Event-B machine, when right-clicking on the machine.
 +
|2. Or for a pre-defined leaf, when right-clicking on the leaf.
 +
|-
 +
| valign="top" | [[Image:flow_machine.jpg|center]]  
 +
| valign="top" | [[Image:flow_leaf.jpg|center]]
 +
|}
 +
 
 +
The following steps will guide you through a combined atomicity decomposition diagram:
 +
* Create a flow for the most abstract machine.
 +
* When refining a machine, the pre-defined flows are copied to the new (refining) machine.
 +
* In the new machine, you can create a new flow for each pre-defined leaf.
 +
 
 +
== Elements and Properties ==
 +
 
 +
For each flow, you can define one or more of the below elements, when right-clicking on the flow:
 +
* typed parameter
 +
* leaf
 +
* ''and'' constructor including two or more leaves (right-click on the ''and'')
 +
* ''or'' constructor including two or more leaves (right-click on the ''or'')
 +
* ''xor'' constructor including two or more leaves (right-click on the ''xor'')
 +
* ''all'' constructor including one leaf and one parameter (right-click on the ''all'')
 +
* ''some'' constructor including one leaf and one parameter (right-click on the ''some'')
 +
* ''one'' constructor including one leaf and one parameter (right-click on the ''one'')
 +
 
 +
[[Image:flow_children.jpg]]
 +
 
 +
=== Flow Properties ===
 +
* Name: a string containing the name of the root event.
 +
* Sw: a boolean indicates strong (''true'') / weak (''false'') sequencing.
 +
 
 +
=== Leaf Properties ===
 +
* Name: a string containing the name of the event.
 +
* Ref: a boolean indicates refining (''true'') / non-refining (''false'') event.
 +
 
 +
[[Image:leaf_properties.jpg]]
 +
 
 +
=== Constructor Properties ===
 +
* Ref: a boolean indicates refining (''true'') / non-refining (''false'') constructor (''and'' / ''or'' / ''xor'' / ''all'' / ''some'' / ''one'').
 +
NOTE: The refining property for (''and'' / ''or'' / ''all'' / ''some'') constructors has to be ''false''.
 +
 
 +
=== Parameter Properties ===
 +
* Name: a string containing the name of the parameter.
 +
* Type: a string containing the type of the parameter.
 +
NOTE: the parameter type has to be defined in the context.
 +
 
 +
== Transforming to Event-B ==
 +
 
 +
For each machine, after completing the flow construction process, you can perform the translation rules to transform the defined AD flow to the Event-B notation (For technical details see [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page). This is done by right-clicking on the machine and launch ''Atomicity Decomposition Transformation -> Transform to Event-B''.
 +
 
 +
== Validating Rules to Follow ==
 +
 
 +
In order to perform the translation rules correctly, you will need to follow these rules:
 +
(For more information about technical reasons see [http://wiki.event-b.org/index.php/Atomicity_Decomposition Atomicity Decomposition] page)
 +
 
 +
*

Revision as of 16:59, 7 August 2012

Introduction

The Atomicity Decomposition (AD) plug-in allows an explicit representation of control flow and explicit representation of refinement relationships between an abstract event and the corresponding concrete events.

See the Atomicity Decomposition page for technical details.

Currently the AD diagrams can be defined in an EMF tree structure included in an Event-B machine which is opened by Rose editor. After defining the control flow and refinement relationships via AD diagrams, the AD diagrams can automatically transformed to the Event-B notation.

Installing and Requirements

Setup

The following steps will guide you through the setup process:

  1. Start Rodin.
  2. In the menu choose Help -> Install New Software....
  3. In the Work with dropdown list, choose the location URL: Rodin - http://rodin-b-sharp.sourceforge.net/updates.
  4. Select the Atomicity Decomposition feature under the Atomicity Decomposition category, then click the check box.
  5. Click Next, after some time, the Install Details page appears.
  6. Click Next and accept the license.
  7. Click Finish.
  8. A Security Warning window may appear: click OK.
  9. Restart Rodin as suggested.

Requirements

The AD plug-in requires Rose Editor Plug-in and EMF Plug-in.

Creating Flow Diagrams

First you need to open the machine in the Rose editor by right-clicking on the machine.

Machine rose.jpg

Then a flow can be created:

1. Either for an Event-B machine, when right-clicking on the machine. 2. Or for a pre-defined leaf, when right-clicking on the leaf.
Flow machine.jpg
Flow leaf.jpg

The following steps will guide you through a combined atomicity decomposition diagram:

  • Create a flow for the most abstract machine.
  • When refining a machine, the pre-defined flows are copied to the new (refining) machine.
  • In the new machine, you can create a new flow for each pre-defined leaf.

Elements and Properties

For each flow, you can define one or more of the below elements, when right-clicking on the flow:

  • typed parameter
  • leaf
  • and constructor including two or more leaves (right-click on the and)
  • or constructor including two or more leaves (right-click on the or)
  • xor constructor including two or more leaves (right-click on the xor)
  • all constructor including one leaf and one parameter (right-click on the all)
  • some constructor including one leaf and one parameter (right-click on the some)
  • one constructor including one leaf and one parameter (right-click on the one)

Flow children.jpg

Flow Properties

  • Name: a string containing the name of the root event.
  • Sw: a boolean indicates strong (true) / weak (false) sequencing.

Leaf Properties

  • Name: a string containing the name of the event.
  • Ref: a boolean indicates refining (true) / non-refining (false) event.

Leaf properties.jpg

Constructor Properties

  • Ref: a boolean indicates refining (true) / non-refining (false) constructor (and / or / xor / all / some / one).

NOTE: The refining property for (and / or / all / some) constructors has to be false.

Parameter Properties

  • Name: a string containing the name of the parameter.
  • Type: a string containing the type of the parameter.

NOTE: the parameter type has to be defined in the context.

Transforming to Event-B

For each machine, after completing the flow construction process, you can perform the translation rules to transform the defined AD flow to the Event-B notation (For technical details see Atomicity Decomposition page). This is done by right-clicking on the machine and launch Atomicity Decomposition Transformation -> Transform to Event-B.

Validating Rules to Follow

In order to perform the translation rules correctly, you will need to follow these rules: (For more information about technical reasons see Atomicity Decomposition page)