Tutorial Rodin Exporting: Difference between revisions
Created page with 'Category:User Manual == Introduction == Many features of ProB are currently only available in the ProB Tcl/Tk or the [[Using_the_Command-Line_Version_of_ProB|probcli comma…' |
No edit summary |
||
| Line 9: | Line 9: | ||
== Exporting for ProB Classic == | == 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": | 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": | ||
[[file:ProBRodinExport.png|center||600px]] | [[file:ProBRodinExport.png|center||600px]] | ||
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 [[Using_the_Command-Line_Version_of_ProB|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. Again, all features applicable to B models also work with Event-B models. | |||
Revision as of 07:23, 25 February 2012
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":
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. Again, all features applicable to B models also work with Event-B models.