Past Developments

This page sum up the developments recently done around or for the Rodin Platform, which are integrated or compatibles with the last platform revision.

Deploy Tasks

The following tasks were planned at some stage of the Deploy project.

Core Platform

Undo / Redo for editors

See also: Undo/Redo design

Systerel is in charge of this task.

The goal of this task is to implement an undo/redo feature for editing actions.

This feature is now part of Rodin v0.9.0.

Mathematical Language V2

Changes to the Mathematical Language of Event-B and the corresponding design documentation.

Predicate variables extension

Proposals for mathematical extensions

The generation of well-definedness lemmas has been improved: Improved WD lemma generation.

New implementation of Identifier Decomposition now supports mathematical extensions.

Rodin Index Manager

Systerel is in charge of this task.

For more details on Rodin index design, see 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.

New Tactic Providers

Systerel was in charge of this task.

For more details on New Tactic Providers, see 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 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).

For more details on Generated Model Elements, see Generated Model Elements.

Fixing Proof Obligations

Systerel was in charge of this task. The WD and FIS proof obligations for concrete actions were wrong and could introduce inconsistencies in Event-B models.

For more details on the cause of this bug and its fix, see Revisiting Feasibility POs.

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.

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.

For more details on this topic, see [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.

For more details on this topic, see Extending Refinement Actions.

Until Rodin 2.1, the Refine and 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.

For more details on this topic, see Current Proof Tree Node in UI.

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

One Single View

Maria Husmann was in charge of this exploratory work during her internship at Systerel.

For more details on Single View Design, see 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

Requirement Management Plug-in

Michael at Düsseldorf is in charge of the Requirements Management Plug-in.

See also: Requirements Management Plug-in and Requirements Tutorial

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

B2Latex Plug-in

Systerel is in charge of the maintenance of B2Latex.

Kriangsak Damchoom has updated the plug-in to add extensions of events.

Event Model Decomposition (A-style)

Systerel (Carine) was in charge of this task.

For more details on Event Model Decomposition, see Event Model Decomposition.

The purpose of (A-style) event model decomposition is to cut a heavy event system into smaller pieces which can be handled more comfortably than the whole. More precisely, each piece can then be refined independently of the others.

New Proof Rules

This document describes the set of newly added reasoners for improving the usability of the prover within Rodin Platform.