Atomicity Decomposition Plug-in User Guide - Revision history

imported>Asiehsalehi: /* Installing and Requirements */

2012-08-21T15:13:47Z

Installing and Requirements

← Older revision		Revision as of 15:13, 21 August 2012
Line 10:		Line 10:
	=== Requirements ===		=== Requirements ===
	The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps in order:		The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps in order:

			* Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates]. Select and install ''Event-B EMF - Support for Modelling Extensions'' and ''Event-B EMF Framework'' under the ''Frameworks'' category.


			[[Image:EMF.jpg\|center]]


	* Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.		* Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.

imported>Asiehsalehi: /* Installing and Requirements */

2012-08-21T14:32:24Z

Installing and Requirements

← Older revision		Revision as of 14:32, 21 August 2012
Line 9:		Line 9:

	=== Requirements ===		=== Requirements ===
	The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps:		The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps in order:

	# Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.		* Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.


Line 17:		Line 17:


	# Add the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.		* Add the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.


Line 24:		Line 24:

	=== Setup ===		=== Setup ===
	~~The following steps will guide you through the setup process of the AD plug-in:~~
	# Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].		* Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
	# Select and install the ''Atomicity Decomposition'' feature under the ''Modelling Extensions'' category.		* Select and install the ''Atomicity Decomposition'' feature under the ''Modelling Extensions'' category.

imported>Asiehsalehi: /* Installing and Requirements */

2012-08-21T14:31:23Z

Installing and Requirements

← Older revision		Revision as of 14:31, 21 August 2012
Line 12:		Line 12:

	# Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.		# Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.


	[[Image:EMFCompare.jpg\|center]]		[[Image:EMFCompare.jpg\|center]]


	# Add the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.		# Add the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.


	[[Image:Epsilon.jpg\|center]]		[[Image:Epsilon.jpg\|center]]


	=== Setup ===		=== Setup ===
Line 23:		Line 27:
	# Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].		# Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
	# Select and install the ''Atomicity Decomposition'' feature under the ''Modelling Extensions'' category.		# Select and install the ''Atomicity Decomposition'' feature under the ''Modelling Extensions'' category.


	[[Image:AD.jpg\|center]]		[[Image:AD.jpg\|center]]

imported>Asiehsalehi: /* Installing and Requirements */

2012-08-21T14:30:55Z

Installing and Requirements

