Difference between pages "Rodin Editor User Guide" and "Rodin Platform 1.1 Release Notes"

Revision as of 10:32, 11 November 2009

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:

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.

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:

Arithmetic rules (e.g. the form $A+B+C-B \defi A+C$ and a few others)
DEF_IN_UPTO: $x \in a \upto b \defi a \leq x \land x \leq b$
One point rule
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)$
SIMP_SPECIAL_OVERL
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

http://wiki.event-b.org/index.php/Refactoring_Framework http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B

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

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 
  
  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 2031274: Rename problem
  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

Difference between pages "Rodin Editor User Guide" and "Rodin Platform 1.1 Release Notes"

Revision as of 10:32, 11 November 2009

Contents

What's New in Rodin 1.1?

Requirements

External plug-ins

Rodin Update Site

Modularisation Plug-in Update Site

Prob Update Site

Downloading

Fixed Bugs and Implemented Feature Requests

Known Issues

Navigation menu

Page actions

Page actions

Personal tools

Navigation

contribute

Search

Tools

@@ Line 1: / Line 1: @@
-== Introduction ==
+{{TOCright}}
-The Rodin Editor plug-in provides a structured editor to model in Event-B withing Rodin. This editor uses a textual representation, and edition is done through an overlay text editor and action depending on the caret position in the text.<br>
+== What's New in Rodin 1.1? ==
-For more details about the principles of this editor,  see [[Rodin_Editor|the Rodin Editor Plug-in page]].
-''<span style="color:#FF4500">IMPORTANT :  we identified a source of concurrency issue in the current version (0.5.0) of the plug-in.</span>''<br>
-<span style="color:#FF4500">'''To avoid any trouble, please do not generate files while having some Rodin Editor open, and edit only one model per project at once.'''</span>
-== Installation ==
+* [[Rodin_Keyboard | Rodin Keyboard]]
+:A new extensible plug-in for the Event-B Keyboard is included. The former one, namely <tt>org.eventb.eventBKeyboard</tt>, translated hard-coded key combos into hard-coded unicode mathematical symbols. There is now one main plug-in, <tt>org.rodinp.keyboard</tt>, that defines a mere extension point <tt>org.rodinp.keyboard.symbols</tt> 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 <tt>org.eventb.keyboard</tt>, for standard Event-B notation translation.
+# One in the plug-in <tt>ch.ethz.eventb.keyboard.latex</tt>, for LaTeX notation translation.
-=== Setup ===
+* [[Versioned Reasoners | Versioned Reasoners]]
-Install the Rodin Editor plug-in:
+:The reasoners are now tagged with a version, which will evolve along with their behavior.
-# In the menu choose Help -> Install New Software...
-# In the Work with dropdown list, choose the location URL: Rodin - http://rodin-b-sharp.sourceforge.net/updates
-# Select the Rodin Editor feature then click the check box
-# Click Next, after some time, the Install Details page appears
-# Click Next and accept the license
-# Click Finish
-# A Security Warning window may appear: click OK
-# Restart Rodin as suggested.
-Now you are ready to use the new Rodin Editor plug-in.
-=== Release Notes ===
+* New [[All_Rewrite_Rules | Rewriting rules]] and on prover rules are included:
-See [[Rodin_Editor_Release_History | Rodin Editor Release Notes]]
+# 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>
+# [http://www.cs.cmu.edu/afs/cs/academic/class/15671-f95/www/handouts/proof/node1.html 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>
+# SIMP_SPECIAL_OVERL
+# SIMP_FUNIMAGE_LAMBDA
+* [[New Tactic Providers | 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.
-== Editing ==
+* 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.
-This is a small exercice to get used to the principles of the new structured editor. It is based on the 'Celebrity' project of the tutorial. You can download the resulting project [http://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Tutorial/1.1/Celebrity.zip/download <tt>here</tt>].<br>
+* [[Generated Model Elements | Generated Model Elements]]
-We will here build the context ''Celebrity_C0''.
+:The generated event-B files are tagged. These files cannot be modified.
-=== Create a context, add elements to it ===
+* [[Symbol Table | Symbol Table]]
-Let's create a Rodin project, and add a context component called ''Celebrity_C0'' to it.<br>
+: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.
--- By opening this context with the Rodin Editor (right click > Open with > Rodin Editor) you shall obtain the following:<br>
-[[Image:RodinEditor_UserGuide_step1.png]]
-This editor allows to do things based on the position of the caret.<br>
+* PO Icons
--- Place the caret at one location on the line of the context label, and before the label, as on the figure below:
+:Changed color of 'pending' icon for undischarged POs from red to orange/brown.
+:Used 'pending_pale' icons for unattempted POs in explorer.
-[[Image:RodinEditor_UserGuide_step2.png]]
+* Modulo
+: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>.
--- Then right click, and add a 'Constant' child using the menus :
+== 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.'' <tt>/usr/local/rodin/rodin -vm /usr/lib/jvm/ia32-java-1.5.0-sun/bin/java</tt> (You have to adjust paths to your system.)
-[[Image:RodinEditor_UserGuide_step3.png|600px]]
+== External plug-ins ==
--- Save the file. <br>
+=== Rodin Update Site ===
-After saving the file, the error markers are recalculated, and you have an error that appears on the newly created constant 'cst1'.<br>
+* [[UML-B_Release_History|UML-B 0.6.0]]
-You shall see this :
+* [[Event-BEMF_ReleaseHistory|Event-B EMF Framework 1.1.2]]
+* [[Feature_Composition_Release_History|Feature Composition Plug-in 0.0.3]]
+* [[Refactoring_Framework_Release_History|Refactoring_Framework Plug-in 0.0.4]]
+* [[Shared Event Composition_Release_History|Shared Event Composition Plug-in 1.1.4]]
-[[Image:RodinEditor_UserGuide_step4.png|600px]]
-Note that you can visualize the error message by going over the error marker with the mouse.
+http://wiki.event-b.org/index.php/Refactoring_Framework
+http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B
--- Enter the edition mode by clicking inside the label 'cst1'.
+=== Modularisation Plug-in Update Site ===
+* [[Modularisation Plug-in|Modularisation Plug-in 1.0.2]]
-[[Image:RodinEditor_UserGuide_step5.png]]
+=== Prob Update Site ===
+* [[Text_Editor|Camille Texteditor]]
+* [http://www.stups.uni-duesseldorf.de/ProB ProB] and ProB Disprover (currently only Mac OS and Linux)
+* [http://www.stups.uni-duesseldorf.de/BMotionStudio/ BMotion Studio]
-The overlay editor then appears (cst1 is in black, and the background is gray[see above]) and you can modify the label of the constant.<br>
+== Downloading ==
--- Modify the label to be 'k'and exit the overlay edition by pressing 'Enter'. ''Note that because 'Enter' is used to enter or exit the overlay mode under the caret, in order to insert carriage return in text, you have to press CTRL+ENTER.<br>''
+[https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.1/ Download Now!]
-You can then save the file. <br>
-You then see something like the following.
-[[Image:RodinEditor_UserGuide_step6.png]]
+== 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
+   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
-Then we want to add another constant. As we have 'k' already, we will use 'add sibling' command to add another constant after k.<br>
+== Known Issues ==
--- Place the caret before k as on the following picture :
-[[Image:RodinEditor_UserGuide_step7.png]]
+* 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.
--- Right-click. The following context menu appears :
+* The list of the currently open bugs is given below:
-[[Image:RodinEditor_UserGuide_step8.png|200px]]
+   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 2031274: Rename problem
+   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
--- Click on "Add Sibling" you see then that a new constant was created, named 'cst1'.
+[[Category:Rodin Platform]]
-[[Image:RodinEditor_UserGuide_step9.png]]
-You can then enter the overlay edition mode to change this value to 'c'
-''' CONGRATULATIONS! You learned how to use the Rodin Editor.'''
-=== Using keyboard shorcuts ===
-Here is the list of the currently key bindings which are set by default and specific to the Rodin Editor.
-{{SimpleHeader}}
-|-
-! scope=col | KEY SEQUENCE || ACTION
-|-
-| BACKSPACE (ENTER) || Enter the edition mode using the overlay editor if the caret is on an editable place.
-|-
-| DEL || Suppress the element after the caret position
-|-
-| CTRL+T || Add a sibling of the element pointed by the caret position. The sibling is placed just after this latter one.
-|-
-| CTRL+SHIFT+N || Opens a popup to select the element type of the child to add to the element pointed by the caret position. Note that if there is only one child type, the child will be directly created.
-|-
-| CTRL+BACKSPACE || Insert a new carriage return while editing with the overlay editor.
-|-
-| ALT+ARROW_UP || Move up the selected elements.
-|-
-| ALT+ARROW_DOWN || Move down the selected elements.
-|-
-| SHIFT+ARROW_UP || Select elements up.
-|-
-| SHIFT+ARROW_DOWN || Select elements down.
-|-
-| ALT+ESC || Quit the current overlay edition (if any) and forget the modifications made, frees the current selection.
-|-
-| TAB || Go to the next editable place (i.e. to the next editable element attribute)
-|-
-| SHIFT+TAB || Go to the previous editable place (i.e. to the next editable element attribute)
-|}
-=== Customize this list ===
-If you don't like these shortcuts, you can modify them by setting your own key preferences.
-To do so, go to Window > Preferences and then General > Key. A table appears were you can find and edit the shortcuts.
-== Tips & Tricks ==
-A command currently (i.e. in Rodin 2.2) disable the possibility to use the ESC instead of ALT+ESC sequence. This is quite cumbersome, and can be tuned!
-To do so, open the preference table for key shortcuts (described above) and after ensuring you disabled the filters of uncategorized commands (using the Filters... dialog)
-search for the command named "Restore Styles". This is the command to release the highlights in the proving views. You can then swith the sequence of this command to ALT+ESC and change the value of the "Abort edition and free selected items" command to ESC. After applying these settings, the shortcuts will be modified as wished above.