Decomposition Plug-in User Guide: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Pascal
imported>Asiehsalehi
 
(98 intermediate revisions by 4 users not shown)
Line 7: Line 7:


== Installing and Updating ==
== Installing and Updating ==
{{TODO | Not yet released, waiting for Rodin 1.2}}
=== 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]:
# Download Rodin for your platform from [http://sourceforge.net/project/showfiles.php?group_id=108850&package_id=181714&release_id=687381 Sourceforge].
# Extract the downloaded zip file.
# Extract the downloaded zip file.
# Start Rodin from the folder where you extracted the zip file in the previous step.
# Start Rodin from the folder where you extracted the zip file in the previous step.
# Install the Decomposition plug-in:
# Install the Decomposition plug-in:
## In the menu choose ''Help'' -> ''Software Updates...''
## In the menu choose ''Help'' -> ''Install New Software...''
## Select the tab ''Available Software'' and click ''Add Site...''
## 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]
## Use the location URL: <tt>http://rodin-b-sharp.sourceforge.net/updates</tt>
## Select the ''Model Decomposition'' feature under the ''Composition and Decomposition'' category, then click the check box
## Back in ''Available Software'' open the update site you just added
## Click ''Next'', after some time, the ''Install Details'' page appears
## Select ''Event-B Decomposition'' and click ''Install...''
## Click ''Next'' and accept the license
## Click ''Finish''
## A ''Security Warning'' window may appear: click ''OK''
# Restart Rodin as suggested.
# Restart Rodin as suggested.


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


=== Update ===
=== Update ===
Line 35: Line 36:


== Decomposing ==
== Decomposing ==
{{TODO}}
=== Running the Decompose Action ===
=== Selecting the Input Machine ===
The <tt>Decompose</tt> action launches the decomposition wizard, which will perform the decomposition according to the preferences. It is available:
{|
|-
|1. Either from the toolbar of the Event-B explorer.
|2. Or from the contextual menu, when right-clicking on a machine.
|-
| valign="top" | [[Image:decompose_explorer.png|center]]
| valign="top" | [[Image:decompose_contextual.png|center]]
|}
 
=== Setting the Preferences ===
=== Setting the Preferences ===
Decomposition style, decomposition of the contexts, etc.
The different decomposition options are described below:
* Decomposition style. The shared variables (A-style) or shared events (B-style) decomposition will be performed, according to the specified decomposition style.
* Create new projects for sub-components. If checked, the decomposed sub-models are created in new projects.
* Context decomposition. The contexts seen by the input machine are decomposed if and only if this option is checked; otherwise, they are copied from the initial model to the decomposed sub-models.
 
[[Image:decompose_options.png]]
 
=== Selecting the Input Machine and Partitioning the Elements ===
The following information has to be provided in the wizard dialog:
* Which machine will be decomposed.
* Which sub-machines will be generated.
* How the elements, and more precisely the events for shared variables (A-style) decomposition and the variables for shared events (B-style) decomposition, are partioned among these sub-machines.
 
[[Image:decompose_partition.png]]
 
=== Importing / Exporting the Configuration ===
=== Importing / Exporting the Configuration ===
It is possible on the one hand to export a configuration to a file, and on the other hand to import a configuration from a file.
Thus, similarly to what it is possible to do with the decomposition wizard, the configuration file allows to replay the decomposition by persistently storing the decomposition settings.
{| class="wikitable"
| [[Image:Save_decomposition_file.png|thumb|left|450x400px|The decomposition file is created from the wizard using the 'save button']]
| [[Image:Decomp file pretty print.png|thumb|center|550x450px|Pretty print view of the configuration file]]
|}
When saving the decomposition file, static checks are run according to the style of decomposition chosen (shared variable or shared event). If an error occurs during the static check, it is displayed in the Rodin Problems view. Only after all the decomposition errors are fixed, the decomposition operation can be run. That is achieved by clicking on the brown button on the menu bar (on top) or by right-clicking in the mouse and selecting the option "Decompose Now":
[[Image:decomposition_file_button.png|center|500x450px]]
In case an error occurs during the decomposition, a message is displayed and the user is asked to delete the possible created files. The error will be displayed in the 'Rodin Problems' view (usually located at the bottom of the screen).
[[Image:decomposition_file_error.png|center|550x500px]]
==='''NOTE: Re-running the decomposition operation will override all the existing generated components without asking any confirmation. This includes all the sub-components machines, contexts, composed machines and even projects (from version 1.2.3 onwards).'''===
=== Shared Event Composition ===
If you have the  [http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B shared event composition plug-in] installed, after the decomposition has been applied (via wizard of via configuration file), a composition file is automatically created, expressing how the events of the original model where split. '''Note''' that currently this only works for a '''shared event decomposition'''.
{| class="wikitable"
| [[Image:decomposition_before.png|frame|left|200x250px|text|Before the decomposition]]
| [[Image:Decomp file pretty print.png|thumb|center|550x450px|Configuration file]]
| [[Image:decomposition_after_1.png|frame|center|baseline|170x250px|text|After the decomposition]]
| [[Image:decomposition_after_2.png|thumb|right|470x550px| alt=alt text|Composition file automatically generated after the decomposition has been applied]]
|}


