Tutorial Rodin Exporting

Revision as of 07:27, 25 February 2012 by Michael Leuschel (talk | contribs)


Introduction

Many features of ProB are currently only available in the 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":

ProBRodinExport.png


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.


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.

ProBRodinLoadedInTclTk.png