From Event-B
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.
- Arithmetic rules (e.g. the form
and a few others)
- DEF_IN_UPTO:
- One point rule
- Goals of the form
when you have a hypothesis that states finite(S)
- SIMP_SPECIAL_OVERL
- SIMP_FUNIMAGE_LAMBDA
- 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.
- 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.
- 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:
is well-defined iff 
.
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
Rodin Update Site
Modularisation Plug-in Update Site
Prob Update Site
ETHZ Update Site
B Method Update Site
Downloading
Download Now!
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
Known Issues
- 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:
-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 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
GDK_NATIVE_WINDOWS=1 /path_to_rodin/rodin
- 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
