Tutorial Rodin Exporting - Revision history

David Geleßus: Update download page link

2021-02-04T14:36:22Z

Update download page link

← Older revision		Revision as of 14:36, 4 February 2021
Line 42:		Line 42:
	[[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).		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 [[Download\|ProB download site]] (we usually recommend the nightly-build version).


	[[file:ProBRodinClassicPreference.png\|center\|\|400px]]		[[file:ProBRodinClassicPreference.png\|center\|\|400px]]

Michael Leuschel: /* Loading an Event-B Project into ProB classic */

2012-02-25T07:55:47Z

Loading an Event-B Project into ProB classic

← Older revision		Revision as of 07:55, 25 February 2012
Line 21:		Line 21:
	probcli b_1_mch.eventb -mc 100000		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.		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.

			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, <tt>-p MAXINT 2147483647</tt>). In ProB Tcl/Tk the preferences are managed from the "Preferences" menu (and current values are saved in a <tt>ProB_Preferences.pl</tt> file).
			The ProB for Rodin preferences are currently <b>not</b> exported into the ".eventb" file.


Line 31:		Line 34:

	[[file:ProBRodinLoadedInTclTk.png\|center\|\|400px]]		[[file:ProBRodinLoadedInTclTk.png\|center\|\|400px]]


	== Starting up ProB Classic Directly ==		== Starting up ProB Classic Directly ==

Michael Leuschel at 07:33, 25 February 2012

2012-02-25T07:33:41Z

← Older revision		Revision as of 07:33, 25 February 2012
Line 4:		Line 4:
	== Introduction ==		== Introduction ==

	Many features of ProB are currently only available in ~~the~~ ProB Tcl/Tk or the [[Using_the_Command-Line_Version_of_ProB\|probcli command-line version]].		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 ~~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 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 ~~Classic~~ ==		== 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 ~~Classic~~":		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]]

Michael Leuschel at 07:29, 25 February 2012

2012-02-25T07:29:25Z

← Older revision		Revision as of 07:29, 25 February 2012
Line 31:		Line 31:

	[[file:ProBRodinLoadedInTclTk.png\|center\|\|400px]]		[[file:ProBRodinLoadedInTclTk.png\|center\|\|400px]]


			== 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":

			[[file:ProBRodinExport.png\|center\|\|400px]]

Michael Leuschel at 07:27, 25 February 2012

2012-02-25T07:27:17Z

← Older revision		Revision as of 07:27, 25 February 2012
Line 11:		Line 11:
	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":

	[[file:ProBRodinExport.png\|center\|\|~~600px~~]]		[[file:ProBRodinExport.png\|center\|\|400px]]


Line 23:		Line 23:


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

			[[file:ProBRodinLoadedInTclTk.png\|center\|\|400px]]

Michael Leuschel at 07:23, 25 February 2012

2012-02-25T07:23:26Z

@@ Line 9: / Line 9: @@
 == 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]]

Michael Leuschel: 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…'

2012-02-25T07:15:43Z

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…'

New page

[[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 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":

[[file:ProBRodinExport.png|center||600px]]