imported>Nicolas |
|
| Line 1: |
Line 1: |
| − | {{TOCright}}
| + | Return to [[Rodin Plug-ins]] |
| | | | |
| − | == What's New in Rodin 3.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. |
| | | | |
| − | *'''Copy/Paste''' of components (machines/contexts/…) from Event-B Explorer.
| + | 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. |
| − | *'''Show/Hide''' elements inherited from abstractions in Rodin Editor (abstract invariants/guards/…):
| |
| − | [[File:ShowInherited.png|500px|bottom]] [[File:HideInherited.png|500px|bottom]]
| |
| − | :This noticeably lightens model display in refinements.
| |
| − | *Better '''proving support''' for theories (improved sequent translation for external provers).
| |
| − | *Improved management of '''obsolete proofs''': now, even a proof that contains rules from an invalid reasoner (old version or not installed) is properly displayed in the Proof Skeleton View.
| |
| − | [[File:ProofSkelUncertain.png]]
| |
| | | | |
| − | In this case, an old version of 'simplification rewrites' has been used; running 'Proof Replay on Undischarged POs' will replay the old proof with the current version of the reasoner.
| + | 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. |
| | | | |
| − | === Changes for plug-in developers ===
| + | * [[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. |
| | | | |
| − | Rodin 3.1 is built on top of Eclipse 4.4.1 (Luna).
| + | * [[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. |
| | | | |
| − | == Installing == | + | ==Lectures== |
| | | | |
| − | === Downloading ===
| + | * [[Media:iUML-BClassDiagramsLecture.pdf | iUML-B Class-diagrams Lecture]] : Lecture slides on the use of iUML-B Class-diagrams |
| | | | |
| − | [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.1/ Download Rodin 3.1 now !] | + | * [[Media:iUML-BStatemachinesLecture.pdf | iUML-B State-machines Lecture]] : Lecture slides on the use of iUML-B State-machines. |
| | | | |
| − | === Upgrading from Rodin 3.0 === | + | ==Tutorials== |
| | | | |
| − | Rodin 3.1 is based on Eclipse 4, whereas Rodin 3.0 was based on Eclipse 3.
| + | * [[iUML-B Class-diagrams Tutorial]] : A tutorial on the use of iUML-B Class-diagrams. |
| − | This change makes it impossible to upgrade from 3.0 to 3.1.
| |
| − | Technically speaking, it's because of hidden package dependencies in Eclipse 4 that are not automatically discovered by the update manager.
| |
| − | Thus, Rodin 3.1 must be [[#Downloading|downloaded]].
| |
| | | | |
| − | == Requirements - Compatibility ==
| + | * [[iUML-B State-machines Tutorial]] : A tutorial on the use of iUML-B State-machines. |
| | | | |
| − | * Configurations supported (and for which binaries are provided)
| + | ==Guidelines== |
| − | ** Linux 32-bit
| |
| − | ** Linux 64-bit
| |
| − | ** Windows 32-bit
| |
| − | ** Windows 64-bit
| |
| − | ** Mac OS X 64-bit
| |
| | | | |
| − | * You need to have a Java JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version. To run Rodin 64-bit, you need a 64-bit JRE. | + | * [[iUML-B Modelling a control system]] : Some guidelines on modelling styles for a control system |
| | | | |
| − | * To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionnalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].
| |
| | | | |
| − | * Linux with GTK and old glibc:
| + | [[Category:User documentation]] |
| − | :A crash or display issues may happen:
| + | [[Category:UML-B]] |
| − | :* glibc <= 2.13: SIGSEGV systematic at launch
| + | [[Category:Plugin]] |
| − | :* glibc 2.17: some actions have no effect, like right click actions in the Rodin Editor
| |
| − | :See [https://bugs.eclipse.org/bugs/show_bug.cgi?id=430736].
| |
| − | :Solutions, one of:
| |
| − | :# upgrade glibc >= 2.19
| |
| − | :# export SWT_GTK3=0
| |
| − | :# edit rodin.ini, in the program argument part (before vmargs), add
| |
| − | <pre>
| |
| − | --launcher.GTK_version
| |
| − | 2
| |
| − | </pre>
| |
| − | * Linux 64-bit:
| |
| − | : package 'libc6-amd64:i386' must be installed, in particular in order to run external prover binaries
| |
| − | : depending on the distribution, you could instead need these packages: lib32z1 lib32ncurses5 lib32bz2-1.0
| |
| − | | |
| − | * Windows 64-bit:
| |
| − | : Atelier B provers work more slowly; it can cause ML to not automatically discharge some sequents that it discharges on windows 32-bit, due to its timeout. A workaround is to download a custom profile: [http://sourceforge.net/projects/rodin-b-sharp/files/DefaultAuto_ML800 DefaultAuto_ML800], then Window > Preferences > Event-B > Sequent Prover > Auto/Post Tactic > Profiles (tab) > Import..., point to the downloaded file, 'Select All' profiles (there are 2), OK. Then in 'Auto/Post Tactic' tab, select 'Default Auto Tactic Profile (ML 800)' profile for auto-tactics. It is the same as the 'Default Auto Tactic Profile', except ML has a longer timeout (800 ms). You can of course change this timeout by editing the 'ML (800)' profile.
| |
| − | : We have not noticed this problem for Linux 64-bit, nor for other platforms; however if you do, the same workaround applies.
| |
| − | == External plug-ins ==
| |
| − | {{:Rodin_Platform_3.1.0_External_Plug-ins}}
| |
| − | | |
| − | == Fixed Bugs and Implemented Features ==
| |
| − | | |
| − | Bugs
| |
| − | 255 RODIN crash adding text to note or text box in class diagram
| |
| − | 402 EB-Editor refuses to save
| |
| − | 521 NewPP, PP, ML fail when datatype in type environment
| |
| − | 571 useless missing hypotheses prevent replay
| |
| − | 648 proving does not work with Ubuntu 64bit
| |
| − | 652 Multiple exceptions in EventB Explorer when updating with Teamwork
| |
| − | 706 No WD check building Partial function
| |
| − | 710 Rodin unexpectedly empties content of a machine
| |
| − | 712 Attempt to insert symbol into symbol table more than once
| |
| − | 713 GenMP makes the prover loop
| |
| − | 714 Abusive class cast in PRProofRule
| |
| − | 715 Auto-completion partially broken in Proof Control
| |
| − | 717 Exception when deserializing an old proof (Rodin 2.8)
| |
| − | 718 Bug with "generalized MP" reasoner
| |
| − | 720 No warning when quantifying an event parameter
| |
| − | 721 Denormalized hypothesis not hidden
| |
| − | 722 Incorrect proof skeleton
| |
| − | 723 Replay less powerful than proving UI
| |
| − | 726 Wrong factory after specialization
| |
| − | 727 Type specialization incomplete
| |
| − | 729 clicking on a proof rule for finite leads to "Parse error for expression"
| |
| − | | |
| − | Feature Requests
| |
| − | 98 Copy & Paste
| |
| − | 198 Copy/Paste in Event-B component context menu
| |
| − | 306 Boolean attributes shall not change value at single click
| |
| − | 313 Automatically discharge FINITE with inclusion
| |
| − | 317 Add preference for SMT timeout
| |
| − | 323 Refine PO for variant WD
| |
| − | 326 Simplify PO for anticipated event
| |
| − | 327 Smart focus in wizards
| |
| − | 328 Allow rewriting based on equivalence
| |
| − | 335 Allow ill-formed formulas in specialization
| |
| − | 336 Add query methods to specializations
| |
| − | 337 Sort tactic names alphabetically
| |
| − | | |
| − | == Known Issues ==
| |
| − | See [http://sourceforge.net/p/rodin-b-sharp/bugs known bugs on SourceForge].
| |
| − | | |
| − | * Linux:
| |
| − | : A crash may occur when closing the Welcome page. After restarting Rodin, everything works fine.<br/>
| |
| − | : This is a known Webkit bug: [https://bugs.eclipse.org/bugs/show_bug.cgi?id=400626]
| |
| − | | |
| − | == Disclaimer ==
| |
| − | Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to ensure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the [mailto:rodin-b-sharp-devel@lists.sourceforge.net development mailing list].
| |
| − | | |
| − | == About ==
| |
| − | Rodin Platform with git commit: e1a03f3.<br/>
| |
| − | Developer Release date : 2014-11-28<br/>
| |
| − | User Release date : 2014-12-17.
| |
| − | | |
| − | [[Category:Rodin Platform Release Notes]] | |
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.
