D45 Code Generation - Revision history

imported>Tommy: /* Available Documentation */

2012-04-20T08:31:32Z

Available Documentation

← Older revision		Revision as of 08:31, 20 April 2012
Line 46:		Line 46:

	= Available Documentation =		= Available Documentation =
	We have updated the documentation, including the Tasking Event-B Overview, and Tutorial materials.		We have updated the documentation<ref>http://wiki.event-b.org/index.php/Code_Generation_Activity</ref>, including the Tasking Event-B Overview<ref>http://wiki.event-b.org/index.php/Tasking_Event-B_Overview</ref>, and Tutorial <ref>http://wiki.event-b.org/index.php/Code_Generation_Tutorial</ref> materials.
	~~[[TODO]] ''complete''~~

	= Status =		= Status =

imported>Andy: /* Using Abstract Translators */

2012-04-20T07:54:43Z

Using Abstract Translators

← Older revision		Revision as of 07:54, 20 April 2012
Line 43:		Line 43:
	== Using Abstract Translators ==		== Using Abstract Translators ==
	To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators.		To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators.
	Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP<ref>http://openmp.org/wp/</ref>		Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP<ref>http://openmp.org/wp/</ref> or Pthreads<ref>https://computing.llnl.gov/tutorials/pthreads/</ref>. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.
	or Pthreads<ref>https://computing.llnl.gov/tutorials/pthreads/</ref>. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.

	= Available Documentation =		= Available Documentation =

imported>Andy: /* Using Abstract Translators */

2012-04-20T07:54:16Z

Using Abstract Translators

← Older revision		Revision as of 07:54, 20 April 2012
Line 43:		Line 43:
	== Using Abstract Translators ==		== Using Abstract Translators ==
	To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators.		To test our approach, we have built translators for C, Ada and Java using the same underlying abstract translators.
	Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP or Pthreads. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.		Additionally we consider the case where a new language may be required that has only modest differences to an existing language. A good example of this is to consider the case where a different library may want to be used from one used in an existing translation. For instance in C, concurrency can be achieved through different mechanisms such as OpenMP<ref>http://openmp.org/wp/</ref>
			or Pthreads<ref>https://computing.llnl.gov/tutorials/pthreads/</ref>. In this case it may be that all but the mechanism for handling a subroutine call are the same, meaning that the majority of the translation can occur using common translators, with separate translators for the different methods of handling a subroutine call. To allow for this we allow the developer to assign a core and specialisation language to each translator they build. In cases where a translator for the specialisation language does not exist, the translator will automatically defer to the default core language translator, if one exists. This means that default translators for a particular core language can be written for the majority of the translation, with specialisations being provided where differences occur. The core and specialisation of the language is also reflected in the theory translator, meaning that language theories are only required for the core languages, rather than for each individual specialization.

	= Available Documentation =		= Available Documentation =

imported>Andy: /* Tasking Event-B and its edition */

2012-04-20T07:48:58Z

Tasking Event-B and its edition

← Older revision		Revision as of 07:48, 20 April 2012
Line 27:		Line 27:
	== Tasking Event-B and its edition ==		== Tasking Event-B and its edition ==
	A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component		A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component
	<ref name="~~aag~~">http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B</ref>. Composed machines are used to store event 'synchronizations', and are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events. The new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.		<ref name="aah">http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B</ref>. Composed machines are used to store event 'synchronizations', and are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events. The new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.

	== Allowing Extensibility ==		== Allowing Extensibility ==

imported>Andy: /* Tasking Event-B and its edition */

2012-04-20T07:48:01Z

Tasking Event-B and its edition

← Older revision		Revision as of 07:48, 20 April 2012
Line 26:		Line 26:

	== Tasking Event-B and its edition ==		== Tasking Event-B and its edition ==
	A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component. Composed machines are used to store event 'synchronizations', and are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events. The new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.		A text-based task body editor was added, to minimize the amount of editing required with the EMF tree editor. The task body editor is associated with a parser-builder; after the text is entered in the editor the EMF representation is generated (by clicking a button) that is, assuming parsing is successful. If the parser detects an error, information about the parse error is displayed in an adjoining text box. When specifying events in the task body, there is no longer a need to specify two events involved in a synchronization. The code generator automatically finds the corresponding event of a synchronization, based on the event name, and using the composed machine component
			<ref name="aag">http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B</ref>. Composed machines are used to store event 'synchronizations', and are generated automatically during the decomposition process. This reduces the amount of typing in the TaskBody editor, since we no longer need to specify both local and remote (synchronizing) events. The new feature also overcomes the 'problem' that we previously experienced, with duplicate event names in a development, and event selection, when specifying the task body. The EMF tree editor in Rose is now only used minimally; to add annotations for Tasking, Shared and Environ Machines; typing annotations, and parameter direction information; and sensing/actuating annotations, where necessary. Further work is under way to integrate the code generation feature with the new Rodin editor.

	== Allowing Extensibility ==		== Allowing Extensibility ==

