Past Developments - Revision history

imported>Laurent: /* Mathematical Language V2 */

2014-02-27T16:57:55Z

Mathematical Language V2

← Older revision		Revision as of 16:57, 27 February 2014
Line 21:		Line 21:

	The generation of well-definedness lemmas has been improved: [[Improved_WD_Lemma_Generation\| Improved WD lemma generation]].		The generation of well-definedness lemmas has been improved: [[Improved_WD_Lemma_Generation\| Improved WD lemma generation]].

			New implementation of [[Identifier Decomposition]] now supports mathematical extensions.

	==== Rodin Index Manager ====		==== Rodin Index Manager ====

imported>Laurent: Move more tasks from Current Development

2013-02-26T11:46:22Z

Move more tasks from Current Development

@@ Line 90: / Line 90: @@
 * Individual Requirements to be linked to individual Event-B-Entities
 * A basic completion test to be performed
 [[Category:Work done]]

imported>Laurent: Moved old tasks from Current development

2013-02-26T11:36:18Z

Moved old tasks from Current development

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

	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]].		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]].

			==== 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.

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

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

2013-02-26T11:34:14Z

Move Event-B editor from current dev to past dev

← Older revision		Revision as of 11:34, 26 February 2013
Line 43:		Line 43:
	The <tt>WD</tt> and <tt>FIS</tt> proof obligations for concrete actions were wrong and could introduce inconsistencies in Event-B models.		The <tt>WD</tt> and <tt>FIS</tt> proof obligations for concrete actions were wrong and could introduce inconsistencies in Event-B models.
	{{details\|Revisiting Feasibility POs\|the cause of this bug and its fix}}		{{details\|Revisiting Feasibility POs\|the cause of this bug and its fix}}

			====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]].

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

imported>Laurent: /* Core Platform */ Add Revisiting Feasibility POs

2012-01-25T16:19:56Z

Core Platform: Add Revisiting Feasibility POs

← Older revision		Revision as of 16:19, 25 January 2012
Line 35:		Line 35:

	==== Generated Model Elements ====		==== Generated Model Elements ====
	[[Systerel]] is in charge of this task.		[[Systerel]] was in charge of this task.
	Elements of a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants).		Elements of a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants).
	{{details\|Generated Model Elements\|Generated Model Elements}}		{{details\|Generated Model Elements\|Generated Model Elements}}

			====Fixing Proof Obligations====
			[[Systerel]] was in charge of this task.
			The <tt>WD</tt> and <tt>FIS</tt> proof obligations for concrete actions were wrong and could introduce inconsistencies in Event-B models.
			{{details\|Revisiting Feasibility POs\|the cause of this bug and its fix}}

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

imported>Laurent: /* Deploy Tasks */ Moved completed items for the core platform

2011-03-31T13:43:59Z

Deploy Tasks: Moved completed items for the core platform

← Older revision		Revision as of 13:43, 31 March 2011
Line 14:		Line 14:

	==== Mathematical Language V2 ====		==== Mathematical Language V2 ====
			[[Changes to the Mathematical Language of Event-B]] and the corresponding [[Mathematical_Language_Evolution_Design\|design]] documentation.

			[[Predicate_Variables_Extension\|Predicate variables extension]]

			[[Mathematical_extensions\|Proposals for mathematical extensions]]

	~~[[Changes to the Mathematical Language~~ of ~~Event~~-~~B]] and the corresponding~~ [[~~Mathematical_Language_Evolution_Design~~\|~~design~~]] ~~documentation~~.		The generation of well-definedness lemmas has been improved: [[Improved_WD_Lemma_Generation\| Improved WD lemma generation]].

	==== Rodin Index Manager ====		==== Rodin Index Manager ====
Line 21:		Line 26:
	{{details\|Rodin Index Design\|Rodin index design}}		{{details\|Rodin Index Design\|Rodin index design}}

	The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.		The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

			==== New Tactic Providers ====
			[[Systerel]] was in charge of this task.
			{{details\|New Tactic Providers\|New Tactic Providers}}

			The purpose is to give more flexibility to tactic providers by allowing them to provide as many tactic applications as they will for a given proof node, even they apply to the same predicate and at the same position.

			==== Generated Model Elements ====
			[[Systerel]] is in charge of this task.
			Elements of a model can be tagged as generated by a tool, in order to prevent the end-user from directly editing them (and their descendants).
			{{details\|Generated Model Elements\|Generated Model Elements}}

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

imported>Laurent: /* One Single View */

2011-03-31T13:38:48Z

One Single View

← Older revision		Revision as of 13:38, 31 March 2011
Line 25:		Line 25:
	== Exploratory Tasks ==		== Exploratory Tasks ==
	=== One Single View ===		=== One Single View ===
	[[User:Maria\|Maria Husmann]] was in charge of this exploratory work during is internship at [http://www.systerel.fr Systerel].		[[User:Maria\|Maria Husmann]] was in charge of this exploratory work during her internship at [http://www.systerel.fr Systerel].
	{{details\|Single View Design\|Single View Design}}		{{details\|Single View Design\|Single View Design}}
	The goal of this project was to present everything in a single view in Rodin. So the user do not have to switch perspectives.		The goal of this project was to present everything in a single view in Rodin. So the user do not have to switch perspectives.

	This work has been integrated into Rodin 0.9.2.		This work has been integrated into Rodin 0.9.2.


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

imported>Nicolas: Moved achieved work from current developments page

2009-08-13T16:06:19Z

Moved achieved work from current developments page

← Older revision		Revision as of 16:06, 13 August 2009
Line 12:		Line 12:

	This feature is now part of Rodin v0.9.0.		This feature is now part of Rodin v0.9.0.

			==== Mathematical Language V2 ====

			[[Changes to the Mathematical Language of Event-B]] and the corresponding [[Mathematical_Language_Evolution_Design\|design]] documentation.

			==== Rodin Index Manager ====
			[[Systerel]] is in charge of this task.
			{{details\|Rodin Index Design\|Rodin index design}}

			The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

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

imported>Mathieu: /* Plug-ins */ Requirement Management Plug-in

2009-03-04T09:43:33Z

Plug-ins: Requirement Management Plug-in

← Older revision		Revision as of 09:43, 4 March 2009
Line 23:		Line 23:

	=== Plug-ins ===		=== Plug-ins ===
			==== Requirement Management Plug-in ====
			[[User:Jastram\|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin\|Requirements Management Plug-in]].

			{{See also\|ReqsManagement\|Requirements Tutorial\|l1=Requirements Management Plug-in}}

			This plug-in allows:
			* Requirements to be edited in a set of documents (independently from Rodin)
			* Requirements to be viewed within Rodin
			* Individual Requirements to be linked to individual Event-B-Entities
			* A basic completion test to be performed

	[[Category:Work done]]		[[Category:Work done]]

imported>Mathieu: One Single View

2009-03-04T09:41:19Z

One Single View

← Older revision		Revision as of 09:41, 4 March 2009
Line 12:		Line 12:

	This feature is now part of Rodin v0.9.0.		This feature is now part of Rodin v0.9.0.

			== Exploratory Tasks ==
			=== One Single View ===
			[[User:Maria\|Maria Husmann]] was in charge of this exploratory work during is internship at [http://www.systerel.fr Systerel].
			{{details\|Single View Design\|Single View Design}}
			The goal of this project was to present everything in a single view in Rodin. So the user do not have to switch perspectives.

			This work has been integrated into Rodin 0.9.2.


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


			[[Category:Work done]]