Tutorial Rodin Exporting: Difference between revisions

Introduction

Many features of ProB are currently only available in ProB Tcl/Tk or the probcli command-line version. Luckily you can export Rodin models for use with those tools. Below we explain how.

Exporting for ProB classic

Start by right clicking (control Click on the Mac) on the machine or context in the "Event-B Explorer" view you wish to export and select "ProB Classic.../Export for use in ProB Classic":

Now a "File Save" dialog will pop up. Choose a location and name (the default one will do) for the file. The file should have the extension ".eventb" (as suggested by default).

Loading an Event-B Project into ProB classic

You can now use the ".eventb" file directly for probcli. For example, the following command will perform standard model checking on the file (supposing it was named b_1_mch.eventb):

 probcli b_1_mch.eventb -mc 100000

All options described in the manual page for probcli for B models are also applicable to Event-B models.

Warning: the preferences for ProB are managed in different ways by the different tools. For the command-line version, preference values have to be passed explicitly using the -p switch (e.g, -p MAXINT 2147483647). In ProB Tcl/Tk the preferences are managed from the "Preferences" menu (and current values are saved in a ProB_Preferences.pl file). The ProB for Rodin preferences are currently not exported into the ".eventb" file.

You can also load the Event-B models into the ProB Tcl/Tk version. Simply choose the command "Open..." in the "File" menu and select the file you have exported above. (You may have to change the filename filter pop-up menu at the bottom of the "Open..." dialog to also show .eventb files.)

Again, all features applicable to B models also work with Event-B models. The source frame of ProB will show an ASCII rendering of the Event-B models. Note that all contexts and ancestor machines are merged into a single ".eventb" project file.

Starting up ProB Classic Directly

You can also start up ProB Classic (aka ProB Tcl/Tk) directly, without first generating an ".eventb" file. For this, start by right clicking (control Click on the Mac) on the machine or context in the "Event-B Explorer" view you wish to validate and select "ProB Classic.../Open in ProB classic":

For this to work, you first need to open the ProB Classic preferences and then click on "Browse" to locate your installation of ProB Classic (which you can obtain from the ProB download site (we usually recommend the nightly-build version).