Difference between pages "Rodin Platform 1.1 Release Notes" and "File:TheoryCGRules.png"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Afuerst
 
(Maintenance script uploaded File:TheoryCGRules.png)
 
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]]
 

Latest revision as of 20:50, 30 April 2020