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) | 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 requires Java Runtime Environment (JRE) 7 or newer. 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).
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.