Details of the ProB Licence can be found here. Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.
ProB is free to use and open source; commercial support can be provided by the spin-off company Formal Mind. In particular, we can provide access to the validation report for using ProB as a tool of class T2 or T3 within the European norm EN50128.
| Platform | Release Date | Download | Dependencies |
|---|---|---|---|
| 1.5.0-final | |||
| Linux | 19. February 2015 | Tarball (with probcli) (32bit), Tarball (with probcli) (64bit) |
Java Runtime Environment (7.0 or newer), Tcl/Tk 8.5 |
| Windows | 19. February 2015 | Zipfile (with probcli) (32bit), Zipfile (with probcli) (64bit) |
Tcl/Tk 8.5 for Windows,
Java Runtime Environment (7.0 or newer), Windows Installation Instructions |
| OS X | 19. February 2015 | Tarball (with probcli) (64bit) Homebrew Tap | Tcl/TK 8.5
Java Runtime Environment or better Java JDK (7.0 or newer) Graphviz for Mac OS X |
The B parser of ProB requires Java 7 or newer. Sometimes you have to install the Java JDK (and not the JRE) so that the new Java version becomes visible to command-line tools. The Graphical User Interface of ProB Tcl/Tk requires Tcl/Tk 8.5. Note: If you wish to use ProB on Windows XP you need the service pack SP3 installed.
To install ProB for Rodin, first download Rodin 2.8 or Rodin 3.1, choose Help -> Install New Software and simply choose the pre-configured ProB update site. More detailed installation instructions and a brief tutorial are available.
Prior Versions of ProB going back to 1.3.1 are still are available for download here. If you are interested in still earlier releases, please have a look at the Download directory.
The B parser of ProB 1.5.1 requires Java Runtime Environment (JRE) 7 or newer. ProB 1.5.0 can be run with JRE 6. Note: on some systems (Mountain Lion OS X) you may have to install the Oracle JDK/JSE (and not just the JRE) so that Java 7 or 8 becomes available to the command-line tools (type java -version to check which version is used by default for command-line tools). In case you have trouble starting the Java parser you can now set the JAVA_PATH preference to point to the java tool (or java.exe on Windows).
To check whether ProB can correctly use its Java parser you can type the following (using probcli.exe on Windows):
probcli -version -v
This will try and start the parser and obtain the parser version. In case Java is not correctly installed you may currently get various error messages. On Windows, you may see the error message
Error occurred during initialization of VM
on the console. This means you should probably re-install the Java JRE with admin rights and try again. If you see the error message
Unsupported major.minor version 51.0
this means you do not have Java 7 or newer installed. You can try setting the path to the correct java version by setting the JAVA_PATH preference as follows:
probcli -p JAVA_PATH path/to/java -version -v
ProB Tcl/Tk requires an installation of Tcl/Tk 8.5. The command-line tool probcli does not require this. Please note that Tcl/Tk 8.6 is not yet generally supported by SICStus Prolog (even though ProB may work with Tcl/Tk 8.6; we recommend installing Tcl/Tk 8.5 though).
Note: for Mac OS you may have to install the ActiveTcl version of Tcl/Tk as indicated above (the distribution provided by Apple is typically broken).
Also note that on Mac OS X you may have to reinstall Tcl/Tk using one of the links given above (because the Tcl/Tk provided by Apple crashes often, e.g., after opening a file using the standard file selection dialog. However, even the version of Active Tcl/Tk on Mac seem quite unreliable and prone to crashing; for example version 8.5.12 has a serious bug related to copying text, see also here; you can use the older version 8.5.11.1 instead). This issue seems to have been fixed in version 8.5.13.
Starting with ProB 1.3.5 you can now use ProB with Tcl/Tk 8.5 on Windows. If you have the older version of Tcl/Tk 8.4 you have to install the newer one 8.5 (you should be able to also keep the older version). For Windows we recommend installing ActiveTcl-8.5. Note: For the 64 bit version of ProB for Windows, you have to install the 64 bit Tcl/Tk 8.5 version! If you wish to use ProB on Windows XP you need the service pack SP3 installed.
On Linux you can typically install Tcl/Tk using sudo apt-get install tcl8.5 tk8.5. On Linux OpenSuse (12.3) you may have to perform the following for ProB to work:
ln -s /usr/lib/libtk8.5.so /usr/lib/libtk8.5.so.0 ln -s /usr/lib/libtcl8.5.so /usr/lib/libtcl8.5.so.0
You can download our nightly integration build from here. Note: if you wish to use the fast rendering for large state spaces, you need the sfdp tool of GraphViz (ideally version 2.28 or newer with the triangulation library; when installing using brew use the option --with-gts; see the section below).
Automatically generated test coverage reports are also available.
Nightly builds of ProB for Rodin 3 can be obtained from within Rodin by using the update site http://www3.hhu.de/stups/rodin/prob1/nightly/.
Nightly builds of ProB for Rodin 2 can be obtained from within Rodin by using the update site http://nightly.cobra.cs.uni-duesseldorf.de/rodin/updatesite/.
Nightly builds of ProB 2 (experimental) for Rodin 3 can be obtained from within Rodin using the update site http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/nightly/.
If you wish to view various visualizations generated by ProB Tcl/Tk or probcli you will need GraphViz. ProB may use the command-line tool dot, a dot-file viewer such as dotty or more recently the command-line tool sfdp.
On Mac you can now install the latest version of Graphviz using brew:
1. brew uninstall graphviz 2. brew install graphviz --with-gts 3. brew link --overwrite graphviz
Step 1. is optional; you only need to use it if you have a prior version of Graphviz installed. Step3 links the binaries to /usr/local/bin.
A version of ProB with built-in support for timed CSP developed by Swansea University (UK) is available on here: http://nightly.cobra.cs.uni-duesseldorf.de/timed-csp/
You can download the latest sourcecode snapshot from: http://www3.hhu.de/stups/downloads/prob/source/
19/2/2015 ProB 1.5.0 is available. Highlights: improved random enumeration, MACE/SEM style static symmetry reduction for deferred set elements, MC/DC coverage analysis for guards and invariants, improved TLC interface, bug fixes and improvements including but not limited to the constraint solver.
29/8/2014 ProB 1.4.1, a small bugfix-only release is available. For a list of new features in 1.4.0 see below.
18/8/2014 ProB 1.4.0 is available. Highlights: CLP(FD)-based constraint solver enabled by default, kernel can handle more operations symbolically, integration of the TLC model checker, bug fixes and performance improvements.
4/3/2013 ProB 1.3.6 is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, improved Kodkod backend and use within REPL, and many more.
8/10/2012 ProB 1.3.5 is available. Highlights: support for external and recursive functions, optional Kodkod backend, TLA+ support, performance improvements, pragmas, units inference, and many more.
30/03/2012 A first prototype of an online ProB Logic Calculator is available.
21/11/2011 ProB 1.3.4 is available. Highlights: Evaluation View and Eval window, CSP assertion checking, improved editor, 64-bit version for Mac and Linux, performance improvements, and many more.
10/02/2011 ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more.
07/30/2010 ProB 1.3.2 is available. Highlights: improved performance, constraint solving over integers (enable in Advanced Preferences), much improved Z support, and many more.
12/07/2009 ProB 1.3.1 is available. Highlights: new data-structure for large sets and relations (see FM 2009), multi-level validation for Event-B, improved constraint propagation for boolean connectives, and many more.
03/20/2009 ProB 1.3.0 is available for download. Highlights: New parser and integrated typechecker, install as AtelierB plugin, improved kernel with support for large sets/relations, improved CSP support, faster LTL model checker, Undo/Redo in text editor, graphical formula viewer, user definable custom animations with gifs.