← Older revision		Revision as of 14:30, 21 August 2012
Line 8:		Line 8:
	== Installing and Requirements ==		== Installing and Requirements ==

	=== ~~Setup~~ ===		=== Requirements ===
	The ~~following steps will guide you through~~ the ~~setup process:~~		The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, perform the below installation steps:
	~~# Start Rodin~~.
	~~# In~~ the ~~menu choose ''Help''~~ -~~> ''Install New Software...''.~~		# Choose the location URL: Indigo Update Site - [http://download.eclipse.org/releases/indigo http://download.eclipse.org/releases/indigo]. Select and install ''EMF Compare'' under the ''Modeling'' category.
	# ~~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~~ ''~~Event-B Atomicity Decomposition~~'' ~~feature~~ under the ''~~Modelling Extensions~~'' 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 ===~~		[[Image:EMFCompare.jpg\|center]]
	* The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, install Epsilon using the Epsilon update site available at [~~http~~:~~//download~~.~~eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/~~]~~. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.~~

			# Add the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.

	[[Image:Epsilon.jpg\|center]]		[[Image:Epsilon.jpg\|center]]

			=== Setup ===
			The following steps will guide you through the setup process of the AD plug-in:
			# Choose the location URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates].
			# Select and install the ''Atomicity Decomposition'' feature under the ''Modelling Extensions'' category.

			[[Image:AD.jpg\|center]]

	== Creating Flow Diagrams ==		== Creating Flow Diagrams ==

imported>Asiehsalehi: /* Installing and Requirements */

2012-08-20T15:14:20Z

Installing and Requirements

← Older revision		Revision as of 15:14, 20 August 2012
Line 21:		Line 21:

	=== Requirements ===		=== Requirements ===
	* The AD plug-in relies on the Epsilon tool suite. ~~Install~~ Epsilon using the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.		* The AD plug-in relies on the Epsilon tool suite. Before installing the AD plug-in, install Epsilon using the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.


			[[Image:Epsilon.jpg\|center]]

	== Creating Flow Diagrams ==		== Creating Flow Diagrams ==

imported>Asiehsalehi: /* Requirements */

2012-08-20T15:11:52Z

Requirements

← Older revision		Revision as of 15:11, 20 August 2012
Line 21:		Line 21:

	=== Requirements ===		=== Requirements ===
	* The AD plug-in relies on the Epsilon tool suite. Install Epsilon using the Epsilon ~~interim~~ update site available at [http://download.eclipse.org~~/modeling/gmt~~/epsilon/~~interim~~/ http://download.eclipse.org~~/modeling/gmt~~/epsilon/~~interim~~/]. Select ''the Epsilon Core (Incubation)'' ~~component, this is the only component that is required for the AD plug-in.~~		* The AD plug-in relies on the Epsilon tool suite. Install Epsilon using the Epsilon update site available at [http://download.eclipse.org/epsilon/updates/ http://download.eclipse.org/epsilon/updates/]. Select and install ''the Epsilon Core (Incubation)'' and ''Human Usable Texual Notation (Incubation)'' components.

	* To create the AD diagrams you need to install [http://wiki.event-b.org/index.php/Rose_(~~Structured~~)~~_Editor Rose Editor]. You can install Rose Editor available at URL: Rodin - [http://rodin-b-sharp.sourceforge.net/updates http://rodin-b-sharp.sourceforge.net/updates] under the ''Editors~~'' ~~category~~.

	== Creating Flow Diagrams ==		== Creating Flow Diagrams ==

imported>Asiehsalehi: /* Transforming to Event-B */

2012-08-09T16:55:54Z

Transforming to Event-B

← Older revision		Revision as of 16:55, 9 August 2012
Line 92:		Line 92:

	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''.		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''.


	[[Image:AD2B.jpg\|center]]		[[Image:AD2B.jpg\|center]]

imported>Asiehsalehi: /* Transforming to Event-B */

2012-08-09T16:55:31Z

Transforming to Event-B

← Older revision		Revision as of 16:55, 9 August 2012
Line 92:		Line 92:

	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''.		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''.

			[[Image:AD2B.jpg\|center]]


	As a result, some read-only event-B elements are generated in order to manage the defined control flow and refinement relationships. User defined event-B elements are allowed; but you can not alter the generated read-only elements.		As a result, some read-only event-B elements are generated in order to manage the defined control flow and refinement relationships. User defined event-B elements are allowed; but you can not alter the generated read-only elements.

imported>Asiehsalehi: /* Leaf Properties */

2012-08-09T16:55:18Z

Leaf Properties

← Older revision		Revision as of 16:55, 9 August 2012
Line 79:		Line 79:

	[[Image:leaf_properties.jpg\|center]]		[[Image:leaf_properties.jpg\|center]]


	=== Constructor Properties ===		=== Constructor Properties ===

imported>Asiehsalehi: /* Elements and Properties */

2012-08-09T16:51:36Z

Elements and Properties

← Older revision		Revision as of 16:51, 9 August 2012
Line 67:		Line 67:

	[[Image:flow_children.jpg\|center]]		[[Image:flow_children.jpg\|center]]


	=== Flow Properties ===		=== Flow Properties ===
Line 78:		Line 79:

	[[Image:leaf_properties.jpg\|center]]		[[Image:leaf_properties.jpg\|center]]


	=== Constructor Properties ===		=== Constructor Properties ===