ProB for Rodin: Difference between revisions

No edit summary
(Update Camille update sites (there seems to be just the nightly update site now))
 
(19 intermediate revisions by 3 users not shown)
Line 1: Line 1:
[[Category:Components]]
[[Category:Components]]


ProB for Rodin Landing Page
Currently there are two versions of ProB available for Rodin.


<img src="/ProB/skins/prob/img/prob_cli.png" class="img-rounded" style="box-shadow: 5px 5px 2px #888888;border:1px solid #888888;" />
=== ProB (1) for Rodin ===
The first one is based on the old Java API and supports [http://wiki.event-b.org/index.php/Rodin_Platform_2.8_Release_Notes Rodin 2.8] and [http://wiki.event-b.org/index.php/Rodin_Platform_3.3_Release_Notes Rodin 3.3]. The update site comes built in into Rodin, see [[Tutorial_Rodin_First_Step|the tutorial on installing ProB for Rodin]].
Nightly releases of this versions are also available on the [[Download#Nightly_Build|Download]] page.
 
=== ProB 2.0 for Rodin ===
The second, still experimental, one is based on the new  [[ProB Java API]] (aka ProB 2.0).
Because the UI components provided by the [[ProB Java API]] are based on web technologies, we were able create a simple plugin for the Rodin 3 tool that provides the user with all of the functionality of ProB within Rodin. The plugin uses views with embedded Eclipse SWT browsers to access the user interface components that are shipped with the [[ProB Java API]] library.
Details about nightly releases of this versions is also available on the [[Download#Nightly_Build|Download]] page.
 
=== Multi-Simulation for Rodin based on ProB ===
 
There is now also a [http://users.ecs.soton.ac.uk/vs2/ac.soton.multisim.updatesite/ Multi-Simulation Plug-in] available for Rodin. It enables discrete/continuous co-simulation.
 
=== Other Plug-Ins for Rodin ===
 
==== Prover Evaluation ====
This Plug-in is available at the update site [http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/ http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/] and is capable to evaluate a variety of provers or tactics on a selection of proof obligations.
 
==== Camille ====
We also develop the Camille text-editor for Rodin.
The update site (https://www3.hhu.de/stups/rodin/camille/nightly/) is preconfigured within Rodin.
More information can be found on the [http://wiki.event-b.org/index.php/Camille_Editor Camille site at event-b.org].

Latest revision as of 14:48, 4 February 2021


Currently there are two versions of ProB available for Rodin.

ProB (1) for Rodin

The first one is based on the old Java API and supports Rodin 2.8 and Rodin 3.3. The update site comes built in into Rodin, see the tutorial on installing ProB for Rodin. Nightly releases of this versions are also available on the Download page.

ProB 2.0 for Rodin

The second, still experimental, one is based on the new ProB Java API (aka ProB 2.0). Because the UI components provided by the ProB Java API are based on web technologies, we were able create a simple plugin for the Rodin 3 tool that provides the user with all of the functionality of ProB within Rodin. The plugin uses views with embedded Eclipse SWT browsers to access the user interface components that are shipped with the ProB Java API library. Details about nightly releases of this versions is also available on the Download page.

Multi-Simulation for Rodin based on ProB

There is now also a Multi-Simulation Plug-in available for Rodin. It enables discrete/continuous co-simulation.

Other Plug-Ins for Rodin

Prover Evaluation

This Plug-in is available at the update site http://nightly.cobra.cs.uni-duesseldorf.de/rodin_provereval/ and is capable to evaluate a variety of provers or tactics on a selection of proof obligations.

Camille

We also develop the Camille text-editor for Rodin. The update site (https://www3.hhu.de/stups/rodin/camille/nightly/) is preconfigured within Rodin. More information can be found on the Camille site at event-b.org.