Current Developments - Revision history

imported>Laurent: /* Core Platform */

2014-03-18T16:35:29Z

Core Platform

← Older revision		Revision as of 16:35, 18 March 2014
Line 15:		Line 15:

	=== Core Platform ===		=== Core Platform ===

			====Extended Operator Translation====

			The purpose of this [[Extended Operator Translation\|development]] is to improve the support of mathematical extensions in external provers without changing them.


	==== Text Editor ====		==== Text Editor ====

imported>Laurent: /* SMT Plug-in */

2014-03-18T16:07:26Z

SMT Plug-in

← Older revision		Revision as of 16:07, 18 March 2014
Line 120:		Line 120:
	proposed in [[Mathematical_extensions]]. For more details, we refer to the [[Rule-based_Prover_Plug-in]] page.		proposed in [[Mathematical_extensions]]. For more details, we refer to the [[Rule-based_Prover_Plug-in]] page.
	and [[Image:Rule-based_Prover_Proposal.pdf \| Proposal for a rule-based extensible prover]].		and [[Image:Rule-based_Prover_Proposal.pdf \| Proposal for a rule-based extensible prover]].

	~~==== SMT Plug-in ====~~

	~~[[Systerel]] ([[User:YGU\|YGU]]) is in charge of this task.~~
	~~{{details\|SMT Plug-in\|SMT Plug-in}}~~
	~~{{details\|Event-B to SMT-LIB\|Event-B to SMT-LIB}}~~

	~~The purpose of the plug-in is to integrate SMT solvers into Rodin.~~

	== Exploratory Tasks ==		== Exploratory Tasks ==

imported>Laurent: /* Core Platform */

2014-03-18T16:06:53Z

Core Platform

← Older revision		Revision as of 16:06, 18 March 2014
Line 15:		Line 15:

	=== Core Platform ===		=== Core Platform ===

	~~====Rodin 3.0====~~

	~~Preliminary design for [[Rodin Platform 3.0 Release Notes\|Rodin 3.0]] has started.~~

	~~There is a note about defining which variant of the Event-B language is used in an Event-B component [[Language of an Event-B Component]].~~

	==== Text Editor ====		==== Text Editor ====

imported>Laurent: /* Rodin 3.0 */

2013-11-20T11:05:21Z

Rodin 3.0

← Older revision		Revision as of 11:05, 20 November 2013
Line 19:		Line 19:

	Preliminary design for [[Rodin Platform 3.0 Release Notes\|Rodin 3.0]] has started.		Preliminary design for [[Rodin Platform 3.0 Release Notes\|Rodin 3.0]] has started.

			There is a note about defining which variant of the Event-B language is used in an Event-B component [[Language of an Event-B Component]].

	==== Text Editor ====		==== Text Editor ====

imported>Laurent: Move more tasks to past development

2013-02-26T11:45:55Z

Move more tasks to past development

@@ Line 62: / Line 62: @@
 * a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
 * a 2D viewer to inspect the state space of the specification
 ==== Parallel Composition Plug-in ====
@@ Line 143: / Line 132: @@
 The purpose of the plug-in is to integrate SMT solvers into Rodin.
 == Exploratory Tasks ==

imported>Laurent: Moved old tasks to Past development

2013-02-26T11:36:26Z

Moved old tasks to Past development

