Tutorial Rodin Exporting: Difference between revisions
No edit summary |
No edit summary |
||
| Line 4: | Line 4: | ||
== Introduction == | == Introduction == | ||
Many features of ProB are currently only available in | Many features of ProB are currently only available in ProB Tcl/Tk or the [[Using_the_Command-Line_Version_of_ProB|probcli command-line version]]. | ||
Luckily you can export Rodin models for use with those tools. Below we explain how. | Luckily you can export Rodin models for use with those tools. Below we explain how. | ||
== Exporting for ProB | == 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": | 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": | ||
| Line 16: | Line 16: | ||
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). | 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 | == 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): | 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): | ||
| Line 36: | Line 36: | ||
You can also start up ProB Classic (aka ProB Tcl/Tk) directly, without first generating an ".eventb" file. | 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 | 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": | ||
[[file:ProBRodinExport.png|center||400px]] | [[file:ProBRodinExport.png|center||400px]] | ||
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 [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Download ProB download site] (we usually recommend the nightly-build version). | |||
[[file:ProBRodinClassicPreference.png|center||400px]] | |||
Revision as of 07:33, 25 February 2012
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.
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).
