Rodin Platform 1.3 Release Notes

What's New in Rodin 1.3?

• Event-B Editor

New in component popup menu. "New Event-B Project" and "New Event-B Component" wizards have been added to the "New" context menu of the event-B explorer. Right-clicking in a blank part or on a project in the Event-B explorer, a popup appears; then in the "New" section, these two actions are proposed.

new preference/properties mechanism. A new preference/properties mechanism to handle and use prefix settings. It is now possible to set prefixes for a workspace scope or a project scope. Prefix settings are extended automatically by editor contributions.

See also: Customize Prefixes

• Proving Perspective

A new "Replay Proof" command. Right-clicking any element in the Event-B Explorer shows the contextual menu, which contains a new command "Proof Replay on Undischarged POs" next to "Retry Auto Provers" and "Recalculate Auto Status".

See also: Proof Obligation Commands

NewPP. Changed the name displayed in proofs to "NewPP" to avoid ambiguity with "PP". It used to be displayed as "Predicate Prover".

• Rodin Builder

Direct children processing only. The builder now only processes direct children of project. Files located in subfolders are ignored.

• Changes for plugin-developers

Added the origin of predicates in a proof. In the sequent of the root node of a IProofTree, the IAxiom, IInvariant, ..., a predicate (hypothesis or goal) comes from can be fetched through the origin of its source location.

For instance: proofTree.getRoot().getSequent().goal().getSourceLocation().getOrigin()

Knowing nature of proof obligations. The nature of a proof obligation (Theorem, Well-Definedness, Invariant Preservation, ...) can be known from a IPOSequent.

See IPOGNature and IPOSequent#getPOGNature().

NewPP Plug-in. The newPP tactic has been published. See PPCore#newPP()

Added ExplorerPlugin#getSelectedStatuses(). Added a function ExplorerPlugin#getSelectedStatuses() to get the PS elements under the current explorer selection.

Extensible pretty print. It is now possible to extend the pretty print page with the same kind of mechanism used to extend the structured editor.

See also: Extending the Pretty Print Page

Requirements

• It is recommended to run the Rodin platform with a Java 1.5 Runtime Environment.
• Only a 32-bit version of the Rodin platform is provided. Some optional libraries dedicated to 32-bit support may be required in order to run it on a 64-bit OS. Moreover, you will have to install a 32-bit Java Virtual Machine (JVM), and then to set the -vm option to make sure that Rodin is run with the correct JVM.

eg. /usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java (You have to adjust paths to your system.)

External plug-ins

TODO: Describe here the available plug-ins, and the supported versions for this release.

• UML-B - Statemachine Animation (version 0.1.3)
• UML-B (version 1.0.1)
• Camille Editor (version 1.1.4)
• Shared Event Composition plug-in (version 1.1.5)
• Refactory plug-in (version 0.0.6)
• Records Extension (version 0.2.0.beta)

Downloading

Download Now!

Bugs Fixed and Feature Requests Implemented

  Bug 1813657: Refactoring menu is not related to refactoring. Implemented a new preference/properties mechanism to handle and use prefix settings.
  Bug 2945276: Rodin keyboard view displayed untimely.
  Bug 2952087: Rodin 1.2 reuses erroneous Rodin 1.1 proof.
  Bug 2952090: Added renaming of proof files.
  Bug 2952705: Progress bar running too fast.
  Bug 2952959: Disabling auto-provers doesn't work.
  Bug 2961115: Pipe as internal name
  Bug 2962503: PPTrans throws NPE
  Bug 2962688: Clean with AutoProve on works the second time
  Bug 2977104: Editors still opened when deleting a project.

  FR 2682079: Renaming issue. The renaming action now fills the renaming box with the current component's name and allows editing it.
  FR 2926238: extensible pretty print.
  FR 2942210: Make SC symbolFactory visible.
  FR 2949606: Add a replay proof command in event-B explorer.

Known Issues

TODO: Add here a link to the SourceForge Bugs page, after filtering bugs (Assignee Any, Status Open, Category Any, Group 1.3).