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)

B Method Update Site

• Atelier B Provers
• B2Rodin
• Brama

Downloading

Download Now!

Bugs Fixed and Feature Requests Implemented

  Bug 1813657: Refactoring menu is not related to refactoring.
  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.
  FR 2926238: extensible pretty print.
  FR 2942210: Make SC symbolFactory visible.
  FR 2949606: Add a replay proof command in event-B explorer.

Known Issues

[|Open bugs page ]

• Early releases of XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). More recent releases fix this bug (works fine with xulrunner-1.9.1.7). Alternatively, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:

-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner-1.9.0.14

where "/usr/lib/xulrunner-1.9.0.14" must be replaced with your actual XULRunner 1.9.0 installation directory.

• A warning like the following one is displayed to the standard output when platform starts on GNOME desktop:

(rodin:17254): GLib-WARNING **: g_set_prgname() called multiple times
 It's a GNOME bug, referenced at: [[1]]

• The error log shows the following problem:

org.osgi.framework.BundleException: The bundle could not be resolved. Reason: Missing Constraint: Import-Package: org.eclipse.equinox.internal.util.event; version="1.0.0"
at org.eclipse.osgi.framework.internal.core.AbstractBundle.getResolverError(AbstractBundle.java:1313)
...

It's an Eclipse 3.5 bug. Information found there: [[2]]

• The list of the currently open bugs is given below:

Bug 2989932: SM translation flow-down buttons KO  		 
Bug 2988294: Nested elaborated transitions produce conflicting actions   
Bug 2987749: Axioms in classtypes not quantified 
Bug 2979444: Matching ; 	
Bug 2979365: Auto completion in wizards 	
Bug 2974867: Camille text editor -  doesn't allow non alphanumeric chars
Bug 2974863: Camille text editor -  Class cast exception when saving a sm  
Bug 2968560: Dependence of Explorer & eventb.ui  
Bug 2964360: unsound inference rule  		 
Bug 2964359: Rule based prover allows me to define unsound rule  		 
Bug 2964350: RBP allows to generate theory with same name as a context  		 
Bug 2964346: RBP: illegal theory directory leads to strange behaviour  		 
Bug 2958877: {1 | true} --> Error Running Tool  		 
Bug 2957980: Proof Skeleton View : \n displayed as squares  		 
Bug 2952758: Highlighting of bound variables  		 
Bug 2952705: Progress bar running too fast  			 
Bug 2952645: Unable to parse || 	
Bug 2952134: conversion to mathematical symbols generates trailing spaces  	 
Bug 2952091: newPP is unsound 	
Bug 2949652: Event-B editor doesn't refresh  
Bug 2942182: unparsing then parsing gives a different expression 
Bug 2941496: NewPP outputs incorrect set of required Hypotheses  		 
Bug 2940575: some fomulas are truncated 	
Bug 2940315: mod operator should be compatible with itself  		 
Bug 2937132: newPP unresponsive 	
Bug 2937124: Symbol Table and Properties 
Bug 2934585: animB : impossible to start animation  		 
Bug 2931450: editor extension - clause names defined in wrong element  	 
Bug 2916134: Atelier-B PP does not understand S /= {}  		 
Bug 2900427: Event-B keyboard does not translate "or"  		 
Bug 2894645: Error on context named "axioms" 
Bug 2893782: error when building new project with a context 
Bug 2886026: "Overflow" in partition rewriting 
Bug 2883199: Fix "new" actions 
Bug 2882318: Error while entering symbol from symbol table  		 
Bug 2871290: Comments are still editable in a generated model  		 
Bug 2871281: Bad display of marked math symbols  		 
Bug 2869663: Changing the font in the pretty print view  		 
Bug 2844813: Turnstile unicode character 
Bug 2844786: Invisible icons in Proof Control coolbar  		 
Bug 2835692: Text Editor exception  		 
Bug 2824204: Change to Rodin Elements not reflected in editor  		 
Bug 2817523: No paste in root contextual menu of explorer  	 
Bug 2782243: BraveSansMono  		 
Bug 2630205: reasoning with "finite" clause 
Bug 2594282: brama - unexpected error  		 
Bug 2573332: Long formulas get truncated  		 
Bug 2531738: RODIN crash adding text to note or text box in class diagram  		 
Bug 2510307: Proof information window empty for grd/WD  		 
Bug 2371318: Unable to apply equality from left to right  	 
Bug 2231401: anormal,error message on animation  		 
Bug 2174629: No PO generated for unrefined event  		 
Bug 2105507: too difficult to work with explicit set expressions  		 
Bug 2082375: input file write-protection a problem to Rodin  		 
Bug 1971279: "java.lang.OutOfMemoryError ..." 
Bug 1954442: Too many handles used by Edit page on Windows  		 
Bug 1949927: newPP is too sensitive to unused hyps  		 
Bug 1841129: Incorrect proof status 	
Bug 1824177: B4free prover translation for <<-> fails  		 
Bug 1766826: Error messages from math parser incomprehensible  		 
Bug 1737819: WD properties are not fully propagated  		 
Bug 1441596: Tool conflicts caused by identically named files