State-Machines and Code Generation
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 >
The translation of the diagrammatic elements to code has been hard-coded in the code generation plug-in. We have introduced new types to the translator's common language model (IL1). We add case-statements and a container for them, since these are commonly used to implement state-machines. The code generator navigates through each state of a state-machine, generating an internal representation of the state-machine which is used to create the IL1 model. The IL1 model is then used to generate code for the various target languages that may have been implemented. We have also updated the IL1-to-target code generators, to generate case statements in Ada, C and Java.
Each state-machine has an Enumerated type whose elements take the names of the states. A state variable is created in the target that keeps track of the current state, and has the type of the enumeration.
In the event that a state has a single outgoing transition,
In the event that a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a case statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Each outgoing transition maps to a case statement guarded by the state variable. In the diagram above, the code is
case sm_state is when A then <body> ; sm_state := B; when ...
So, if the case branch is true then the actions of the branch are performed, and the state variable is updated. Additional guards and actions of <body> are translated from the event associated with the transition.
Initial state
