State-Machines and Code Generation: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Andy
mNo edit summary
imported>Andy
Line 2: Line 2:
We introduce the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machine(s) are created in a machine using the existing state-machine plug-in, subject to the limitations described below.  
We introduce the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machine(s) are created in a machine using the existing state-machine plug-in, subject to the limitations described below.  
== Limitations/What Can Be Translated ==
== Limitations/What Can Be Translated ==
The current code generation tool is restricted to generating code for a single Event-B machine containing one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines.
The current code generation tool is restricted to generating code for a single Event-B machine containing one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines distributed between them.


We do not handle nested state-machines.
Another limitation is that we do not handle nested state-machines, although this should be feasible.


== Translations ==
== Translations ==

Revision as of 07:10, 16 May 2012

Generating Code from State-Machine Diagrams

We introduce the ability to generate code from state-machine diagrams in version 0.2.3 of the code generation feature plug-in. Code is generated from the diagram itself, and no additional mark-up of the model is required; that is, nothing over and above the usual mark-up required for Tasking Event-B, such as identifying non-typing/typing invariants, and guards etc. State-machine(s) are created in a machine using the existing state-machine plug-in, subject to the limitations described below.

Limitations/What Can Be Translated

The current code generation tool is restricted to generating code for a single Event-B machine containing one or more state-machines. We have yet to explore the decomposition/composition of machines containing state-machines. In principal we should be able to apply decomposition techniques to decompose the single Event-B machine with state-machines into a number of machines, with the state-machines distributed between them.

Another limitation is that we do not handle nested state-machines, although this should be feasible.

Translations

Diagram here

Enumeration of states.

Initial state

Single outgoing transition

Multiple Outgoing transitions

Tooling

TODO - list