Rodin Platform 1.2 Release Notes

From Event-B
Revision as of 10:06, 28 July 2010 by imported>Pascal (→‎External plug-ins)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigationJump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

What's New in Rodin 1.2?

  • Event-B Editor
Section expanding. A preference has been added for section expanding (See "Window > Preferences > Event-B > Modelling UI"). More precisely, this new option allows to specify that the sections shall not be expanded when unfolding an element of the Event-B editor. By default, any section of an element is expanded (as in previous releases).
Generated elements. The generated elements (e.g., produced by UML-B or the decomposition plug-in) cannot be edited, and appear grayed in the Event-B editor. This feature concerns whole generated contexts/machines, as well as other Event-B elements such as events, variables, ...
  • Proving Perspective
Easily creating new projects or components. Shortcuts have been added to the "File > New" menu of the Proving perspective to create a new Event-B project or a new Event-B component.
Copying from the proof skeleton to the proof tree. It is now possible to copy a subtree of a stored proof from the proof skeleton view to an edited proof tree. See also Copy/Paste to Proof Tree.
Hypothesis View. A dropdown list is now included to the Hypothesis view, to toggle the "Consider hidden hypotheses" preference directly from the hypothesis view. A quick search field and its related buttons have been added.
  • Rewriting Rules and Inference Rules

The existing rules have been reviewed and several implemented rules have been fixed.

FIN_FUN1_R, FIN_FUN2_R, FIN_FUN_IMG_R, FIN_FUN_RAN_R and FIN_FUN_DOM_R. The well-definedness condition was not implemented. See also Inference Rules.
DISTRI_RANSUB_BUNION_R, DISTRI_RANSUB_BINTER_R, DISTRI_DOMSUB_BUNION_L and DISTRI_DOMSUB_BINTER_L. These rules were wrongly defined and wrongly implemented. See the history of the Relation Rewrite Rules page for details.
  • Migration to Eclipse 3.5 (Galileo)
The extension point org.eclipse.core.contenttype.contentTypes is now used instead of the deprecated org.eclipse.core.runtime.contentTypes.
The method "org.osgi.service.prefs.Preferences.flush" is used instead of the deprecated org.eclipse.core.runtime.Plugin.savePluginPreferences.
Added support for predicate variables in the AST library.
In the previous release, it was possible to mark an Event-B machine/context as generated, in order to prevent users from inadvertently modifying it.
In this release, more fine-grained "read only" restrictions are enforced and any internal element may be tagged as generated (org.eventb.core.generated="true").

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.

B Method Update Site

Downloading

Download Now!

Bugs Fixed and Feature Requests Implemented

  Bug 1819316: Existential PO does not discharge
  Bug 1820566: Problem with naming in Windows 
  Bug 1824569: Error Markers in Synthesis view do not update
  Bug 1922694: Crazy Copy/Paste
  Bug 1977355: Edit tab does not reflect changes made by other programs
  Bug 2031274: Rename problem
  Bug 2657540: Synthesis view: elements inverted
  Bug 2815882: Primed identifiers are allowed
  Bug 2818587: Machine renaming not propagated to extends clauses
  Bug 2880858: Wrong arithmetic simplification
  Bug 2883204: Symbols View not directly accessible
  Bug 2884511: Rewritten formula should be type checked exception
  Bug 2884753: Oftype makes assert exception errors in hypotheses page
  Bug 2884774: No indication of Theorem guards in pretty print tab
  Bug 2891365: Unexpected Error (possibly stack overflow)
  Bug 2893379: Can't edit Refinement if var and event have the same name
  Bug 2900389: Event-B keyboard does not translate "or"
  Bug 2900456: Empty Goal Window
  Bug 2901018: "distinct variable" requirement in lambda abstraction
  Bug 2908239: id (identity function) ill-typed in rodin
  Bug 2909409: Unavoidably too many open handles?
  Bug 2916130: The lasso command selects hidden hypotheses
  Bug 2931424: NPE in SearchHypothesis view
  Bug 2936324: Extends clauses in pretty print
  Bug 2938707: instable Event B machine editor (v1.2RC1)
  Bug 2939467: SWTException: Graphic is disposed when saving proofs
  Bug 2940139: org.eventb.core.seqprover.totalDom:0 unsound
  Bug 2941295: Race condition in XProverCall and descendants
  
  FR 1614997: Theorems following event guards
  FR 1866809: Rewriting automatically dom(f) = S
  FR 1942714: Set comprehension rewrite
  FR 2073763: Support for "new" sets of relations
  FR 2740294: Functions on finite set are finite
  FR 2844800: Copy from Proof Skeleton to Proof Tree
  FR 2922261: Launch prover(s) automatically on added hypothesis
  FR 2937100: Traces for Simplification Rewriter
  FR 2937127: Symbol Table view

