Difference between revisions of "Atomicity Decomposition Plug-in User Guide"

From Event-B
Jump to navigationJump to search
imported>Asiehsalehi
imported>Asiehsalehi
Line 8: Line 8:
 
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.  
 
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 Updating ==
+
== Installing and Requirements ==
  
 
=== Setup ===
 
=== Setup ===
 
The following steps will guide you through the setup process:
 
The following steps will guide you through the setup process:
−
# Download Rodin for your platform from [http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714&release_id=687381 Sourceforge].
+
## Start Rodin.
−
# Extract the downloaded zip file.
 
−
# Start Rodin from the folder where you extracted the zip file in the previous step.
 
−
# Install the Atomicity Decomposition plug-in:
 
 
## In the menu choose ''Help'' -> ''Install New Software...''
 
## 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]
 
## 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]
Line 23: Line 20:
 
## Click ''Finish''
 
## Click ''Finish''
 
## A ''Security Warning'' window may appear: click ''OK''
 
## A ''Security Warning'' window may appear: click ''OK''
−
# Restart Rodin as suggested.
+
## Restart Rodin as suggested.
−
 
 
−
Now you are ready to use the Atomicity Decomposition plug-in.
 
−
 
 
−
== Requirements ==
 
  
 +
=== 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].
 
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].
−
 
−
=== Update ===
 
−
The following steps will guide you through the update process:
 
−
# In Rodin open the preferences (''Window'' -> ''Preferences'' or for Mac: ''Rodin'' -> ''Preferences'')
 
−
# Find ''Install/Update'' -> ''Automatic Updates''
 
−
# Select ''Automatically find new updates and notify me''
 
−
 
−
As soon as Rodin finds a new update it will ask you if you would like to install it.
 
  
 
== Creating Flow Diagrams ==
 
== Creating Flow Diagrams ==

Revision as of 15:44, 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

Validating Rules to Follow

Transform to Event-B

Retrieved from ‘https://wiki.event-b.org/index.php?title=Atomicity_Decomposition_Plug-in_User_Guide&oldid=850’