Outstanding Tooling Issues
From Event-B
- As a result of the decomposition process, the tool can produce a remote event, without a corresponding local event. A local event, with no guards and skip action, must be added manually to the tasking machine, and composed machine in order to facilitate code generation. This relates to an implementation with a subroutine call, where there are no parameters passed, and no local updates i.e. remote updates only. The addition of the 'dummy' event will be automated in a pre-processing step in the near future. It is not necessary to have a dummy remote event if a remote event does not exist.
- Flattening of Composition Machines, Machines.
- Addition of Addressed Variables
