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

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Asiehsalehi
 
imported>Tommy
m
 
Line 1: Line 1:
== Introduction ==
+
B2Latex is a plug-in for Rodin that allows you to export Event-B contexts and machines in Latex files that can then be further rendered.
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.
+
Current Version : 0.5.3
  
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.  
+
== Installation/Upgrade ==
 +
The B2latex plugin or "Event-B to Latex exporter" is available from the Main Rodin update site.
 +
Select the main Rodin Update site from the "work with:" field in the Help > Install New Software menu in Rodin.
  
== Installing and Requirements ==
+
== How to use B2Latex? ==
 +
Righ click on a machine or a context directly from the project explorer and select 'Generate Latex Document' command to produce latex documents.
 +
The latex docs are generated in the 'latex' folder in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together
 +
with a style file named ''b2latex.sty''. bsymb.sty and b2latex.sty are required to process the latex.
 +
You can then run Latex on the source files using your own latex installation.
  
=== Setup ===
+
bsymb.sty can be dowloaded from http://www.event-b.org or https://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Event%20B%20LaTeX%20style/1.9/
The following steps will guide you through the setup process:
+
== News? ==
# Start Rodin.
+
The B2Latex 0.5.3 is now available from the Rodin update site. It is compatible with Rodin 2.4 and Rodin 2.5.
# In the menu choose ''Help'' -> ''Install New Software...''.
+
Since B2Latex 0.5.1, the command to export files has been moved to the Event-B project explorer. Users can select
# 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].
+
a machine or a context to produce latex documents directly from
# Select the ''Event-B Atomicity Decomposition'' feature under the ''Modelling Extensions'' category, then click the check box.
+
the project explorer by pressing right click and then select menu 'Generate Latex Document' on the component of their choice.
# Click ''Next'', after some time, the ''Install Details'' page appears.
+
The latex documents are generated in the 'latex' folder like it was done in other previous releases.
# Click ''Next'' and accept the license.
 
# Click ''Finish''.
 
# A ''Security Warning'' window may appear: click ''OK''.
 
# Restart Rodin as suggested.
 
  
=== Requirements ===
+
== Tips ==
* 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.
 
  
* 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.
+
- If you wish to have math formulas or B code in a comment, you need to put them in $..$.
  
== Creating Flow Diagrams ==
+
- The file ''b2latex.sty'' which is generated in the ''latex'' directory can be modified to change the style of the documentation.
  
First you need to open the machine in the Rose editor by right-clicking on the machine.  
+
- To avoid copying ''bsymb.sty'' to every folder where it is used, please follow the procedure below:
 +
  (If you have used MikTex)
 +
  (1) copy the bsmb.sty file into the MikTex directory
 +
      (somewhere like C:\Program Files\MiKTeX 2.7\tex\latex),
 +
  (2) select start -> program -> MikTex 2.x -> setting.
 +
      You will see a dialog box "MikTeX Options".
 +
  (3) Select "General" tab and then click "Refresh FNDB" to update to the miktex database.
 +
 
 +
  This process makes the bsymb.sty can be used everywhere without copying to any folders.
  
[[Image:machine_rose.jpg]]
+
== Old releases ==
 +
B2Latex 0.5.0, is now available from the Rodin update site.
 +
This release is for the Rodin 0.9.2.x or higher.  
  
Then a flow can be created:
+
B2Latex 0.4.1 is required for the Rodin 0.9.1.  
{|
+
If you want to use the Rodin 0.8.x, you need to install the release 0.3.0 instead.
|-
 
|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:
+
''How to use old versions?''
* Create a flow for the most abstract machine.
+
After installation, releases 0.3.x up to 0.5.0, you will see an LX entry in the context menu in the Event-B perspective.
* When refining a machine, the pre-defined flows are copied to the new (refining) machine.
+
Select the Machine or Context you want to translate to Latex and then press the LX button.
* In the new machine, you can create a new flow for each pre-defined leaf.
+
A latex source file will be generated in a folder named ''latex''
 +
in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together
 +
with a style file named ''b2latex.sty''. bsymb.sty and b2latex.sty are required to process the latex.
 +
Run latex on the source files using your own latex installation.  
  
== Elements and Properties ==
+
bsymb.sty can be dowloaded from http://www.event-b.org or http://sourceforge.net/projects/rodin-b-sharp/
  
For each flow, you can define one or more of the below elements, when right-clicking on the flow:
 
* typed parameter
 
* leaf
 
* ''loop'' constructor including one leaf (right-click on the ''loop'')
 
* ''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]]
+
[[Category:User documentation]]
 
