Revision as of 10:50, 4 July 2013

Version 1.0

Implemented a workaround to take contributed elements (records, …) into account. Works properly when NOT decomposing contexts.

Updated for Rodin 1.3.x.
Includes a decomposition file where the decomposition settings can be saved for future reuse. Decomposition file is created from the wizard ('save as' button).
When decomposing using the shared event style, a shared event composition machine is created which allows the reassembly of the sub-components (to validate the decomposition).
Removes the 'theorem' tag from the typing guards.

Updated for Rodin 2.2.x.
Feature request: removed parameters that are not used in any of the guards or actions of a decomposed event

User's inputs and request were taken into account. In particular in terms of better usability of the tool. We addressed this topic by:

Typing guards (automatically generated) are marked as theorems
Static checks were added to the decomposition file according to the decomposition style chosen.
Improved UI interface: removed dialog requesting confirmation to delete possible existing sub-components (generated sub-components are marked as read-only)
Changed suffix of decomposition file to "_DCMP"
Fixed small bugs

Release compatible with version 2.6.x of the platform.

Bug fixes
- Decomposition wizard problem for large number of variables/events (were not displayed in full)
- Fixed small bugs

Release compatible with version 2.7.x of the platform.

Release compatible with version 2.7.x and 2.8.x of the platform.

Re-running a decomposition configuration (configured for "New Project" containing sub-models) will keep the Event-B components have been built in the new projects containing sub-models; just the sub-models' Event-B components are replaced by the new ones.

TODO: List here the new features and improvements.

@@ Line 47: / Line 47: @@
 = Version 1.2.6 =
-Release compatible with version 2.7.x of the platform.
+Release compatible with version 2.7.x and 2.8.x of the platform.
 * Re-running a decomposition configuration (configured for "New Project" containing sub-models) will keep the Event-B components have been built in the new projects containing sub-models; just the sub-models' Event-B components are replaced by the new ones.