Outstanding Tooling Issues

From Event-B
Revision as of 16:26, 28 November 2011 by 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 ...)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search
  • 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