+
[[Category:Plugin]]
=== 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 (''loop'', ''and'' / ''or'' / ''xor'' / ''all'' / ''some'' / ''one'').
 
NOTE: The refining property for (''loop'' / ''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''.
 
 
 
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.
 
 
 
== Validation 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)
 
 
 
* Rules on the flow:
 
** Never change the ''copy'' property of a flow. This is an internal property use to make the internal programming decision.
 
** A most abstract flow is a flow with (''sw'' = ''true'') and its children are all non-refining (''ref'' = ''false'').
 
** For each non-abstract flow, EXACTLY one refining child (''ref'' = ''true'') has to be defined.
 
** Each flow inherits its parameter from its parent flow and parent (''all'' / ''some'' / ''one'') constructor (if exists). This has to be done manually. For each new defined flow, copy and paste all necessary parameters from pre-defined parent flow / constructor.
 
** For technical reasons, a ''loop'' constructor never can placed as the first or last child of a flow.
 
 
 
*Rules on the parameter:
 
** The parameter type has to be defined in the context.
 
** The parameter name has to be unique.
 
 
 
* Rules on the constructors:
 
** The refining property for (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') constructors has to be ''false''.
 
** A constructor leaf inherits its refining property from its parent constructor. For example, for a refining ''xor'' (''ref'' = ''true''), all of its leaves' refining property has to be ''true''. Therefore the (''loop'' / ''and'' / ''or'' / ''all'' / ''some'') children refining property is always ''false''.
 

Revision as of 15:52, 23 April 2012

B2Latex is a plug-in for Rodin that allows you to export Event-B contexts and machines in Latex files that can then be further rendered.

Current Version : 0.5.3

Installation/Upgrade

The B2latex plugin or "Event-B to Latex exporter" is available from the Main Rodin update site. Select the main Rodin Update site from the "work with:" field in the Help > Install New Software menu in Rodin.

How to use B2Latex?

Righ click on a machine or a context directly from the project explorer and select 'Generate Latex Document' command to produce latex documents. The latex docs are generated in the 'latex' folder in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together with a style file named b2latex.sty. bsymb.sty and b2latex.sty are required to process the latex. You can then run Latex on the source files using your own latex installation.

bsymb.sty can be dowloaded from http://www.event-b.org or https://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Event%20B%20LaTeX%20style/1.9/

News?

The B2Latex 0.5.3 is now available from the Rodin update site. It is compatible with Rodin 2.4 and Rodin 2.5. Since B2Latex 0.5.1, the command to export files has been moved to the Event-B project explorer. Users can select

a machine or a context to produce latex documents directly from

the project explorer by pressing right click and then select menu 'Generate Latex Document' on the component of their choice.

The latex documents are generated in the 'latex' folder like it was done in other previous releases.

Tips

- If you wish to have math formulas or B code in a comment, you need to put them in $..$.

- The file b2latex.sty which is generated in the latex directory can be modified to change the style of the documentation.

- To avoid copying bsymb.sty to every folder where it is used, please follow the procedure below:

 (If you have used MikTex) 
  (1) copy the bsmb.sty file into the MikTex directory
     (somewhere like C:\Program Files\MiKTeX 2.7\tex\latex),
  (2) select start -> program -> MikTex 2.x -> setting. 
      You will see a dialog box "MikTeX Options".
  (3) Select "General" tab and then click "Refresh FNDB" to update to the miktex database.
  
 This process makes the bsymb.sty can be used everywhere without copying to any folders.

Old releases

B2Latex 0.5.0, is now available from the Rodin update site. This release is for the Rodin 0.9.2.x or higher.

B2Latex 0.4.1 is required for the Rodin 0.9.1. If you want to use the Rodin 0.8.x, you need to install the release 0.3.0 instead.

How to use old versions? After installation, releases 0.3.x up to 0.5.0, you will see an LX entry in the context menu in the Event-B perspective. Select the Machine or Context you want to translate to Latex and then press the LX button. A latex source file will be generated in a folder named latex in your Event-B project directory (i.e. ...\workspaceName\projectName\latex\*.tex) together with a style file named b2latex.sty. bsymb.sty and b2latex.sty are required to process the latex. Run latex on the source files using your own latex installation.

bsymb.sty can be dowloaded from http://www.event-b.org or http://sourceforge.net/projects/rodin-b-sharp/