Known Issues

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

  • Using Rodin on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin

It's a GTK bug, referenced for Eclipse at [[1]]
See also Gnome and broken buttons.

  • 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. Information found there: [[2]]

  • 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: [[3]]

  • The list of the currently open bugs is given below:
  Bug 1441596: Tool conflicts caused by identically named files
  Bug 1737819: WD properties are not fully propagated
  Bug 1766826: Error messages from math parser incomprehensible
  Bug 1813657: Refactoring menu is not related to refactoring
  Bug 1818464: Trivial PO does not discharge
  Bug 1824177: B4free prover translation for <<-> fails
  Bug 1841129: Incorrect proof status
  Bug 1897572: Error in Proof Obligation Generator
  Bug 1919546: P1,PP,M0-M3 not available as post tactic
  Bug 1948095: importing existing projects
  Bug 1949927: newPP is too sensitive to unused hyps
  Bug 1954442: Too many handles used by Edit page on Windows
  Bug 2082375: input file write-protection a problem to Rodin
  Bug 2105507: too difficult to work with explicit set expressions
  Bug 2174629: No PO generated for unrefined event
  Bug 2371318: Unable to apply equality from left to right
  Bug 2414463: Builder called on non-Rodin files
  Bug 2433212: Poor performance under KDE
  Bug 2510307: Proof information window empty for grd/WD
  Bug 2531738: RODIN crash adding text to note or text box in class diagram
  Bug 2573332: Long formulas get truncated
  Bug 2630205: reasoning with "finite" clause
  Bug 2648946: Predicate Provers (newPP, P0) unable to discharge simple PO
  Bug 2656831: saving proofs does not always work
  Bug 2694492: proB widget do not display on second proB launch
  Bug 2744052: NullPointerException in Builder on cyclic refinement
  Bug 2782126: Your platform does not support SWT Browser widget.
  Bug 2782243: BraveSansMono
  Bug 2817523: No paste in root contextual menu of explorer
  Bug 2824204: Change to Rodin Elements not reflected in editor
  Bug 2827806: Zombie files in buffer
  Bug 2835692: Text Editor exception
  Bug 2836774: Text Editor unable to save  (exception)
  Bug 2844786: Invisible icons in Proof Control coolbar
  Bug 2844797: The Proof Skeleton View does not adapt to the container
  Bug 2844813: Turnstile unicode character
  Bug 2869663: Changing the font in the pretty print view
  Bug 2871281: Bad display of marked math symbols
  Bug 2871290: Comments are still editable in a generated model
  Bug 2882318: Error while entering symbol from symbol table
  Bug 2883199: Fix "new" actions
  Bug 2886026: "Overflow" in partition rewriting
  Bug 2893782: error when building new project with a context
  Bug 2894645: Error on context named "axioms"
  Bug 2895507: MH and other rules are ill-defined
  Bug 2900427: Event-B keyboard does not translate "or"
  Bug 2916134: Atelier-B PP does not understand S /= {}
  Bug 2931450: editor extension - clause names defined in wrong element
  Bug 2934585: animB : impossible to start animation
  Bug 2937124: Symbol Table and Properties
  Bug 2937132: newPP unresponsive
  Bug 2940315: mod operator should be compatible with itself
  Bug 2940575: some fomulas are truncated
  Bug 2941496: NewPP outputs incorrect set of required Hypotheses
  Bug 2942182: unparsing then parsing gives a different expression

Post Release Bugs