imported>Renato |
|
| Line 1: |
Line 1: |
| − | {{TOCright}}
| + | Return to [[Rodin Plug-ins]] |
| | | | |
| − | == What's New in Rodin 1.1? ==
| + | UML-B provides a 'UML-like' graphical front end for Event-B. It provides various diagrammatic modelling notations and editors for creating models which are then translated into Event-B for verification. [[UML-B]] works alongside Event-B allowing the modeller to model in normal Event-B but also contribute some aspects of the model via diagrams. |
| | | | |
| − | * [[Rodin_Keyboard | Rodin Keyboard]]
| + | Our [https://www.uml-b.org UML-B] website contains more information about installing UML-B and getting started, as well as our current research and collaborations. |
| − | :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]]
| + | UML-B is a collection of diagrammatic editors for Event-B. The diagrams are used to elaborate the machine and its content with extra model features. The diagrams may either by contained within the machine they contribute to, or can be contained in a separate UML-B model file that is linked to the machine. |
| − | :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: | + | * [[Image:IUMLB.png]] [[Event-B Statemachines| State-machine diagrams]] a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine. |
| − | # 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]] | + | * [[Image:IUMLB.png]] [[Event-B Classdiagrams| Class diagrams]] a class diagram editor which can be used to define data entities and their relationships and to lift behaviour based on data sets. |
| − | :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
| + | ==Lectures== |
| − | :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]] | + | * [[Media:iUML-BClassDiagramsLecture.pdf | UML-B Class-diagrams Lecture]] : Lecture slides on the use of UML-B Class-diagrams |
| − | :The generated event-B files are tagged. These files cannot be modified. | |
| | | | |
| − | * [[Symbol Table | Symbol Table]] | + | * [[Media:iUML-BStatemachinesLecture.pdf | UML-B State-machines Lecture]] : Lecture slides on the use of UML-B State-machines. |
| − | :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
| + | ==Tutorials== |
| − | :Changed color of 'pending' icon for undischarged POs from red to orange/brown.
| |
| − | :Used 'pending_pale' icons for unattempted POs in explorer.
| |
| | | | |
| − | * Modulo | + | * [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of UML-B Class-diagrams. |
| − | :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 ==
| + | * [[iUML-B State-machines Tutorial]] : A tutorial on the use of UML-B State-machines. |
| − | * 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 == | + | ==Guidelines== |
| | | | |
| − | === Rodin Update Site ===
| + | * [[UML-B - Modelling a control system]] : Some guidelines on modelling styles for a control system |
| − | * [[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]]
| |
| | | | |
| | | | |
| − | http://wiki.event-b.org/index.php/Refactoring_Framework
| + | [[Category:User documentation]] |
| − | http://wiki.event-b.org/index.php/Parallel_Composition_using_Event-B
| + | [[Category:UML-B]] |
| − | | + | [[Category:Plugin]] |
| − | === 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]
| |
| − | | |
| − | == 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
| |
| − |
| |
| − | 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
| |
| − | | |
| − | [[Category:Rodin Platform]] | |
State-machine diagrams a hierarchical state-machine diagram editor which can be used to impose sequential ordering to your events. An animator is also provided to visualise the progress of the state-machine.
