State-Machines and Code Generation: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Andy
imported>Andy
Line 10: Line 10:
== Translations ==
== Translations ==


 
<div id="fig:Example State-machine Diagram">
 
<br/>
http://wiki.event-b.org/index.php/Image:StateMachine.png
[[Image:StateMachine.png|center||caption text]]
 
<center>'''Figure 1''': Example State-machine Diagram</center>
 
<br/>
 
</div>


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 (analogous to ''switch'') 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/switch statements in Ada, C and Java.  
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 (analogous to ''switch'') 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/switch statements in Ada, C and Java.  

Revision as of 08:40, 17 May 2012

Generating Code from State-Machine Diagrams

We have introduced the ability to generate code from state-machine diagrams, in version 0.2.3 of the code generation feature plug-in. Implementation 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-machines are created, using the existing state-machine plug-in, subject to the limitations described below.

Limitations

The current code generation tool is restricted to generating code for a single Event-B machine, which may contain 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, or the elements of state-machines, distributed between them.

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

Only the state-machines of tasking/environ machines generate code. State-machines of shared machines do not generate code. This should be explored further during research into decomposition.

Translations


caption text
caption text
Figure 1: Example State-machine Diagram


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 (analogous to switch) 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/switch 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.

We generate a subroutine that controls the state machine, and code, in the task body, to call the subroutines once in every execution cycle. Each state in the state machine is related to a case statement in the subroutine. For instance, the Ada code for the diagram above, is,

case sm_state is
when A then <body> ; sm_state := B;
when B then ... 

The <body> translation is determined by the number of outgoing transitions and the guards and actions of the elaborated events. In the event that a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. In the event that a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable v:INT and events ab and ac defined below,

ab = when v < 10 then <a1> end;
ac = when v >= 10 then <a2> end

Then this is translated to a branching statement, as in this example translation to Ada:

if v < 10 then <a1>
elsif v >= 10 then <a2>
end if;

Tooling