Rodin: Installation and Basic Tips

Install Rodin

A tool to develop Event B models and discharge proof obligations using
semi-automatic theorem provers.

I have tested the installation of Rodin 3.9 in Linux, but not in Windows or Mac. If you (try to) install it in a Windows or Mac machine and you experience any errors and/or find workarounds, please share your experience with your classmates through the class mailing list.

  • Tool site with instructions: http://www.event-b.org/install.html (but you can probably follow the points below).
  • Download latest version from https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/
    • Enter the directory of the last stable version (3.9, at the time of writing).
    • Pay attention to the instructions at the bottom of that page.
    • Download the version corresponding to your OS (ignore org.rodinp.dev-*.zip files).
    • Uncompress, follow instructions.
  • Start Rodin!
  • Go to Help → Install New Software → choose Atelier B Provers from the Work with drop-down menu → select it → click Next. Follow instructions.

If Rodin Does Not Start. . .

Make sure to have Java 1.8 JDK installed (I believe Java JRE is not enough). Oracle Java may be necessary.

Mac Os X
  • Change attributes of rodin.app (see instructions in download page).
  • New M1 , M2, M3 Macs: runtime translation seems to work.
Windows
  • I can offer little help here.
(Ubuntu) Linux
  • Rodin 3.9 works out of the box in Ubuntu 24.10.

If everything fails

Using Rodin

  • Using the theorem prover will be your next task.
  • To do so: ensure first your installation is working!

Please import the “integer division” example. Refer to the “Exporting and Importing Projects” (later). Click on the project, expand the ID_M0 component, make sure the “Proof Obligations” section has a green icon at its left.

Editing models

  • Editing models: right-click on keywords for a drop-down menu with
    elements to add.
  • Useful keybindings:
    • Alt-G: add children element e.g., if in THEN, add action.
    • Alt-T: add sibling element e.g., if finished with one guard, add another guard.
    • Ctrl-S: save model, run auto-provers, update proof status.
    • Return in an editable section: turn edition on an off.
    • TAB: go to the next editable section.
    • Help → Show Active Keybindings: more keybindings.
    • Help → Help Contents → Rodin Keyboard User Guide → Introduction: list of special symbols and how to insert them using the keyboard. There is also a Symbols tab on the bottom right pane that shows symbols that can be clicked to insert them. However, using the keyboard is much faster.
  • “Explorer window”: expand project, machine / context, “Proof Obligations” to check undischarged proofs:
    • Double click on undischarged proof:
    • Switch to “Prover view” in icons under menu: (or in Window → Perspective → Open Perspective in some versions of Rodin).
    • Switch back to “Event-B view” to continue editing.

Exporting and Importing Projects


Exporting (full reference at https://www3.hhu.de/stups/handbook/rodin/current/html/sect0032.html):

  • Select project, right-click and select Export.
  • Select General → Archive File, click Next.
  • Choose path and file name; click Finish.


Importing (full reference at https://www3.hhu.de/stups/handbook/rodin/current/html/sect0033.html):

  • File → Import from menu.
  • Select General → Existing Projects into Workspace, click Next.
  • Choose Select archive file, then Browse.
  • Find zip file and click Finish.

Note: importing will fail if project names clash.
You can right-click and Rename before exporting (to save under a different name), or before importing (to change name of target project).