== Reporting a Bug or Requesting a Feature ==
== Reporting a Bug or Requesting a Feature ==
Line 48: Line 101:
== Error Messages ==
== Error Messages ==
=== When running the decomposition ===
=== When running the decomposition ===
The decomposition is forbidden, and an error message is displayed, if one of the following conditions applies:
The decomposition is forbidden and an error message is displayed, 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.
 
:<tt>Action {0} of the INITIALISATION event modifies a private variable and a shared variable</tt>
*The built INITIALISATION events of the sub-machines would define an action modifying at the same time a ''private'' variable and a ''shared'' variable.<br/><tt>Action {0} of the INITIALISATION event modifies a private variable and a shared variable</tt><br/>
:See [http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_a_shared_variable_is_not_refined_by_an_initialization_event Ensuring that a shared variable is not refined by an initialization event] for further explanations.
See [http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_a_shared_variable_is_not_refined_by_an_initialization_event Ensuring that a shared variable is not refined by an initialization event] for further explanations.
* The sub-models shall be created in new Event-B projects, but one of the entered project names already exists.
 
:<tt>The project {0} should not exist</tt>
*The sub-models shall be created in new Event-B projects, but one of the entered project names already exists.<br/><tt>The project {0} should not exist</tt>
* The same project name has been entered for two distinct sub-models.
:<tt>Duplicate sub-model names: {0}</tt>


=== When running the static checker ===
*The same project name has been entered for two distinct sub-models.<br/><tt>Duplicate sub-model names: {0}</tt>
The following rules are enforced by the static checker, and errors are returned (in the Rodin Problems view) accordingly:
 
* A ''shared'' variable shall be present in subsequent refinements.
*For the shared event decomposition, the predicates (invariants, guards) and assignments (actions) must not refer to elements that belong to different sub-components. If we create sub-component C1 with element el1 and sub-component C2 with element el2 from the non-decomposed component C, then a predicate P(el1, el2) (like el1=el2) in C would generate this error while decomposing. The predicate/assignment is too complex since refers to elements that belong to different sub-components. So solve this issue, the user must explicitly separate the elements (by a further refinement or introducing an auxiliary parameter p representing the value of a variable: el1=el2 <=> p=el2 /\ el1 = p). <br/><tt>Action/Guard {0} in event {1}.{2} is too complex to be decomposed (includes variables that do not belong to this sub-component):\n\nAvailable variables/parameters: {3}\n\nAvailable carrier sets/constants: {4}\n\nAction: {5}\n\nPlease simplify/separate variables before decomposing.</tt>
:<tt>Shared variable {0} has disappeared</tt>
 
* A ''shared'' variable shall still have the ''shared'' attribute in subsequent refinements.
* When decomposing, all the events (shared variable approach) or all the variables (shared event approach) must be selected and allocated to the sub-components in order for the decomposition to run. If there are events/variables unselected, an error of this kind occurs:<br/> <tt>All the {events/variables} in {MachineName} must be used as (subComponent) elements before decomposing.</tt><br/>To fix this error, the user must allocate the unselected variables/events to any of the sub-components.
:<tt>Inconsistent nature of shared variable {0}, shared expected</tt>
 
* An ''external'' event shall be present in subsequent refinements.
* When a static check error exists in the decomposition file, the decomposition button will not work and the decomposition will not be run.
:<tt>External event {0} has disappeared</tt>
 
* An ''external'' event shall still have the ''external'' attribute in subsequent refinements.
* If an error occurs when running the decomposition, the user will be asked to delete the partial created sub-components.
:<tt>Inconsistent status of external event {0}, external expected</tt>
 
