Difference between pages "Developer FAQ" and "Event-B Qualitative Probability User Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Jrloria
 
imported>Son
m
 
Line 1: Line 1:
== How to contribute? ==
+
[[User:Son]] at '''ETH Zurich''' is in charge of the plug-in.
 +
{{TOCright}}
  
=== What are the main community channels? ===
+
== Introduction ==
Beside the [[Mailing lists|mailing lists]], you may want to follow:
+
Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).
* the ''#rodin'' channel on irc://irc.freenode.net
 
* the [http://cia.vc/stats/project/rodin-b-sharp  commit RSS feed] on [http://cia.vc cia.vc],
 
* one of the [https://sourceforge.net/export/rss2_project.php?group_id=108850 sourceforge RSS feed],
 
* the [[Main Page]] of this very site.
 
  
The [[EB:VP|Village Pump]] may also be useful for everything which is more or less wiki related.
 
  
 +
== Installing and Updating ==
 +
The plug-in is available through the main Rodin Update Site under '''Modelling Extension''' category.
  
=== How do I report a bug or a feature request? ===
+
== News ==
You may use sourceforge [http://sourceforge.net/tracker2/?group_id=108850&atid=651669 bug and feature tracker]. Please verify that your bug has not already been reported before submitting it.
+
* 23.11.2011: Version 0.2.1 released for Rodin 2.3.*
  
You may want to submit a partial or full log which you can find in the following file {{file|.metadata/.log}} under the rodin workspace (generally {{file|runtime-Rodin.product/}}).
+
== Technical References ==
  
=== How do I get current source code? ===
+
== Usage ==
 
 
You may get the whole [[Rodin Platform]] and most of associated [[Rodin Plug-ins]] from Subversion on SourceForge using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
 
 
 
To compile the core platform from sources fetched from Subversion, download the latest stable version of Eclipse Classic and install the [http://subclipse.tigris.org/ Subclipse] plug-ins. Then, follow this procedure to fetch the source plug-ins from Subversion:
 
* click {{Menu|File>Import...}}
 
* select {{Menu|SVN>Checkout Projects from SVN}} and click {{Button|Next}}
 
* tick {{Menu|Create a new repository location}} and click {{Button|Next}}
 
* in the Url field, enter <tt><nowiki>https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp</nowiki></tt> and click {{Button|Next}}
 
* after a while, a tree appears.  Select folder <tt>trunk/RodinCore/org.rodinp.releng</tt> in the tree and click {{Button|Finish}}
 
* click {{Menu|File>Import...}}
 
* select {{Menu|Team>Team Project Set}} and click {{Button|Next}}
 
* click {{Button|Browse...}} and select file <tt>rodin-core.psf</tt> in project <tt>org.eclipse.releng</tt>, then click {{Button|Finish}}
 
 
 
After a long while (around a quarter of an hour), all projects of the core Rodin platform have been retrieved from Subversion into your workspace.
 
 
 
You can retrieve the test plug-ins of the core platform in a similar way by repeating the last three steps but selecting file <tt>rodin-tests.psf</tt> instead.
 
 
 
Note: The repository was formerly CVS which is still available read-only.  It is not possible to commit to the CVS repository anymore.  More information is available in the [[Switch from CVS to Subversion]] page.
 
 
 
=== How do I launch the [[Rodin Platform]] from Eclipse? ===
 
 
 
Normally, you should be able to launch the [[Rodin Platform]] by launching Rodin.product in org.rodinp.platform as an Eclipse application.
 
At the time of writing (June 11, 2009), the platform crashes, because not all the required plug-ins are included.
 
 
 
A workaround is to include all workspace and enabled target plug-ins in the run configuration:
 
* go to run -> run configurations
 
* select the newly generated run configuration
 
* go to the tab "plug-ins"
 
* Choose: "launch with: all workspace and enabled target plug-ins in the run configuration"
 
 
 
=== How can I access or create Rodin elements like projects, components or proofs? ===
 
 
 
This section illustrates some of the things you are likely to want to do in your plug-ins if you are extending the Rodin platform.
 
* How do I start a new development ? See the [[Procedure for developing, reviewing and publishing a plugin]].
 
* [[How to read Rodin projects and elements programmatically]].
 
* [[How to create Rodin projects programmatically]].
 
* [[Accessing Proof Obligations|How to access Proof Obligations]].
 
* How to add [[Adding Automatic Inference Reasoners|automatic]] or [[Adding Manual Inference Reasoners|manual]] inference [[reasoners]].
 
* How to add [[Adding Automatic Rewrite Reasoners|automatic]] or [[Adding Manual Rewrite Reasoners|manual]] rewrite [[reasoners]].
 
* [[How to make extensions to Rodin features]].
 
 
 
=== How do I propose a patch? ===
 
You may find useful directions and good practises in the page describing [[How to Submit Patches|how to submit patches]].
 
 
 
== 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 as Target Platform ===
 
From Rodin 1.3 on, source bundles can be included in a [[Using Rodin as Target Platform|target platform]] configuration.
 
 
 
=== 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 to generate ''Rodin'' source plugins for a Target Platform configuration ? ===
 
 
 
For source plugins to work properly in a [[Using Rodin as Target Platform|target platform]] configuration, use the Ant script explained in [[Generating source bundles for inclusion in a target platform configuration|this page]].
 
 
 
=== 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 internal elements. This is done by declaring an <code>attributeRelation</code> element.  Note: In fact, this relationship declares which element '''allows''' to have this 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]].
 
 
 
The detail steps are described in the following page [[Extending the Structure Editor#Adding a New Attribute|Extending the Structure Editor]].
 
 
 
 
 
[[Category:Developer FAQ]]
 

Revision as of 11:14, 23 November 2011

User:Son at ETH Zurich is in charge of the plug-in.

Introduction

Event-B Qualitative Probability plug-in provides supports for reasoning about termination with probability 1 (almost-certain termination).


Installing and Updating

The plug-in is available through the main Rodin Update Site under Modelling Extension category.

News

  • 23.11.2011: Version 0.2.1 released for Rodin 2.3.*

Technical References

Usage