Difference between pages "Rodin Developer Support" and "State-Machines and Code Generation"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>WikiSysop
 
imported>Andy
 
Line 1: Line 1:
−
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
+
= 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.
  
−
[[Category:Developer Documentation]]
+
Another limitation is that we do not handle nested state-machines, although this should be feasible.
−
[[Category:Rodin Platform]]
 
  
−
== Rodin Platform Overview ==
+
== Translations ==
  
−
== Architecture of the Rodin Platform ==
+
Diagram here
  
−
=== Rodin Platform Core ===
+
Enumeration of states.
  
−
* [[Database]]
+
Initial state
  
−
* [[Builder]]
+
Single outgoing transition
  
−
=== Event-B User Interface ===
+
Multiple Outgoing transitions
  
−
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Editing|editing]] Event-B models or [[Proving|proving]] properties of models.
+
== Tooling ==
  
−
* [[Editing]]
 
  
−
* [[Proving]]
 
  
−
=== Event-B Component Library ===
+
== TODO - list ==
−
 
 
−
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving|proving user interface]]).
 
−
 
 
−
* [[Abstract Syntax Tree]]
 
−
 
 
−
* [[Static Checker]]
 
−
 
 
−
* [[Proof Obligation Generator]]
 
−
 
 
−
* [[Proof Manager]]
 
−
 
 
−
* [[Getting Started]]
 
−
 
 
−
* [[Plug-in Tutorial]]
 
−
 
 
−
== Useful Hints ==
 
−
 
 
−
=== Testing ===
 
−
 
 
−
=== Debugging ===
 
−
 
 
−
== Rodin Developer FAQ ==
 

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Developer_Support&oldid=9468’