* An ''external'' event shall have the ''extended'' attribute in subsequent refinements.
=== When running the static checker... ===
:<tt>Inconsistent status of external event {0}, extended expected</tt>
==== ... on a machine file ====
* An ''external'' event shall not declare any additional parameter in subsequent refinements.
The following rules are enforced on the machine files by the static checker, and errors are returned (in the Rodin Problems view) accordingly:
:<tt>Parameters cannot be added in external events</tt>
*A ''shared'' variable shall be present in subsequent refinements.<br/><tt>Shared variable {0} has disappeared</tt>
* An ''external'' event shall not declare any additional guard in subsequent refinements.
*A ''shared'' variable shall still have the ''shared'' attribute in subsequent refinements.<br/><tt>Inconsistent nature of shared variable {0}, shared expected</tt>
:<tt>Guards cannot be added in external events</tt>
*An ''external'' event shall be present in subsequent refinements.<br/><tt>External event {0} has disappeared</tt>
* An ''external'' event shall not declare any additional action in subsequent refinements.
*An ''external'' event shall still have the ''external'' attribute in subsequent refinements.<br/><tt>Inconsistent status of external event {0}, external expected</tt>
:<tt>Actions cannot be added in external events</tt>
*An ''external'' event shall have the ''extended'' attribute in subsequent refinements.<br/><tt>Inconsistent status of external event {0}, extended expected</tt>
* An INITIALISATION event shall not contain an action modifying at the same time a ''private'' variable and a ''shared'' variable.
*An ''external'' event shall not declare any additional parameter in subsequent refinements.<br/><tt>Parameters cannot be added in external events</tt>
:<tt>Action {0} of the INITIALISATION event modifies a private variable and a shared variable</tt>
*An ''external'' event shall not declare any additional guard in subsequent refinements.<br/><tt>Guards cannot be added in external events</tt>
* The actions of an INITIALISATION event modifying a ''shared'' variable shall be present and be syntactically equal in subsequent refinements.
*An ''external'' event shall not declare any additional action in subsequent refinements.<br/><tt>Actions cannot be added in external events</tt>
:<tt>Action {0} of the INITIALISATION event has disappeared</tt>
*An INITIALISATION event shall not contain an action modifying at the same time a ''private'' variable and a ''shared'' variable.<br/><tt>Action {0} of the INITIALISATION event modifies a private variable and a shared variable</tt>
*The actions of an INITIALISATION event modifying a ''shared'' variable shall be present and be syntactically equal in subsequent refinements.<br/><tt>Action {0} of the INITIALISATION event has disappeared</tt>


