Installation - Revision history

David Geleßus: Fix some obviously outdated information

2026-03-05T17:36:53Z

Fix some obviously outdated information

David Geleßus: Moved category to bottom

2022-03-24T08:21:12Z

Moved category to bottom

← Older revision		Revision as of 08:21, 24 March 2022
Line 1:		Line 1:
	~~[[Category:User Manual]]~~__NOTOC__		__NOTOC__
	== Which version should I use? ==		== Which version should I use? ==

Line 38:		Line 38:
	Note: you can use the "Pick" button to locate the dot program and the dot viewer.		Note: you can use the "Pick" button to locate the dot program and the dot viewer.
	See more information about the [[Graphical Viewer\|Graphical Viewer here]].		See more information about the [[Graphical Viewer\|Graphical Viewer here]].

			[[Category:User Manual]]

David Geleßus: Removed list of ProB versions that mostly just duplicates the homepage

2022-03-24T08:20:53Z

Removed list of ProB versions that mostly just duplicates the homepage

← Older revision		Revision as of 08:20, 24 March 2022
Line 1:		Line 1:
	[[Category:User Manual]]__NOTOC__		[[Category:User Manual]]__NOTOC__
	== ~~What are the available versions~~? ==		== Which version should I use? ==

	* The standalone Tcl/Tk Version of ProB (ProB Tcl/Tk)
	* The standalone command-line version of ProB ([[Using_the_Command-Line_Version_of_ProB\|probcli]])
	* The [[Tutorial_Rodin_First_Step\|ProB Plugin for Rodin/Eclipse]]
	* The online [[ProB_Logic_Calculator\|ProB Logic Calculator]]

	Both the standalone ProB Tcl/Tk and probcli can be downloaded together (within a Zip archive or tarball together with examples) from our [[Download\|Downloads page]]. The online [[ProB_Logic_Calculator\|ProB Logic Calculator]] requires no installation; just type in predicates and expressions into the web page.

	~~There is also a~~ [~~http://www.tools.clearsy.com/index.php5?title=ProB_etool_generation plugin for Atelier B], in order to use the standalone ProB Tcl/Tk Version on~~ [~~http://www.atelierb.eu/ Atelier B] projects. It comes bundled with~~ ProB ~~Tcl/Tk.~~		See [[The ProB Animator and Model Checker#Versions of ProB\|our homepage]] for an overview of the available versions of ProB.
			All ProB tools can be downloaded from our [[Download]] page.
	ProB ~~is used within a few other tools, such as [http://wiki.event-b.org/index.php/IUML-B iUML-B~~] ~~or [http://safecap.sourceforge.net/index.shtml SafeCap~~].

	~~We are also developing a new Java-based API called [[ProB_2.0_Tutorial\|~~ProB ~~2.0]], which is a high-level wrapper for the command-line version~~ [[~~Using_the_Command-Line_Version_of_ProB\|probcli~~]].

	~~== Which version should I use? ==~~

	The standalone version Tcl/Tk of ProB contains a richer set of features than the Rodin version and also works on other formalisms than Event-B (e.g., classical B, Z, CSP, B\|\|CSP, Promela, ...). If you want to do animation and model checking of Event-B models, the Rodin version might be enough. The Rodin version contains a translation tool from Rodin into Event-B package files that can be used within the standalone version of ProB.		The standalone version Tcl/Tk of ProB contains a richer set of features than the Rodin version and also works on other formalisms than Event-B (e.g., classical B, Z, CSP, B\|\|CSP, Promela, ...). If you want to do animation and model checking of Event-B models, the Rodin version might be enough. The Rodin version contains a translation tool from Rodin into Event-B package files that can be used within the standalone version of ProB.

Michael Leuschel at 07:51, 7 July 2021

2021-07-07T07:51:10Z

← Older revision		Revision as of 07:51, 7 July 2021
Line 50:		Line 50:
	Note: you can use the "Pick" button to locate the dot program and the dot viewer.		Note: you can use the "Pick" button to locate the dot program and the dot viewer.
	See more information about the [[Graphical Viewer\|Graphical Viewer here]].		See more information about the [[Graphical Viewer\|Graphical Viewer here]].

	~~== Installation Instruction for ProB (Rodin Plugin) ==~~

	~~The following movie shows how to install the ProB Rodin Plugin.~~

	~~<swf width="800" height="600">http://www.stups.uni-duesseldorf.de/ProB/Install.swf</swf>~~

Michael Leuschel: /* Installation Instruction for ProB (Standalone) */

2018-07-09T12:40:50Z

Installation Instruction for ProB (Standalone)

← Older revision		Revision as of 12:40, 9 July 2018
Line 27:		Line 27:
	StartProB.sh tcl		StartProB.sh tcl
	On Windows, you will also have a subfolder called "Microsoft.VC80.CRT" containing the DLLs for the C runtime. Also, the binary is called "ProBWin" and not "prob".		On Windows, you will also have a subfolder called "Microsoft.VC80.CRT" containing the DLLs for the C runtime. Also, the binary is called "ProBWin" and not "prob".
	* Be sure that you have Tcl/Tk installed (see, e.g., http://www.tcl.tk/software/tcltk/). With the latest version of ProB, you have to install Tcl/Tk version 8.~~4 (for some versions of ProB even 8~~.~~5)!~~ For ~~Windows~~ you can find a correct version of Tcl/Tk ~~at http~~://downloads.activestate.com/ActiveTcl/~~Windows~~/~~8.4.19/ . The Mac version needs Tcl/Tk~~ 8.5 ~~or higher (http://www~~.~~tcl~~.~~tk/software/tcltk/8.5.html~~/).		* Be sure that you have Tcl/Tk installed (see, e.g., http://www.tcl.tk/software/tcltk/).
	* To load your own B machines you also need Java runtime ~~installed (http://java.sun.com/j2se/index.jsp~~ or ~~directly to http://java.sun.com/javase/downloads/index.jsp to download the standard edition 5.0; on Mac and Linux Java is probably already installed)~~.		With the latest version of ProB, you
			have to install Tcl/Tk version 8.5.
			For example, you can find a correct version of Tcl/Tk athttp://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ .
			* To load your own B machines you also need Java 7 or newer runtime or better JDK.
	* Note: you can skip this step if you do not wish to use the visualization commands. Install the "dot" program and "dotty" viewer from AT&T's Graphviz package (http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/). By default, ProB will open the "dotty" program to visualize the graphs, but postscript viewers (such as gv) are also supported. So, you do not need to install dotty if you don't want to; but it is probably easiest to install the entire Graphviz package.		* Note: you can skip this step if you do not wish to use the visualization commands. Install the "dot" program and "dotty" viewer from AT&T's Graphviz package (http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/). By default, ProB will open the "dotty" program to visualize the graphs, but postscript viewers (such as gv) are also supported. So, you do not need to install dotty if you don't want to; but it is probably easiest to install the entire Graphviz package.
	* Change to the ProB directory and then start up prob. In Windows you can simply double-click on the ProBWin Application. On Mac OS X you may have to type 'limit data unlimited' (in tcsh) or 'ulimit -d unlimited' (in bash) before launching ProB using the Terminal Application. The distribution contains a script StartProB.sh which does this for you (note you may have to do chmod u+x StartProB.sh before launching it from the command-line).		* Change to the ProB directory and then start up prob. In Windows you can simply double-click on the ProBWin Application. On Mac OS X you may have to type 'limit data unlimited' (in tcsh) or 'ulimit -d unlimited' (in bash) before launching ProB using the Terminal Application. The distribution contains a script StartProB.sh which does this for you (note you may have to do chmod u+x StartProB.sh before launching it from the command-line).

Michael Leuschel: /* Checklist/Troubleshooting */

2018-07-09T12:38:34Z

Checklist/Troubleshooting

← Older revision		Revision as of 12:38, 9 July 2018
Line 35:		Line 35:
	=== Checklist/Troubleshooting ===		=== Checklist/Troubleshooting ===

	* Java: be sure to have Java ~~1.5~~ or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.		* Java: be sure to have Java 7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.

	* Tcl/Tk: be sure to have a suitable version of TclTk installed. In general you should install ~~at least 8.4.14 in general and~~ at least 8.5 ~~on the Mac~~. You also need the 64 bit version of Tcl/Tk for 64 bit versions of ProB.		* Tcl/Tk: be sure to have a suitable version of TclTk installed. In
			general you should install at least 8.5.
			You also need the 64 bit version of Tcl/Tk for 64 bit
			versions of ProB.

	* GraphViz: in order to make use of the graphical visualization features, you need to install a version of GraphViz suitable for your architecture. Then use the command "Graphical Viewer Preferences..." in the Preferences Menu to set or check the following preferences:		* GraphViz: in order to make use of the graphical visualization features, you need to install a version of GraphViz suitable for your architecture. Then use the command "Graphical Viewer Preferences..." in the Preferences Menu to set or check the following preferences:

Michael Leuschel: /* What are the available versions? */

2014-09-16T15:01:54Z

What are the available versions?

← Older revision		Revision as of 15:01, 16 September 2014
Line 7:		Line 7:
	* The online [[ProB_Logic_Calculator\|ProB Logic Calculator]]		* The online [[ProB_Logic_Calculator\|ProB Logic Calculator]]

	Both the standalone ProB Tcl/Tk and probcli can be downloaded together (within a Zip archive or tarball together with examples) from our [[Download\|Downloads page]].		Both the standalone ProB Tcl/Tk and probcli can be downloaded together (within a Zip archive or tarball together with examples) from our [[Download\|Downloads page]]. The online [[ProB_Logic_Calculator\|ProB Logic Calculator]] requires no installation; just type in predicates and expressions into the web page.

	There is also a [http://www.tools.clearsy.com/index.php5?title=ProB_etool_generation plugin for Atelier B], in order to use the standalone ProB Tcl/Tk Version on [http://www.atelierb.eu/ Atelier B] projects. It comes bundled with ProB Tcl/Tk.		There is also a [http://www.tools.clearsy.com/index.php5?title=ProB_etool_generation plugin for Atelier B], in order to use the standalone ProB Tcl/Tk Version on [http://www.atelierb.eu/ Atelier B] projects. It comes bundled with ProB Tcl/Tk.

Michael Leuschel: /* What are the available versions? */

2014-09-16T15:00:53Z

What are the available versions?

← Older revision		Revision as of 15:00, 16 September 2014
Line 13:		Line 13:
	ProB is used within a few other tools, such as [http://wiki.event-b.org/index.php/IUML-B iUML-B] or [http://safecap.sourceforge.net/index.shtml SafeCap].		ProB is used within a few other tools, such as [http://wiki.event-b.org/index.php/IUML-B iUML-B] or [http://safecap.sourceforge.net/index.shtml SafeCap].

	We are also developing a new Java-based API called [[ProB_2.0_Tutorial ProB 2.0]], which is a high-level wrapper for the command-line version [[Using_the_Command-Line_Version_of_ProB\|probcli]].		We are also developing a new Java-based API called [[ProB_2.0_Tutorial\|ProB 2.0]], which is a high-level wrapper for the command-line version [[Using_the_Command-Line_Version_of_ProB\|probcli]].

	== Which version should I use? ==		== Which version should I use? ==

Michael Leuschel at 15:00, 16 September 2014

2014-09-16T15:00:38Z

← Older revision		Revision as of 15:00, 16 September 2014
Line 3:		Line 3:

	* The standalone Tcl/Tk Version of ProB (ProB Tcl/Tk)		* The standalone Tcl/Tk Version of ProB (ProB Tcl/Tk)
	* The standalone command-line version of ProB (probcli)		* The standalone command-line version of ProB ([[Using_the_Command-Line_Version_of_ProB\|probcli]])
	* The ProB Plugin for Rodin/Eclipse		* The [[Tutorial_Rodin_First_Step\|ProB Plugin for Rodin/Eclipse]]
			* The online [[ProB_Logic_Calculator\|ProB Logic Calculator]]

	Both the standalone ProB Tcl/Tk and probcli can be downloaded together (within a Zip archive or tarball together with examples) from our [[Download\|Downloads page]].		Both the standalone ProB Tcl/Tk and probcli can be downloaded together (within a Zip archive or tarball together with examples) from our [[Download\|Downloads page]].
Line 11:		Line 12:

	ProB is used within a few other tools, such as [http://wiki.event-b.org/index.php/IUML-B iUML-B] or [http://safecap.sourceforge.net/index.shtml SafeCap].		ProB is used within a few other tools, such as [http://wiki.event-b.org/index.php/IUML-B iUML-B] or [http://safecap.sourceforge.net/index.shtml SafeCap].

			We are also developing a new Java-based API called [[ProB_2.0_Tutorial ProB 2.0]], which is a high-level wrapper for the command-line version [[Using_the_Command-Line_Version_of_ProB\|probcli]].

	== Which version should I use? ==		== Which version should I use? ==

Jens Bendisposto at 11:10, 23 July 2014

2014-07-23T11:10:14Z

← Older revision		Revision as of 11:10, 23 July 2014
Line 46:		Line 46:
	The following movie shows how to install the ProB Rodin Plugin.		The following movie shows how to install the ProB Rodin Plugin.

	<swf width="800" height="600">Install.swf</swf>		<swf width="800" height="600">http://www.stups.uni-duesseldorf.de/ProB/Install.swf</swf>

← Older revision		Revision as of 17:36, 5 March 2026
Line 9:		Line 9:

	== Installation Instruction for ProB (Standalone) ==		== Installation Instruction for ProB (Standalone) ==
	~~Note: we have specific [[Windows_Installation_Instructions]]. These here are the generic instructions.~~

	* Obtain your platform specific ProB distribution from [[~~Download\|Downloads~~]]. Decompress and expand the ProB directory if necessary. Do not change the location and structure of the files and directories within ProB (apart from the ~~Machines~~ directory)! ~~On Windows you just have to double-click the installer.~~ The contents of the ProB directory should look something like this:		* Obtain your platform specific ProB distribution from the [[download]] page. Decompress and expand the ProB directory if necessary. Do not change the location and structure of the files and directories within ProB (apart from the examples directory)! The contents of the ProB directory should look something like this:
	examples lib prob		examples lib prob
	StartProB.sh tcl		StartProB.sh tcl
	On Windows~~, you will also have a subfolder called "Microsoft.VC80.CRT" containing the DLLs for the C runtime. Also~~, the binary is called "ProBWin" and not "prob".		On Windows, the binary is called "ProBWin.exe" and not "prob".
	* Be sure that you have Tcl/Tk installed (see, e.g., http://www.tcl.tk/software/tcltk/).		* Be sure that you have Tcl/Tk installed (see, e.g., http://www.tcl.tk/software/tcltk/).
	With the latest version of ProB, you		With the latest version of ProB, you
	have to install Tcl/Tk version 8.5.		have to install Tcl/Tk version 8.5.
	For example, you can find a correct version of Tcl/Tk athttp://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ .		For example, you can find a correct version of Tcl/Tk athttp://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ .
	* To load your own B machines you also need Java 7 or newer runtime or better JDK.		* To load your own B machines you also need Java 8 or newer runtime or better JDK.
	* Note: you can skip this step if you do not wish to use the visualization commands. Install the "dot" program and "dotty" viewer from AT&T's Graphviz package (http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/). By default, ProB will open the "dotty" program to visualize the graphs, but postscript viewers (such as gv) are also supported. So, you do not need to install dotty if you don't want to; but it is probably easiest to install the entire Graphviz package.		* Note: you can skip this step if you do not wish to use the visualization commands. Install the "dot" program and "dotty" viewer from AT&T's Graphviz package (http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/). By default, ProB will open the "dotty" program to visualize the graphs, but postscript viewers (such as gv) are also supported. So, you do not need to install dotty if you don't want to; but it is probably easiest to install the entire Graphviz package.
	* Change to the ProB directory and then start up ~~prob~~. In Windows you can simply double-click on the ProBWin Application. ~~On Mac OS X you may have to type 'limit data unlimited' (in tcsh) or 'ulimit -d unlimited' (in bash) before launching ProB using~~ the ~~Terminal Application. The~~ distribution contains a script StartProB.sh ~~which does this~~ for ~~you~~ (note you may have to do chmod u+x StartProB.sh before launching it from the command-line).		* Change to the ProB directory and then start up ProB. In Windows you can simply double-click on the ProBWin Application. For macOS and Linux, the distribution contains a script StartProB.sh for starting the prob executable (note you may have to do chmod u+x StartProB.sh before launching it from the command-line).
	* Now you should be able to open some of the B Machines in the ~~Machines~~ directory. You should then be able to initialize the machines and animate them. Have a look at the supplied ~~Machines~~ in the examples directory. Have fun ! Please report bugs!		* Now you should be able to open some of the B Machines in the examples directory. You should then be able to initialize the machines and animate them. Have a look at the supplied machines in the examples directory. Have fun! Please report bugs!

	=== Checklist/Troubleshooting ===		=== Checklist/Troubleshooting ===

	* Java: be sure to have Java 7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.		* Java: be sure to have Java 8 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.

	* Tcl/Tk: be sure to have a suitable version of TclTk installed. In		* Tcl/Tk: be sure to have a suitable version of TclTk installed. In
	general you should install at least 8.5.		general you should install at least 8.5.
	~~You also need the 64 bit version of Tcl/Tk for 64 bit~~
	~~versions of ProB.~~

	* GraphViz: in order to make use of the graphical visualization features, you need to install a version of GraphViz suitable for your architecture. Then use the command "Graphical Viewer Preferences..." in the Preferences Menu to set or check the following preferences:		* GraphViz: in order to make use of the graphical visualization features, you need to install a version of GraphViz suitable for your architecture. Then use the command "Graphical Viewer Preferences..." in the Preferences Menu to set or check the following preferences:
Line 37:		Line 34:
	** Path/Command for dot viewer (e.g., dotty)		** Path/Command for dot viewer (e.g., dotty)
	Note: you can use the "Pick" button to locate the dot program and the dot viewer.		Note: you can use the "Pick" button to locate the dot program and the dot viewer.
	See more information about the [[Graphical Viewer~~\|Graphical Viewer here~~]].		See more information about the [[Graphical Viewer]].

	[[Category:User Manual]]		[[Category:User Manual]]