Rodin Platform 1.1 Release Notes
What's New in Rodin 1.1?
- A new extensible plug-in for the Event-B Keyboard is included. The former one, namely org.eventb.eventBKeyboard, translated hard-coded key combos into hard-coded unicode mathematical symbols. There is now one main plug-in, org.rodinp.keyboard, that defines a mere extension point org.rodinp.keyboard.symbols to define associations between an ASCII sequence and a symbol. It avoids hard-coding anything.
- There are currently two extensions of this point:
- One in the plug-in org.eventb.keyboard, for standard Event-B notation translation.
- One in the plug-in ch.ethz.eventb.keyboard.latex, for LaTeX notation translation.
- The reasoners are now tagged with a version, which will evolve along with their behavior.
- New Rewriting rules and on prover rules are included:
- Arithmetic rules (e.g. the form <math>A+B+C-B \defi A+C</math> and a few others)
- DEF_IN_UPTO: <math>x \in a \upto b \defi a \leq x \land x \leq b</math>
- One point rule
- Goals of the form <math>\exists n \qdot \forall x \qdot x \in S \limp x \leq n</math> when you have a hypothesis that states <math>finite(S)</math>
- A new tactic provider extension API is proposed. It allows tactic providers to give several possible tactic applications, even at the same position in a predicate. This new mechanism is also intended to fit with rule-based provers needs.
- Proof obligations
- The POG does not not generate any longer THM POs for guards when the conditions have already been proved for the abstract event.
- The generated event-B files are tagged. These files cannot be modified.
- A symbol table view is provided. It contains the mathematical symbols. When clicking on a symbol, it is included at the current position in the text of the Rodin Context/Machine editor.
- PO Icons
- Changed color of 'pending' icon for undischarged POs from red to orange/brown.
- Used 'pending_pale' icons for unattempted POs in explorer.
- Reinforced the WD condition for the modulo operator. We now have exactly the same condition as in classical B: <math>x \bmod b~</math> is well-defined iff <math>0 \leq x \land 0 < y</math>.
- 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.)
Rodin Update Site
- UML-B 0.6.0
- Event-B EMF Framework 1.1.2
- Feature Composition Plug-in 0.0.3
- Refactoring Framework Plug-in 0.0.4
- Shared Event Composition Plug-in 1.1.4
Modularisation Plug-in Update Site
Prob Update Site
ETHZ Update Site
B Method Update Site
Fixed Bugs and Implemented Feature Requests
Bug 1822179: Problem with XML parser Bug 1830816: Incorrect associativity of function application Bug 1834722: no horizontal scroll bars Bug 1926739: Machine Renaming Bug 2004000: The cursor is not visible at the end of text fields. Bug 2024804: No typecheck error when missing INITIALISATION Bug 2616436: SWTException when deleting an element Bug 2648926: Post-Tactic is invoked after saving Bug 2782166: Clean & Build Bug 2804049: Exception on partition sent to ML Bug 2814047: Refines clause on INITIALISATION event ignored Bug 2818588: Long formulas not broken across lines Bug 2821439: functional simplification Bug 2821449: functional simplification Bug 2824401: NPE when following a marker Bug 2829164: exception in navigator Bug 2830809: parser inconsistent with Mathematical Language Specification Bug 2840549: Development: Building problem for path with blank Bug 2841423: use of set comprehension? Bug 2856893: Impossible to add an element to an event-B component Bug 2860800: Paths of Plugins (again) Bug 2864985: Problem with Design of EventBRoot Bug 2865874: Error when calling ML Bug 2031274: Rename problem FR 1592016: Automatic Completion FR 1740718: Verification for New Internal Element Wizards FR 1909636: Arithmetics simplification FR 1936295: Automatic rule for <+ FR 1942487: Remove membership for range FR 2140186: prooving when using "lambda expression" FR 2782135: Pretty Print Font Size FR 2803368: Versioning reasoners FR 2817266: Copy of full projects FR 2864252: Anticipated events in last refinement
- XULRunner 1.9.1 may cause an SWT exception that prevents from opening an editor (as well as any browser-based ui component). To fix it, it is possible to specify XULRunner path to point to 1.9.0: edit "rodin.ini" and add the following line:
where "/usr/lib/xulrunner-22.214.171.124" must be replaced with your actual XULRunner 1.9.0 install directory.
- Using Rodin 1.1 on GNOME desktop may result in a situation where buttons lock windows. To avoid this situation, it is needed to launch Rodin with
- 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 1743521: Event keyboard : abusive mapping in insertion mode 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 1819316: Existential PO does not discharge Bug 1820566: Problem with naming in Windows Bug 1824177: B4free prover translation for <<-> fails Bug 1824569: Error Markers in Synthesis view do not update Bug 1841129: Incorrect proof status Bug 1897572: Error in Proof Obligation Generator Bug 1919546: P1,PP,M0-M3 not available as post tactic Bug 1922694: Crazy Copy/Paste 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 1977355: Edit tab does not reflect changes made by other programs 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 2417801: Simplified hypothesis is not hidden 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 2657540: Synthesis view: elements inverted 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 2815882: Primed identifiers are allowed Bug 2817523: No paste in root contextual menu of explorer Bug 2818587: Machine renaming not propagated to extends clauses 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 2844889: Plug-in installation in Rodin platform 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