imported>Mathieu |
imported>Tommy |
| Line 1: |
Line 1: |
| − | == General == | + | {{Navigation|Next= [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]]}} |
| − | === 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 Rodin? ===
| + | '''Tutorial for the extension of the Rodin platform by plugin addition''' |
| − | 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? ===
| + | This tutorial is problem solving oriented. |
| | + | In a first part, we will focus on Rodin extensions to develop a plugin for Probabilistic Termination and Qualitative Reasoning. In a second part, we will study specific problem cases and extend Rodin to solve them. More details can be found in the [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]]. |
| | | | |
| − | == General Tool Usage? == | + | ==Outline== |
| | + | * {{topic|Introduction_(How_to_extend_Rodin_Tutorial)|Introduction}} |
| | + | ''First part'' (Probabilistic Termination and Qualitative Reasoning Plugin): |
| | + | * {{topic|Creating_a_new_plug-in_using_eclipse_(How_to_extend_Rodin_Tutorial)|1 Creating our plug-in}} |
| | + | * {{topic|Extending_the_Rodin_database_(How_to_extend_Rodin_Tutorial)|2 Contributing new elements in the Rodin database}} |
| | + | * {{topic|Extend_Rodin_Structured_Editor_(How_to_extend_Rodin_Tutorial)|3 Adding support for new elements in the Rodin structured editor}} |
| | + | * {{topic|Extend_Rodin_EventB_Explorer(How_to_extend_Rodin_Tutorial)|4 Adding elements to the Event-B explorer}} |
| | + | * {{topic|Extending_Rodin_Pretty Print Page(How_to_extend_Rodin_Tutorial)|5 Display added elements in the Pretty Print Page}} |
| | + | * {{topic|Providing_help_for_your_plug-in_(How_to_extend_Rodin_Tutorial)|6 Providing help}} |
| | + | * {{topic|Extending_the_Static_Checker(How_to_extend_Rodin_Tutorial)|7 Extending the Static Checker}} |
| | + | * {{topic|Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial)|8 Extending the Proof Obligation Generator}} |
| | | | |
| − | === How do I install external plug-ins without using Eclipse Update Manager? ===
| + | ''Second part'' (Various problem solvings): |
| − | 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]]''.
| + | ==Projects== |
| | + | The archives of the projects built in this tutorial are available here: |
| | + | // '''FIXME. Add the links to the .zip files here.''' |
| | + | * [http://sourceforge.net/projects/rodin-b-sharp/files/Doc_%20Tutorial/2.0/Help.zip/download<tt>Help.zip</tt>], which will be needed in section XXX. |
| | | | |
| − | === The builder takes too long === | + | {{Navigation|Next= [[Introduction_(How_to_extend_Rodin_Tutorial)|Introduction]]}} |
| − | 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.
| + | [[Category:Developer documentation|*Index]] |
| − | | + | [[Category:Rodin Platform|*Index]] |
| − | 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.
| + | [[Category:Tutorial|*Index]] |
| − | | |
| − | ===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.
| |
| − | | |
| − | == Modeling and Proving==
| |
| − | === 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'' ===
| |
| − | You should mark the variable as an ''after variable'' by using a tick. 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.
| |
| − | | |
| − | === How can I do a Proof by Induction? ===
| |
| − | [[Induction proof]] will give you some tips about it.
| |
| − | | |
| − | === 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'' | |
| − | | |
| − | == Developer FAQ ==
| |
| − | === Using Rodin-CVS from eclipse consumes too much memory ===
| |
| − | You can [[#How do I generate a Rodin product from CVS|generate a product]] and use it as if it was a normal release.
| |
| − | | |
| − | === How do I generate a ''Rodin'' product from CVS? ===
| |
| − | 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 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]].
| |
| − | | |
| − | [[Category:User FAQ]] | |
| − | [[Category:Developer FAQ]] | |
