imported>Afuerst |
|
Line 1: |
Line 1: |
− | {{TOCright}}
| |
| | | |
− | == What's New in Rodin 1.1? ==
| |
− |
| |
− | * [[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.
| |
− |
| |
− | * [[Versioned Reasoners | Versioned Reasoners]]
| |
− | :The reasoners are now tagged with a version, which will evolve along with their behavior.
| |
− |
| |
− | * New [[All_Rewrite_Rules | 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>
| |
− | # [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.
| |
− |
| |
− | * 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 | Generated Model Elements]]
| |
− | :The generated event-B files are tagged. These files cannot be modified.
| |
− |
| |
− | * [[Symbol Table | 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: <math>x \bmod b~</math> is well-defined iff <math>0 \leq x \land 0 < y</math>.
| |
− |
| |
− | == 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.)
| |
− |
| |
− | == External plug-ins ==
| |
− |
| |
− | === Rodin Update Site ===
| |
− | * [[UML-B_Release_History|UML-B 0.6.0]]
| |
− | * [[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]]
| |
− |
| |
− | === Modularisation Plug-in Update Site ===
| |
− | * [[Modularisation Plug-in|Modularisation Plug-in 1.0.2]]
| |
− |
| |
− | === 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]
| |
− |
| |
− | === ETHZ Update Site ===
| |
− | * [[Pattern|Pattern Plug-in 0.8.0]]
| |
− |
| |
− | == Downloading ==
| |
− | [https://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/1.1/ 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
| |
− |
| |
− | [[Category:Rodin Platform]]
| |