For additional information, see:
For additional information, see:
* [http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_a_shared_variable_is_not_refined Ensuring that a shared variable is not refined].
*[http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_a_shared_variable_is_not_refined Ensuring that a shared variable is not refined].
* [http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_an_external_event_is_not_refined Ensuring that an external event is not refined].
*[http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_an_external_event_is_not_refined Ensuring that an external event is not refined].
* [http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_a_shared_variable_is_not_refined_by_an_initialization_event Ensuring that a shared variable is not refined by an initialization event].
*[http://wiki.event-b.org/index.php/Event_Model_Decomposition#Ensuring_that_a_shared_variable_is_not_refined_by_an_initialization_event Ensuring that a shared variable is not refined by an initialization event].
 
==== ... on a configuration file ====
*In the configuration file, it is required only one component machine.<br/> <tt>Only one component machine may be decomposed</tt> <br/> <tt>Missing component name</tt> <br/> <tt>Component machine {0} not found</tt>
*In the configuration file, it is required only one section.<br/> <tt>Component machine {0} does not have a configuration</tt> or <tt>Only one configuration is allowed per decomposition file</tt>
** It is required to select the style between ''shared event'' or ''shared variable''.<br/> <tt>Missing 'Style' definition</tt> <br/> <tt>Style {0} not recognised</tt>
** It is required to select how to decompose the context  between ''no decomposition'' or ''minimal decomposition''.<br/> <tt>Missing 'Decomposition Context' definition</tt> <br/> <tt>Kind of decomposition context {0} not recognised</tt>
** It is required to select how to decompose between ''New Project'' or ''Same Project''.<br/> <tt>Missing 'New Project/Same Project Decomposition' definition</tt>
*In the decomposition file, the subComponents must exist and have different labels.<br/> <tt>SubComponents not found</tt> and <tt>Ambiguous subComponent label {0}</tt>
** All the subComponent elements derived from the component machine (variables or events) must be used before decomposing.<br/> <tt>All the {0} in {1} must be used as (subComponent) elements before decomposing</tt>
** Each subComponent must have at least one subComponent element.<br/> <tt>SubComponent Elements not found for subComponent {0}</tt>
** Depending on the select style of decomposition, the subComponent elements must exist and either variables or events.<br/><tt>Invalid subComponent element</tt> <br/> <tt>{0} does not have expected type [shared variable:events; shared event:variables] or does not exist in component {1}</tt>


== Tips and Tricks ==
== Tips and Tricks ==
=== ''Shared variables'' (A-style) decomposition ===
=== ''Shared variables'' (A-style) decomposition ===
<ol>
*'''An invariant is missing in a sub-machine, but I would like to have it copied.'''<br/>For example, an invariant between a concrete variable and some abstract variable may be useful.<br/>A solution is to add a theorem based on the missing predicate in the non-decomposed machine. See the last paragraph [[Event_Model_Decomposition#inv_distribution | about the invariants]] in the Event-B Model Decomposition page.
<li> '''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.
*'''An axiom is missing in a sub-context, but I would like to have it copied.'''<br/>Such a situation may be encountered if the "Decompose contexts" option is checked.<br/>The workaround proposed for the invariants applies to the axioms as well.<br/>For example, if the non-decomposed context defines the axiom <math>a \in S</math>, and this axiom is not copied in a sub-context which contains the <math>S</math> carrier set but does not contain the <math>a</math> constant, then the information <math>S \neq \emptyset</math> is lost. In order to keep it, it is possible to add the theorem <math>\exists x \qdot x \in S</math> in the non-decomposed context.
:A solution is to add a theorem based on the missing predicate in the non-decomposed machine. See the last paragraph [[Event_Model_Decomposition#inv_distribution | about the invariants]] in the Event-B Model Decomposition page.
 
*'''A variable is tagged as ''private'' in a sub-machine, but I would like to have it tagged ''shared''.'''<br/>Such a behavior is suitable if you want to prevent this variable from being further refined.<br/>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 v</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.<br/>In the first example below, the <math>min</math> variable will become ''private'' when performing the decomposition:[[Image:scenario1.png|center|500px|]]<br/>In the second example below, the <math>min</math> variable will become ''shared'' when performing the decomposition:[[Image:scenario2.png|center|500px|]]
 
=== ''Shared event'' (B-style) decomposition ===
*'''When decomposing I am getting an error  saying that the non-decomposed machine has complex actions/guards''' <br/> This usually means that a predicate/assignment is too complex to be decomposed automatically. If a predicate/assignment refers to variables that belong to different sub-components, that predicate/assignment cannot be decomposed automatically: the user must explicitly make the separation of the variables in the predicate/assignment. A solution can be add an additional parameter representing the value of the used variable. Consider <math>v1</math> a variable that is a sub-set of carrier set <math>S</math> (<math>v1 \subseteq S</math>) and <math>v2</math> that is an element of <math>S</math> (<math>v2 \in S</math>).  The predicate <math>v1 = S \backslash \{v2\} </math> cannot  be decomposed automatically if  <math>v1</math> and <math>v2</math> belong to different sub-components. A possible solution is to add a parameter <math>p</math>: <math>p = v2 \wedge v1 = S \backslash \{p\}</math>.
 
*'''Shared Event Composition''' <br/> The [[Parallel_Composition_using_Event-B#Shared_Event_Composition_Plug-in | shared event composition]] plug-in can be used to see how the shared events are composed if this plug-in installed. Also it allows the generation of a composed machine that is a refinement of the non-decomposed machine. Below it is an example of just case: Machine '''cm11''' was decomposed as seen in the decomposition file '''decompFile_cm11'''. And the shared events can be seen in shared event composition file '''cm11_cmp''':<br/> <br/>


<li>'''An axiom is missing in a sub-context, but I would like to have it copied.'''
[[Image:machine_cm11.png|left|150px]] <br/>
:Such a situation may be encountered if the "Decompose contexts" option is checked.
[[Image:decompFile_cm11.png|center|190px]] <br/> <br/>
:The workaround proposed for the invariants applies to the axioms as well.
[[Image:compFile_cm11_cmp.png|center|480px]] <br/>
:For example, if the non-decomposed context defines the axiom <math>a \in S</math>, and this axiom is not copied in a sub-context which contains the <math>S</math> carrier set but does not contain the <math>a</math> constant, then the information <math>S \neq \emptyset</math> is lost. In order to keep it, it is possible to add the theorem <math>\exists x \qdot x \in S</math> in the non-decomposed context.


<li> '''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 <math>v</math> of a sub-machine <math>M_i</math> is to add a fake action <math>v \bcmeq v</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.
: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:
[[Image:scenario2.png|center|500px|]]
</ol>


[[Category:User documentation]]
[[Category:User documentation]]
[[Category:Work in progress]]
[[Category:Composition]]
[[Category:Plugin]]
[[Category:Design]]

Latest revision as of 15:25, 4 July 2013

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 -> Install New Software...
    2. In the Work with dropdown list, choose the location URL: Rodin - http://rodin-b-sharp.sourceforge.net/updates
    3. Select the Model Decomposition feature under the Composition and Decomposition category, then click the check box
    4. Click Next, after some time, the Install Details page appears
    5. Click Next and accept the license
    6. Click Finish
    7. A Security Warning window may appear: click OK
  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 Release History.

Decomposing

Running the Decompose Action

The Decompose action launches the decomposition wizard, which will perform the decomposition according to the preferences. It is available:

1. Either from the toolbar of the Event-B explorer. 2. Or from the contextual menu, when right-clicking on a machine.

Setting the Preferences

The different decomposition options are described below:

  • Decomposition style. The shared variables (A-style) or shared events (B-style) decomposition will be performed, according to the specified decomposition style.
  • Create new projects for sub-components. If checked, the decomposed sub-models are created in new projects.
  • Context decomposition. The contexts seen by the input machine are decomposed if and only if this option is checked; otherwise, they are copied from the initial model to the decomposed sub-models.

Selecting the Input Machine and Partitioning the Elements

The following information has to be provided in the wizard dialog:

  • Which machine will be decomposed.
  • Which sub-machines will be generated.
  • How the elements, and more precisely the events for shared variables (A-style) decomposition and the variables for shared events (B-style) decomposition, are partioned among these sub-machines.

Importing / Exporting the Configuration

It is possible on the one hand to export a configuration to a file, and on the other hand to import a configuration from a file.

Thus, similarly to what it is possible to do with the decomposition wizard, the configuration file allows to replay the decomposition by persistently storing the decomposition settings.

The decomposition file is created from the wizard using the 'save button'
Pretty print view of the configuration file

When saving the decomposition file, static checks are run according to the style of decomposition chosen (shared variable or shared event). If an error occurs during the static check, it is displayed in the Rodin Problems view. Only after all the decomposition errors are fixed, the decomposition operation can be run. That is achieved by clicking on the brown button on the menu bar (on top) or by right-clicking in the mouse and selecting the option "Decompose Now":

In case an error occurs during the decomposition, a message is displayed and the user is asked to delete the possible created files. The error will be displayed in the 'Rodin Problems' view (usually located at the bottom of the screen).

NOTE: Re-running the decomposition operation will override all the existing generated components without asking any confirmation. This includes all the sub-components machines, contexts, composed machines and even projects (from version 1.2.3 onwards).

Shared Event Composition

If you have the shared event composition plug-in installed, after the decomposition has been applied (via wizard of via configuration file), a composition file is automatically created, expressing how the events of the original model where split. Note that currently this only works for a shared event decomposition.

Before the decomposition
Configuration file
After the decomposition
alt text
Composition file automatically generated after the decomposition has been applied

Reporting a Bug or Requesting a Feature

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

Error Messages

When running the decomposition

The decomposition is forbidden and an error message is displayed, 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.
    Action {0} of the INITIALISATION event modifies a private variable and a shared variable

See Ensuring that a shared variable is not refined by an initialization event for further explanations.

  • 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}
  • For the shared event decomposition, the predicates (invariants, guards) and assignments (actions) must not refer to elements that belong to different sub-components. If we create sub-component C1 with element el1 and sub-component C2 with element el2 from the non-decomposed component C, then a predicate P(el1, el2) (like el1=el2) in C would generate this error while decomposing. The predicate/assignment is too complex since refers to elements that belong to different sub-components. So solve this issue, the user must explicitly separate the elements (by a further refinement or introducing an auxiliary parameter p representing the value of a variable: el1=el2 <=> p=el2 /\ el1 = p).
    Action/Guard {0} in event {1}.{2} is too complex to be decomposed (includes variables that do not belong to this sub-component):\n\nAvailable variables/parameters: {3}\n\nAvailable carrier sets/constants: {4}\n\nAction: {5}\n\nPlease simplify/separate variables before decomposing.
  • When decomposing, all the events (shared variable approach) or all the variables (shared event approach) must be selected and allocated to the sub-components in order for the decomposition to run. If there are events/variables unselected, an error of this kind occurs:
    All the {events/variables} in {MachineName} must be used as (subComponent) elements before decomposing.
    To fix this error, the user must allocate the unselected variables/events to any of the sub-components.
  • When a static check error exists in the decomposition file, the decomposition button will not work and the decomposition will not be run.
  • If an error occurs when running the decomposition, the user will be asked to delete the partial created sub-components.

When running the static checker...

... on a machine file

The following rules are enforced on the machine files by the static checker, and errors are returned (in the Rodin Problems view) accordingly:

  • A shared variable shall be present in subsequent refinements.
    Shared variable {0} has disappeared
  • A shared variable shall still have the shared attribute in subsequent refinements.
    Inconsistent nature of shared variable {0}, shared expected
  • An external event shall be present in subsequent refinements.
    External event {0} has disappeared
  • An external event shall still have the external attribute in subsequent refinements.
    Inconsistent status of external event {0}, external expected
  • An external event shall have the extended attribute in subsequent refinements.
    Inconsistent status of external event {0}, extended expected
  • An external event shall not declare any additional parameter in subsequent refinements.
    Parameters cannot be added in external events
  • An external event shall not declare any additional guard in subsequent refinements.
    Guards cannot be added in external events
  • An external event shall not declare any additional action in subsequent refinements.
    Actions cannot be added in external events
  • An INITIALISATION event shall not contain an action modifying at the same time a private variable and a shared variable.
    Action {0} of the INITIALISATION event modifies a private variable and a shared variable
  • The actions of an INITIALISATION event modifying a shared variable shall be present and be syntactically equal in subsequent refinements.
    Action {0} of the INITIALISATION event has disappeared

For additional information, see:

... on a configuration file

  • In the configuration file, it is required only one component machine.
    Only one component machine may be decomposed
    Missing component name
    Component machine {0} not found
  • In the configuration file, it is required only one section.
    Component machine {0} does not have a configuration or Only one configuration is allowed per decomposition file
    • It is required to select the style between shared event or shared variable.
      Missing 'Style' definition
      Style {0} not recognised
    • It is required to select how to decompose the context between no decomposition or minimal decomposition.
      Missing 'Decomposition Context' definition
      Kind of decomposition context {0} not recognised
    • It is required to select how to decompose between New Project or Same Project.
      Missing 'New Project/Same Project Decomposition' definition
  • In the decomposition file, the subComponents must exist and have different labels.
    SubComponents not found and Ambiguous subComponent label {0}
    • All the subComponent elements derived from the component machine (variables or events) must be used before decomposing.
      All the {0} in {1} must be used as (subComponent) elements before decomposing
    • Each subComponent must have at least one subComponent element.
      SubComponent Elements not found for subComponent {0}
    • Depending on the select style of decomposition, the subComponent elements must exist and either variables or events.
      Invalid subComponent element
      {0} does not have expected type [shared variable:events; shared event:variables] or does not exist in component {1}

Tips and Tricks

Shared variables (A-style) decomposition

  • 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.
  • 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.
  • 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:

Shared event (B-style) decomposition

  • When decomposing I am getting an error saying that the non-decomposed machine has complex actions/guards
    This usually means that a predicate/assignment is too complex to be decomposed automatically. If a predicate/assignment refers to variables that belong to different sub-components, that predicate/assignment cannot be decomposed automatically: the user must explicitly make the separation of the variables in the predicate/assignment. A solution can be add an additional parameter representing the value of the used variable. Consider v1 a variable that is a sub-set of carrier set S (v1 \subseteq S) and v2 that is an element of S (v2 \in S). The predicate v1 = S \backslash \{v2\} cannot be decomposed automatically if v1 and v2 belong to different sub-components. A possible solution is to add a parameter p: p = v2 \wedge v1 = S \backslash \{p\}.
  • Shared Event Composition
    The shared event composition plug-in can be used to see how the shared events are composed if this plug-in installed. Also it allows the generation of a composed machine that is a refinement of the non-decomposed machine. Below it is an example of just case: Machine cm11 was decomposed as seen in the decomposition file decompFile_cm11. And the shared events can be seen in shared event composition file cm11_cmp: