Plug-in Tutorial

What's New in Rodin 1.1?

• Rodin Keyboard

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:

1. One in the plug-in org.eventb.keyboard, for standard Event-B notation translation.
2. One in the plug-in ch.ethz.eventb.keyboard.latex, for LaTeX notation translation.

• Versioned Reasoners

The reasoners are now tagged with a version, which will evolve along with their behavior.

• New Rewriting rules and on prover rules are included:

1. Arithmetic rules (e.g. the form $A+B+C-B \defi A+C$ and a few others)
2. DEF_IN_UPTO: $x \in a \upto b \defi a \leq x \land x \leq b$
3. One point rule
4. Goals of the form $\exists n \qdot \forall x \qdot x \in S \limp x \leq n$ when you have a hypothesis that states $finite(S)$
5. SIMP_SPECIAL_OVERL
6. SIMP_FUNIMAGE_LAMBDA

• New Tactic Providers

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.

• Generated Model Elements

The generated event-B files are tagged. These files cannot be modified.

• Symbol Table

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.

• Modulo

Reinforced the WD condition for the modulo operator. We now have exactly the same condition as in classical B: $x \bmod b~$ is well-defined iff $0 \leq x \land 0 < y$.

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

• 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

• Modularisation Plug-in 1.0.2

Prob Update Site

• Camille Texteditor
• ProB and ProB Disprover (currently only Mac OS and Linux)
• BMotion Studio

ETHZ Update Site

• Pattern Plug-in 0.8.0

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.

• 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