Decomposition Plug-in User Guide

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

TODO

Setting the Preferences

Decomposition style, decomposition of the contexts, etc.

Reporting a Bug or Requesting a Feature

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

• Bugs
• Feature Requests

Error Messages

The decomposition is forbidden if one of the following conditions applies:

• The built INITIALISATION events of the sub-machines would define an action modifying at the same time a private variable and a shared variable, when performing the shared variables (A-style) decomposition.

Action {0} of the INITIALISATION event modifies a private variable and a shared variable

• The sub-models shall be created in new Event-B projects, but one of the entered project names already exists.

The project {0} should not exist

• The same project name has been entered for two distinct sub-models.

Duplicate sub-model names: {0}

TODO decomposition_error_contextDecompositionKind=Chosen context decomposition kind is not available decomposition_error_duplicateSubModelNames=Duplicate sub-model names: {0} decomposition_error_existingmachine=The machine {0} should not exist decomposition_error_existingcontext=The context {0} should not exist decomposition_error_existingproject=The project {0} should not exist

database_VariableInvalidNatureFailure = Invalid nature value in {0} scuser_VariableHasDisappearedError = Shared variable {0} has disappeared scuser_VariableInvalidNatureError = Inconsistent nature of shared variable {0}, shared expected scuser_EventHasDisappearedError = External event {0} has disappeared scuser_EventInvalidStatusError = Inconsistent status of external event {0}, {1} expected scuser_ParametersInExternalEventError = Parameters cannot be added in external events scuser_GuardsInExternalEventError = Guards cannot be added in external events scuser_ActionsInExternalEventError = Actions cannot be added in external events scuser_ActionOnPrivateAndSharedError = Action {0} of the INITIALISATION event modifies a private variable and a shared variable scuser_ActionOnSharedError = Action {0} of the INITIALISATION event has disappeared

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.

   A solution is to add a theorem based on the missing predicate in the non-decomposed machine. 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.

   Such a situation may be encountered if the "Decompose contexts" option is checked.

   The workaround proposed for the invariants applies to the axioms as well.

   For example, if the non-decomposed context defines the axiom $a \in S$, and this axiom is not copied in a sub-context which contains the $S$ carrier set but does not contain the $a$ constant, then the information $S \neq \emptyset$ is lost. In order to keep it, it is possible to add the theorem $\exists x \qdot x \in S$ in the non-decomposed context.

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 v$ 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: