imported>Pascal |
|
| Line 1: |
Line 1: |
| − | {{TOCright}}
| |
| | | | |
| − | == Introduction ==
| |
| − | The Decomposition plug-in allows to decompose a model into sub-models.
| |
| − |
| |
| − | See the [http://wiki.event-b.org/index.php/Event_Model_Decomposition 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:
| |
| − | # 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.
| |
| − | # Start Rodin from the folder where you extracted the zip file in the previous step.
| |
| − | # Install the Decomposition plug-in:
| |
| − | ## In the menu choose ''Help'' -> ''Software Updates...''
| |
| − | ## Select the tab ''Available Software'' and click ''Add Site...''
| |
| − | ## Use the location URL: <tt>http://rodin-b-sharp.sourceforge.net/updates</tt>
| |
| − | ## Back in ''Available Software'' open the update site you just added
| |
| − | ## Select ''Event-B Decomposition'' and click ''Install...''
| |
| − | # 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:
| |
| − | # In Rodin open the preferences (''Window'' -> ''Preferences'' or for Mac: ''Rodin'' -> ''Preferences'')
| |
| − | # Find ''Install/Update'' -> ''Automatic Updates''
| |
| − | # 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 [http://wiki.event-b.org/index.php/Decomposition_Release_History Decomposition plug-in release history].
| |
| − |
| |
| − | == Decomposing ==
| |
| − | {{TODO}}
| |
| − | === 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:
| |
| − | * [https://sourceforge.net/tracker/?atid=651669&group_id=108850&category=1259297 Bugs]
| |
| − | * [https://sourceforge.net/tracker/?atid=651672&group_id=108850&category=1259298 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 ===
| |
| − | <ol>
| |
| − | <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.
| |
| − | :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 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 <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:Work in progress]]
| |
