Outstanding Tooling Issues: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Andy New page: * 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 ... |
imported>Andy |
||
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
==== TODO list: ==== | |||
* 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. | * 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, | * Flattening of Composition Machines, and Machines at the Implementation level, composed machine refinement. | ||
* Addition of Addressed Variables | * Addition of Addressed Variables | ||
Latest revision as of 08:56, 29 November 2011
TODO list:
- 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, and Machines at the Implementation level, composed machine refinement.
- Addition of Addressed Variables
