Decomposition Plug-in User Guide: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Pascal
imported>Pascal
Line 57: Line 57:
:Such a behavior is suitable if you want to prevent this variable from being further refined.
:Such a behavior is suitable if you want to prevent this variable from being further refined.
:A solution for such a variable <math>v</math> of a sub-machine <math>M_i</math> is to add a fake action <math>v \bcmeq </math> in a event of the non-decomposed machine which is associated to the sub-machine <math>M_j</math> (<math>M_i</math> and <math>M_j</math> are distinct sub-machines) when performing the decomposition.
:A solution for such a variable <math>v</math> of a sub-machine <math>M_i</math> is to add a fake action <math>v \bcmeq </math> in a event of the non-decomposed machine which is associated to the sub-machine <math>M_j</math> (<math>M_i</math> and <math>M_j</math> are distinct sub-machines) when performing the decomposition.
:The following example illustrates this.
:In the first example below, the <math>min</math> variable will become ''private'' when performing the decomposition:
 
[[Image:scenario1.png|center|500px|]]
 
:In the second example below, the <math>min</math> variable will become ''shared'' when performing the decomposition:
:In the second scenario, the <math>min</math> variable will become ''shared'' when performing the decomposition.  
[[Image:scenario2.png|center|500px|]]
 
</ol>
</ol>


[[Category:User documentation]]
[[Category:User documentation]]
[[Category:Work in progress]]
[[Category:Work in progress]]

Revision as of 13:01, 3 November 2009

Introduction

The Decomposition plug-in allows to decompose a model into sub-models.

See the Event-B Model Decomposition page for technical details on shared variables (A-style) decomposition.

Installing and Updating

Setup

The following steps will guide you through the setup process:

  1. Download Rodin for your platform from Sourceforge:
  2. Extract the downloaded zip file.
  3. Start Rodin from the folder where you extracted the zip file in the previous step.
  4. Install the Decomposition plug-in:
    1. In the menu choose Help -> Software Updates...
    2. Select the tab Available Software and click Add Site...
    3. Use the location URL: http://rodin-b-sharp.sourceforge.net/updates
    4. Back in Available Software open the update site you just added
    5. Select Event-B Decomposition and click Install...
  5. Restart Rodin as suggested.

Now you are ready to use the Decomposition plug-in.

Update

The following steps will guide you through the update process:

  1. In Rodin open the preferences (Window -> Preferences or for Mac: Rodin -> Preferences)
  2. Find Install/Update -> Automatic Updates
  3. 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.

Release Notes

See the Decomposition plug-in release history.

Decomposing

Selecting the Input Machine

Setting the Preferences

Decomposition style, decomposition of the contexts, etc.

Importing / Exporting the Configuration

Reporting a Bug or Requesting a Feature

Please, use the SourceForge trackers to report a bug on existing features, or to request new features:

Tips and Tricks

Shared variables (A-style) decomposition

  1. An invariant is missing in a sub-machine, but I would like to have it copied.
    For example, an invariant between a concrete variable and some abstract variable may be useful.
    See the last paragraph about the invariants in the Event-B Model Decomposition page.
  2. An axiom is missing in a sub-context, but I would like to have it copied.
  3. A variable is tagged as private in a sub-machine, but I would like to have it tagged shared.
    Such a behavior is suitable if you want to prevent this variable from being further refined.
    A solution for such a variable v of a sub-machine M_i is to add a fake action v \bcmeq in a event of the non-decomposed machine which is associated to the sub-machine M_j (M_i and M_j are distinct sub-machines) when performing the decomposition.
    In the first example below, the min variable will become private when performing the decomposition:
    In the second example below, the min variable will become shared when performing the decomposition:
Retrieved from ‘https://wiki.event-b.org/index.php?title=Decomposition_Plug-in_User_Guide&oldid=3452’