← Older revision		Revision as of 11:36, 26 February 2013
Line 24:		Line 24:

	The first version of the TextEditor will be released in a few weeks (following the Rodin 1.0 release). Until then we are going to release a few testing releases (beta) for interested users. Find detailed information on the page [[Text Editor\|TextEditor]].		The first version of the TextEditor will be released in a few weeks (following the Rodin 1.0 release). Until then we are going to release a few testing releases (beta) for interested users. Find detailed information on the page [[Text Editor\|TextEditor]].

	~~==== EMF framework for Event-B ====~~
	Newcastle, Southampton and Düsseldorf have begun to develop an EMF framework to support Rodin modelling tools based on EMF. The framework includes an EMF representation of Event-B, a synchronising persistence interface for loading and saving models via the Rodin API and facilities to support text editing and parsing. Examples of tools that will be based on the EMF framework for Rodin are, a Text editor, a compare/merge editor (which can be used for team based development), pattern/composition tools, Diagram Editors.

	~~More details can be found here: [[EMF framework for Event-B]]~~

	~~==== Preferences for the automatic tactics ====~~
	~~[[Systerel]] is in charge of this task.~~
	~~{{details\|http://handbook.event-b.org/current/html/preferences.html#preferences_for_the_automatic_tactics Preferences for the automatic tactics}}~~

	~~The purpose is to give more detailed preferences to the user to build his own automated tactics.~~

	~~==== Extending the Refine/Extend actions ====~~
	~~[[Systerel]] is in charge of this task.~~
	~~{{details\|Extending Refinement Actions\|this topic}}~~

	Until Rodin 2.1, the {{Menu\|Refine}} and {{Menu\|Extend}} actions were hard-coded in the event-B UI plug-in. This development aims at opening up their implementation so that external plug-ins can contribute to these actions.

	~~==== Views Based on the Current Proof Tree Node ====~~
	~~[[Systerel]] is in charge of this task.~~
	~~{{details\|Current Proof Tree Node in UI\|this topic}}~~

	Two views (Proof Details and Type Environment) display some information which is associated to the current proof tree node, if any. However, in Rodin 2.3 the behavior of these views is somewhat strange and someone often has to click in various places to refresh these views. The objective of this task is to make these views more user-friendly.

	=== Plug-ins ===		=== Plug-ins ===

imported>Laurent: Move Event-B editor from current dev to past dev

2013-02-26T11:34:22Z

Move Event-B editor from current dev to past dev

← Older revision		Revision as of 11:34, 26 February 2013
Line 19:		Line 19:

	Preliminary design for [[Rodin Platform 3.0 Release Notes\|Rodin 3.0]] has started.		Preliminary design for [[Rodin Platform 3.0 Release Notes\|Rodin 3.0]] has started.

	~~====Better event-B Editor====~~

	Feedback from users indicates strongly that the current layout used in the default event-B editor (edit tab) is sub-optimal and severely hinders usability of the Rodin platform. Ideas for improving this are collected on page: [[Layout improvements in the event-B editor]].

	==== Text Editor ====		==== Text Editor ====

imported>Laurent: /* Current Tasks */

2012-07-21T13:56:50Z

Current Tasks

← Older revision		Revision as of 13:56, 21 July 2012
Line 5:		Line 5:

	== Current Tasks ==		== Current Tasks ==
	The following tasks were planned at some stage of the [[Deploy]] project.		The following tasks were planned at some stage of the [[Deploy]] or [[Advance]] project.

	=== Code Generation ===		=== Code Generation ===

imported>Laurent: /* Core Platform */ Rodin 3.0

2012-07-21T13:55:24Z

Core Platform: Rodin 3.0

← Older revision		Revision as of 13:55, 21 July 2012
Line 15:		Line 15:

	=== Core Platform ===		=== Core Platform ===

			====Rodin 3.0====

			Preliminary design for [[Rodin Platform 3.0 Release Notes\|Rodin 3.0]] has started.

	====Better event-B Editor====		====Better event-B Editor====

imported>Laurent at 13:52, 21 July 2012

2012-07-21T13:52:50Z

← Older revision		Revision as of 13:52, 21 July 2012
Line 4:		Line 4:
	You may also have a look at [[Past Developments\|past developments]].		You may also have a look at [[Past Developments\|past developments]].

	== ~~Deploy~~ Tasks ==		== Current Tasks ==
	The following tasks were planned at some stage of the [[Deploy]] project.		The following tasks were planned at some stage of the [[Deploy]] project.