|
|
| (12 intermediate revisions by 4 users not shown) |
| Line 1: |
Line 1: |
| == General ==
| | [http://handbook.event-b.org/current/html/faq.html Rodin Handbook (FAQ)] |
| === What is event-B? ===
| |
| '''Event-B''' is a formal method for system-level modelling and analysis. Key features of event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. More details are available in http://www.event-b.org/
| |
| | |
| === What is the difference between event-B and the B method? ===
| |
| | |
| Event-B is derived from the [http://en.wikipedia.org/wiki/B-Method B method]. Both notations have the same [http://en.wikipedia.org/wiki/Jean-Raymond_Abrial inventor], and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose. The B method is devoted to the development of ''correct by construction'' software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation).
| |
| | |
| Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different).
| |
| | |
| === What is Rodin? ===
| |
| The '''Rodin Platform''' is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins.
| |
| | |
| === Where does the ''Rodin'' name come from? ===
| |
| | |
| The Rodin platform was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” . Rodin is also the name of a famous French [http://en.wikipedia.org/wiki/Auguste_Rodin sculptor], one of his most famous work being the [http://en.wikipedia.org/wiki/The_Thinker Thinker].
| |
| | |
| == General Tool Usage? ==
| |
| | |
| === How do I install external plug-ins without using Eclipse Update Manager? ===
| |
| Although it is preferred to install additional plug-ins into the Rodin platform using the Update Manager of Eclipse, this might not always be practical. In this case, a manner to install these plug-ins is to emulate either manually or using ad-hoc scripts the operations normally performed by the Update Manager.
| |
| | |
| This manual installation of plug-ins is described in ''[[Installing external plug-ins manually]]''.
| |
| | |
| === The builder takes too long ===
| |
| Generally, the builder spends most of its time attempting to prove POs. There are basically two ways to get it out of the way:
| |
| * the first one is to disable the automated prover in the Preferences panel.
| |
| * the second one is to mark some PO as reviewed when you don't want the auto-prover to attempt them anymore.
| |
| Note that if you disable the automated prover, you always can run it later on some files by using the contextual menu in the event-B Explorer.
| |
| | |
| To disable the automated prover, open Rodin <tt>Preferences</tt> (menu {{menu|Window > Preferences...}}). In the tree in the left-hand panel, select {{menu|Event-B > Sequent Prover > Auto-tactic}}. Then, in the right-hand panel ensure that the checkbox labelled <tt>Enable auto-tactic for proving</tt> is disabled.
| |
| | |
| To review a proof obligation, just open it in the interactive prover, then click on the ''review'' button (this is a round blue button with a ''R'' in the proof control toolbar). The proof obligation should now labelled with the same icon in the event-B explorer.
| |
| | |
| ===What are the ASCII shortcuts for mathematical operators===
| |
| | |
| The ASCII shortcuts that can be used for entering mathematical operators are described in the help of the event-B keyboard plug-in. In the help system, this page has the following path {{menu|Event-B Keyboard User Guide > Getting Started > Special Combos}}.
| |
| | |
| This page is also available in the dynamic help system. The advantage of using dynamic help is that it allows to display the help page side-by-side with the other views and editors. To start the dynamic help, click {{menu|Help > Dynamic Help}}, then click {{menu|All Topics}} and select the page in the tree.
| |
| | |
| | |
| ===Rodin (and eclipse) doesn't take into account the MOZILLA_FIVE_HOME environment variable===
| |
| You have to add a properties by appending the following code to your {{file|eclipse/eclipse.ini}} or {{file|rodin/rodin.ini}} file:
| |
| -Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner/xulrunner-xxx
| |
| | |
| == Modeling ==
| |
| === Witness for {{Ident|Xyz}} missing. Default witness generated ===
| |
| A parameter as disappeared during a refinement. If this is intentional, you have to add a [[Witnesses (Modelling Language)|witness]] telling how the abstract parameter is refined.
| |
| | |
| === Identifier {{ident|Xyz}} should not occur free in a witness ===
| |
| You refer to {{ident|Xyz}} in a witness predicate where {{ident|Xyz}} is a disappearing abstract variable or parameter which is not set as the witness label.
| |
| | |
| === In {{event|INITIALISATION}}, I get ''Witness {{ident|Xyz}} must be a disappearing abstract variable or parameter'' ===
| |
| The witness is for the after value of the abstract variable, hence you should use the primed variable. The witness label should be {{ident|Xyz'}}, and the predicate should refer to {{ident|Xyz'}} too.
| |
| | |
| === I've added a witness for {{ident|Xyz}} but it keeps saying ''"Identifier {{ident|Xyz}} has not been defined"'' ===
| |
| As specified in the [[Witnesses (Modelling Language)|modelling language manual]], the witness must be labelled by the name {{Ident|Xyz}} of the concrete variable being concerned.
| |
| | |
| === What are type expressions in Event-B? ===
| |
| The type expressions are defined recursively as follows:
| |
| | |
| * Built-in types: ℤ, BOOL (Note that ℕ is NOT a type expressions).
| |
| | |
| * Any carrier set is a type expression.
| |
| | |
| * If <math>T</math> is a type expression then <math>ℙ(T)</math> is a type expression.
| |
| | |
| * If <math>S</math> and <math>T</math> are type expressions then <math>S × T</math> is a type expression.
| |
| | |
| == Proving ==
| |
| | |
| === How can I do a Proof by Induction? ===
| |
| [[Induction proof|This page about proof by induction]] will give you some starting tips.
| |
| | |
| === Labels of proof tree nodes explained ===
| |
| * {{ident|ah}} means ''add hypothesis'',
| |
| * {{ident|eh}} means rewrite with ''equality from hypothesis'' from left to right,
| |
| * {{ident|he}} means rewrite with ''equality from hypothesis'' from right to left,
| |
| * {{ident|rv}} tell us that this goal as been manually [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Control_Window|reviewed]],
| |
| * {{ident|sl/ds}} means ''selection/deselection'',
| |
| * {{ident|PP}} means ''discharged by the predicate prover''
| |
| * {{ident|ML}} means ''discharged by the mono lemma prover''
| |
| | |
| == How to contribute? ==
| |
| See the [[How_To_Contribute|How to contribute]] page.
| |
| | |
| == Developer FAQ ==
| |
| === How can I get the sources of the Rodin platform? ===
| |
| | |
| There are two options for getting the sources of the Rodin platform:
| |
| # The safe option is to download the source bundle which is made available with each platform release. This ensures that you will get a consistent set of source files, albeit maybe a bit outdated.
| |
| # The other option is to fetch the sources from Subversion, which allows to get their latest version. The Rodin developers strive for keeping theses sources usable (i.e. they should always compile and pass unit tests), but breakage can happen.
| |
| | |
| === Installing the source bundle in Eclipse ===
| |
| | |
| To install the bundled sources, you first have to download the bundle from SourceForge. It takes the form of a ZIP file named <tt>rodin-VERSION-sources.zip</tt>. Then, in Eclipse, click {{Menu|File > Import...}} In the ''Import'' popup, select {{Menu|General > Existing Projects into Workspace}} and click {{button|Next}}. Then tick {{Menu|Select archive file}} and enter the path to the source bundle you have just downloaded. Ensure that all projects are ticked and click {{button|Finish}}. Your workspace gets populated with the source projects of the Rodin platform and Eclipse starts building.
| |
| | |
| === Installing the sources from Subversion in Eclipse ===
| |
| | |
| To install the sources from Subversion, in Eclipse click {{Menu|File > Import...}}, then select {{Menu|SVN > Checkout Projects from SVN}} in the ''Import'' popup and click {{button|Next}} twice. In the ''Url'' textbox, enter <tt>https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp</tt> and click {{button|Next}}. In the tree displaying the subversion repository, select path <tt>trunk/RodinCore/org.rodinp.releng</tt> and click {{button|Finish}}. Your workspace now contains the project <tt>org.rodinp.releng</tt>.
| |
| | |
| To install the other source projects, click again {{Menu|File > Import...}}, but this time select {{Menu|Team > Team Project Set}} and click {{button|Next}}. When asked for a ''File name'', enter the path to file <tt>org.rodinp.releng/rodin-core.psf</tt> in your workspace and click {{button|Finish}}. Eclipse then fetches the other source projects of the Rodin platform into your workspace (this can take some time).
| |
| | |
| === Using Rodin-SVN from Eclipse consumes too much memory ===
| |
| Running the Rodin platform from Eclipse can consume a lot of RAM and become impractical on a small machine. If you fall in this case, you can [[#How_do_I_generate_a_Rodin_product_from_SVN.3F|generate a product]] and use it as if it was a normal release.
| |
| | |
| === How do I generate a ''Rodin'' product from sources? ===
| |
| In the project ''org.rodinp.platform'', right-click on ''Rodin.platform'' and select {{menu|export}}. Choose {{menu|Plug-in Development > Eclipse product}} and click on {{button|Next}} type <tt>Rodin</tt> for the ''Root directory'', and choose the ''Destination directory''. Then click on {{button|Finish}}.
| |
| | |
| === How to build ''Rodin'' headless? ===
| |
| When releasing a new version of the Rodin platform, the Rodin team builds the platform headless (i.e. using batch scripts rather than Eclipse GUI). The process used for that is described in [[Building Rodin Headless]]. Alternatively, the Rodin team has also set up a [[CruiseControl]] server for checking that builds do not break.
| |
| | |
| === How do I collect debug information from the Rodin platform? ===
| |
| You may see the log in the console by appending <tt>-consoleLog</tt> to the rodin executable: <code>rodin -consoleLog</code>
| |
| | |
| You may add specific debug informations by setting specific options: <code>rodin --debug options.file -consoleLog</code> where {{file|options.file}} contains something like:
| |
| <pre>
| |
| org.pluginname/debug = true
| |
| org.pluginname/debug/optionaldebug = true
| |
| </pre>
| |
| where'' optionaldebug'' may be found in the {{file|org.pluginname/.options}} file in the [http://rodin-b-sharp.cvs.sourceforge.net/rodin-b-sharp/ rodin source repository].
| |
| | |
| === How do I submit a patch? ===
| |
| Good practises for patch submission are described [[How to Submit Patches|here]].
| |
| | |
| === How do I track memory leaks? ===
| |
| If you suspect that some memory isn't freed, you may find some useful directions on how to track memory leaks [[Tracking Memory Leaks|here]].
| |
| | |
| === How do I report a bug. ===
| |
| See [[How_To_Contribute#How_do_I_report_a_bug_or_a_feature_request.3F|the ''How to contribute'' page]].
| |
| | |
| === How do I save the models ? ===
| |
| After the separation between a file ({{class|IRodinFile}}) and its root (a {{class|IInternalElement}}), that occurred in version 0.9.2, model saving is no more achievable through internal elements. Instead, you have to save the {{class|IRodinFile}}.
| |
| | |
| IInternalElement element = ...
| |
| element.getRodinFile().save(...);
| |
| | |
| | |
| === How do I add a new attribute to existing elements (e.g. Event-B event)? ===
| |
| You need to extend the following extension point <code>org.rodinp.core.attributeTypes</code> to declare the new attribute.
| |
| | |
| Note: There is no constraint on which element type this attribute type associated with. In principle, any attribute type can be attached to the any internal element type.
| |
| | |
| The detail steps are described in the following page [[Extending the Rodin Database#Adding a New Attribute|Extending the Rodin Database]].
| |
| | |
| === How do I extend the Event-B structure editor (the Edit Tab of the Event-B editor) for editing an attribute (which I added to the Rodin DB as described [[#How do I add a new attribute to existing elements (e.g. Event-B event)?| here]])? ===
| |
| | |
| You need to extend the following extension point <code>org.eventb.ui.editorItems</code> to declare the two different elements:
| |
| | |
| * How the attribute is going to be displayed/edited. This is done by declaring one of the following elements: <code>textAttribute</code>, <code>choiceAttribute</code> or <code>toggleAttribute</code>.
| |
| | |
| * The relationship between the attribute and an internal element. This is done by declaring an <code>attributeRelation</code> element. Note: In fact, this relationship declares which element '''allows''' to have the attribute, which is not something enforce when the attribute is added as described [[#How do I add a new attribute to existing elements (e.g. Event-B event)?| here]].
| |
| | |
| [[Category:User FAQ]]
| |
| [[Category:Developer FAQ]]
| |
