Rodin: Installation and Basic Tips

Install Rodin

• 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.7, 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.

If everything fails

• Check the mailing lists at https://sourceforge.net/p/rodin-b-sharp/mailman/
• I have left a .vmdk virtual machine with a minimal Ubuntu installation and Rodin 3.6 with the Atelier B provers installed.
  • Size: 10 GB.
  • User: rodin; password: rodin.
  • You can probably give it at least 3 threads so that the user interface and Rodin can work simultaneously. You may want to increase the RAM available to the virtual machine (e.g., 2GB) to avoid it paging, which is likely to be slow in a virtual machine.
  • This should work in VirtualBox, VMWare, and probably Parallels. I only have direct experience with the first one.
  • It should be possible to share folders between the host and the guest operating systems, which makes it easier to exchange files. Check the virtual machine software documentation.

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).