D32 General Platform Maintenance
Overview
The main goal of the platform corrective and evolutive maintenance is to fix the listed known bugs, and implement some new requested features. As in the previous years of Deploy, these bugs and features are reported either by mail or through dedicated SourceForge trackers.
The terse list below gives an overwiew of the noteworthy features added in the main platform during the past year:
- Proof replay of undischarged POs (releases 1.3 and upper)
- It often happens, while modifying a model, that a set of previously manually discharged POs are slightly changed and need to be discharged again. However, replaying the proof for those POs could most of the time be enough to discharge it. Hence, a command was added to manually try replaying the proofs for a set of undischarged POs. This request was expressed by end users. See [1].
- Rule Details View (releases 2.0 and upper)
- When doing an interactive proof, one is guided by the proof tree appearing on the proof tree view. However, it is sometimes needed to get more informations about the rules being involved in a proof, such as instantiation details, hidden hypotheses, etc. The Rule Details View displaying such details has been added.
- Refactoring plug-in (releases 1.2 and upper)
- Documentation
- Plug-in developers expressed their need to get a detailed documentation about Rodin extension ability. A dedicated tutorial has been written accordingly, and was the support of a training session given at the Rodin User and Developer Workshop in Düsseldorf this year.
See the Release Notes and the SourceForge databases (bugs and feature requests) for details about the previous and upcoming releases of the Rodin platform.
Motivations
The evolutive maintenance (resp. corrective maintenance) has its origin in the Deploy project's description of work, and the various requests (resp. bug reports) listed by WP1-4 partners, developers and users. Since the Deploy project's birth, various streams can be used to express feature requests or track an encountered bug :
- - dedicated trackers,
- - mail to the deploy user list, etc.
During the WP9 meetings, maintenance tasks to perform are being given a priority and are assigned to an according WP9 partner (as mentionned in the D23). The higher priority is given to WP partners requests. The following table describes the tasks motivating the evolutive maintenance that has been done during the last Deploy project's year, as well as scheduled tasks :
| Type | Origin | Maintenance Task | Done | Scheduled |
|---|---|---|---|---|
| Documentation | Developers | Rodin Extension documentation | x | |
| End Users | Meaning of Retry auto-provers / Recalculate auto-status | x | ||
| Evolutive Maintenance | End Users | Adding a replay proof command in the Event-B Explorer |
Choices / Decisions
---MAC plat 3.6
Available Documentation
As in the previous D23 delivrable, the following pages give useful information about the Rodin platform releases:
- Release notes.
- See Rodin Platform Releases.
- More details are provided in the notes distributed with each release (eg. [2]).
- Bugs.
- See [3].
- Feature requests.
- See [4].
Planning
The Rodin Platform Releases wiki page lists in particular the upcoming releases and give the scheduled release dates.