imported>Andy: /* Choices / Decisions */

2012-04-20T07:34:50Z

Choices / Decisions

← Older revision		Revision as of 07:34, 20 April 2012
Line 23:		Line 23:
	* Minimal use is made of the EMF tree editor in Rose.		* Minimal use is made of the EMF tree editor in Rose.

	These evolutions will be detailed hereafter. Moreover, the code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set		These evolutions will be detailed hereafter. Moreover, the code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set<ref name="aag">http://www.eclipse.org/epsilon/</ref>, but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor.

	<ref name="aag">http://www.eclipse.org/epsilon/</ref>

	, but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor.

	== Tasking Event-B and its edition ==		== Tasking Event-B and its edition ==

imported>Andy: /* Choices / Decisions */

2012-04-20T07:34:01Z

Choices / Decisions

← Older revision		Revision as of 07:34, 20 April 2012
Line 23:		Line 23:
	* Minimal use is made of the EMF tree editor in Rose.		* Minimal use is made of the EMF tree editor in Rose.

	These evolutions will be detailed hereafter. Moreover, the code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set, but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor.		These evolutions will be detailed hereafter. Moreover, the code generators have been completely re-written. The translators are now implemented using Java only. In our previous work we attempted to make use of the latest model-to-model transformation technology, available in the Epsilon tool set

			<ref name="aag">http://www.eclipse.org/epsilon/</ref>

			, but we decided to revert to Java since Epsilon lacked the debugging and productivity features of the Eclipse Java editor.

	== Tasking Event-B and its edition ==		== Tasking Event-B and its edition ==

imported>Andy: /* Motivations */

2012-04-20T07:29:01Z

Motivations

← Older revision		Revision as of 07:29, 20 April 2012
Line 4:		Line 4:
	= Motivations =		= Motivations =
	DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems		DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems
	<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language		<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language<ref>J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.</ref>, and use it as a basis for the abstractions used in our approach.<br>

	<ref>J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.</ref>

	, and use it as a basis for the abstractions used in our approach.<br>
	We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers, and thus motivated numerous evolutions and new features such as:		We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers, and thus motivated numerous evolutions and new features such as:
	* allowing a more seamless edition of tasking Event-B,		* allowing a more seamless edition of tasking Event-B,

imported>Andy: /* Motivations */

2012-04-20T07:28:17Z

Motivations

← Older revision		Revision as of 07:28, 20 April 2012
Line 6:		Line 6:
	<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language		<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language

	<ref ~~name="aaf"~~ J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.</ref>		<ref>J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.</ref>

	, and use it as a basis for the abstractions used in our approach.<br>		, and use it as a basis for the abstractions used in our approach.<br>

imported>Andy: /* Motivations */

2012-04-20T07:25:22Z

Motivations

← Older revision		Revision as of 07:25, 20 April 2012
Line 4:		Line 4:
	= Motivations =		= Motivations =
	DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems		DEPLOY industrial partners are interested in the formal development of multi-tasking, embedded control systems. During the project, work has been undertaken to investigate automatic generation, from Event-B models, for these type of systems
	<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language<ref name="J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006."</ref>, and use it as a basis for the abstractions used in our approach.<br>		<ref name="aaa">http://eprints.soton.ac.uk/270824/ "Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010"</ref><ref name="aab">http://eprints.soton.ac.uk/272006/ "Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany"</ref><ref name="aac">http://eprints.soton.ac.uk/272771/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B Models to Code: Sensing, Actuating, and the Environment. At SBMF2011, Sao Paulo, Brazil, 28 - 26 Sep 2011."</ref><ref name="aad">http://eprints.soton.ac.uk/335400/ "Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp. (In Press)"</ref><ref name="aae">http://eprints.soton.ac.uk/336226/ "Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp. (In Press)"</ref>. Initially, we chose to translate to the Ada programming language

			<ref name="aaf" J. Barnes. Programming in Ada 2005. International Computer Science Series. Addison Wesley, 2006.</ref>

			, and use it as a basis for the abstractions used in our approach.<br>
	We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers, and thus motivated numerous evolutions and new features such as:		We described our previous code generation feature as a demonstrator tool; chiefly a tool designed as a proof of concept, used by us to validate the approach. In this sense, the tool as it stands now, is the first prototype intended to be used by developers, and thus motivated numerous evolutions and new features such as:
	* allowing a more seamless edition of tasking Event-B,		* allowing a more seamless edition of tasking Event-B,