| Line 38: | Line 38: | ||
| [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.11.1/ProB_mac_os.x86_64.notarized.zip Zipfile] (notarized) <br/> | | [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.11.1/ProB_mac_os.x86_64.notarized.zip Zipfile] (notarized) <br/> | ||
[https://github.com/hhu-stups/homebrew-prob Homebrew Tap] | [https://github.com/hhu-stups/homebrew-prob Homebrew Tap] | ||
| OS X 10.9 (Mavericks) or newer, [ | | OS X 10.9 (Mavericks) or newer, Tcl/Tk [[#Tcl.2FTk_on_Mac_OS.2FX|(see below)]], | ||
[http://www.oracle.com/technetwork/java/javase/downloads/index.html Java JDK] or [https://adoptopenjdk.net Adopt JDK], <br/> | [http://www.oracle.com/technetwork/java/javase/downloads/index.html Java JDK] or [https://adoptopenjdk.net Adopt JDK], <br/> | ||
[http://www.graphviz.org/download/ Graphviz] | [http://www.graphviz.org/download/ Graphviz] | ||
Below are links for downloading the latest stable release of probcli (the command line version of ProB) and ProB Tcl/Tk (ProB with a graphical user interface written in Tcl/Tk). Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.
Details of the ProB Licence can be found here. ProB is free to use and open source. For commercial support contact Michael Leuschel. 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 (64 bit) | Dependencies |
|---|---|---|---|
| 1.11.1 | |||
| Linux | 29.12.2021 | Tarball |
Java Runtime Environment (7.0 or newer) or Adopt JDK, |
| Windows | 29.12.2021 | Zipfile (Tcl/Tk 8.6), Zipfile (Tcl/Tk 8.5) |
Tcl/Tk for Windows,
Java Runtime Environment (7.0 or newer) or Adopt JDK, |
| OS X | 29.12.2021 | Zipfile (notarized) |
OS X 10.9 (Mavericks) or newer, Tcl/Tk (see below), |
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 unless stated otherwise. On very recent Linux systems (such as Ubuntu 20.04) you may want to download (and compile) Tcl/Tk 8.5 or use packages from earlier releases. All releases include the command-line version probcli which does not require Tcl/Tk. All releases are compiled for 64-bit architectures.
Note that: on macOS you still have to right-click on the application and use "Open", even though ProB Tcl/Tk (and probcli and all libraries) are signed and notarized. Also, in order for the menus to work you may first have to click into another window and then click again onto the ProB main window. This seems to be a bug in Tcl/Tk on macOS. Finally, if you get the error message macOS 11 or later required, then try reinstalling Active Tcl/Tk or running brew install tcl (see stackoverflow or here and see our instructions below).
The latest beta release is 1.10.0-beta4 (and in this case is older than the current release above). An official beta release always passes all of ProB's tests. However, we do not follow the stringent checklist for final releases (e.g., checking SICStus Prolog Spider warnings, checking coverage and additional manual UI tests). Also, we do not store coverage reports and other information necessary for T2 certification.
More current nightly integration releases are also available below. These releases are not stored and usually updated every night. There is also a notarized version available for useful, e.g., for macOS Catalina.
You can now create Jupyter Notebooks in B using the ProB Jupyter Kernel.
To install ProB for Rodin, first download Rodin 2.8, Rodin 3.3 or Rodin 3.4, choose Help -> Install New Software and simply choose the pre-configured ProB update site. (The pre-configured update site is http://www.stups.uni-duesseldorf.de/prob_updates for Rodin 2.8 and http://www.stups.hhu.de/prob_updates_rodin3 for Rodin 3.x. The update site for nightly builds for Rodin 3.x is https://www3.hhu.de/stups/rodin/prob1/nightly.) More detailed installation instructions and a brief tutorial are available.
Warning: in Rodin 3.4 there is an issue where a model checking counter example leads to a hanging Rodin if the machine is not initialised. The issue is solved in the latest nightly build of ProB for Rodin (https://www3.hhu.de/stups/rodin/prob1/nightly). The issue is not present in Rodin 3.3.
Version 1.1.0 of the new Java FX based ProB2-UI is available. You can use these stand-alone versions which come bundled with the right Java runtime environment:
Note that: on macOS you may have to initially launch ProB2-UI twice.
You can also download a multi-platform jar which works Java 11 or later (and with Java 8 versions which have JavaFX included) on all platforms (including Linux):
For Java 8 we recommend using Azul Zulu. Adopt OpenJDK does not come with JavaFX at the moment.
The SVG-based visualization called VisB is included in version 1.1.0 of ProB2-UI.
Details about new features and improvements can be found in the release history, along with download links for older versions.
Snapshot builds of the current development version of ProB2-UI are available at https://www3.hhu.de/stups/downloads/prob2/snapshot/.
Note, on macOS you may need to run the following command to be able to launch ProB2-UI, as the nightly builds are not notarized or signed:
sudo xattr -r -c ProB\ 2\ UI.app/
You can also start the latest version directly from source:
run task to start the application:
./gradlew run.\gradlew.bat runIf the build shows errors during createHelp, you need to install Pandoc.
Alternatively you can add the argument --exclude-task createHelp to the gradlew command to skip building the help files.
The underlying Java API ProB2 of ProB2-UI is available to Java developers via Maven Central.
A VIM plugin for ProB is available. It shows a quick fix list of parse and type errors for classical B machines (.mch) using the command line tool probcli. VIM has builtin syntax highlighting support for B.
There is a package language-b-eventb available for the Atom editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom. It integrates with command line tool probcli to obtain error markers for syntax and type errors.
Some BBedit Language modules for B, TLA+, CSP and Prolog are available; these do not use command line tool probcli.
Prior Versions of ProB going back to 1.3.1 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 (Mac OS X) you may have to install a JDK such as the Adopt OpenJDK, Azul Zulu or 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; see also this discussion on StackOverflow). In case you have trouble starting the Java parser you can now set the JAVA_PATH preference of ProB 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 should get an error message. 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 or Tcl/Tk 8.6 depending on the version of ProB. The command-line tool probcli does not require this.
Note: for macOS (until bigSur) you may have to install the ActiveTcl version of Tcl/Tk as indicated above (the distribution provided by Apple is typically broken, e.g., after opening a file using the standard file selection dialog some versions crash). However, even the version of Active Tcl/Tk on Mac can be quite unreliable and prone to crashing; for example version 8.5.12 has a serious bug related to copying text, see also here). This issue has been fixed in version 8.5.13 or later.
Note: on macOS Catalina or later the Tcl/Tk menu bar is sometimes not working. Switching to another application and then back to ProB seems to solve the problem. If you see the message "macOS 11 or later required !" in the terminal when launching prob you should re-install Tcl/Tk as described above.
On macOS Monterey you should use Tcl/Tk 8.6.9 or later, as version 8.5 no longer seems to work correctly (e.g., text views are black). However, in Active Tcl/Tk 8.6 on macOS the double click in the "Operations View" or other views is not working correctly. You have to hit the RETURN key in the "Operations View" or right-click on an operation and select "Perform ..." to execute an operation until this is fixed. You can install a newer Tcl/Tk (e.g., 8.6.12) using Homebrew or MacPorts. Unfortunately, the earlier release 8.6.11 also has problems on macOS Monterey, the file open and file save dialogs will not work. Release 8.6.12 has fixed this. For Homebrew the command to install thetcl-tk formula is:
brew install tcl-tk
However, as the location of the libraries is not standard, you have to define the variable SP_TCL_DSO. You can also define and export this variable before starting ProB from the Terminal by typing this (you may have to adapt the link if you are using another version of Tcl/Tk):
export SP_TCL_DSO=/usr/local/Cellar/tcl-tk/8.6.12/lib/libtcl8.6.dylib
If you have uses MacPorts the path is probably /opt/local/lib/libtcl.dylib. You can also set the variable by adding -DSP_TCL_DSO=/usr/local/Cellar/tcl-tk/8.6.12/lib/libtcl8.6.dylib to the command starting ProB. You may also have to install tk-table package yourself (it is bundled with Active Tcl).
We currently provide two downloads of ProB, one for Tcl/Tk 8.6 (which we recommend) and a version for Tcl/Tk 8.5. You can use for example the ActiveTcl releases. Note: For the 64 bit version of ProB for Windows, you have to install the 64 bit Tcl/Tk 8.5 version!
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
Also, some of the feature require the table extension, which can be installed like this:
sudo apt install tk-table
Finally, support for .png ANIMATION_IMG declarations requires the Img package:
sudo apt install libtk-img
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 and a dot-file viewer such as dotty (optionally in ProB Tcl/Tk).
On Mac, the only working application to view dot files is graphviz-gui by MacPorts. To install the application do this
The viewer can now be found in /Applications/MacPorts/Graphviz.app (you may have to set the ProB graphical viewer preference dot_viewer to this path). Some ProB commands work directly with the command-line tool dot which you can install with MacPorts like this:
On Mac you can now install the latest version of Graphviz using HomeBrew:
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. This is probably better than using the older version from Pixelglow.
Note: if you wish to use the fast rendering for large state spaces in ProB 1.7.x, 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). As of version 1.8.1 ProB only uses the dot binary for command-line tasks (and not sfdp anymore), making use of the -Ksfdp option.
You can download the latest Prolog sourcecode snapshot from: http://www3.hhu.de/stups/downloads/prob/source/
The source code for the ProB parsers (B, LTL, ...) can be obtained from: https://github.com/hhu-stups/probparsers.
The ProB2-Java-API source code can be obtained from: https://github.com/hhu-stups/prob2_kernel.
The ProB2-Java-FX UI source code can be obtained from: https://github.com/hhu-stups/prob2_ui.
6/10/2021 ProB 1.11.0 is available. Improved support for infinite sets, operation caching (OPERATION_REUSE), faster LTL checking for safety formulas, more compact .prob files, VisB HTML export, constructive Z3 translation.
15/12/2020 ProB 1.10.0 is available. Highlights: well-definedness prover, REAL datatype, -lint comand for VSCode and Atom, improved unsat core and error messages.
19/2/2020 ProB 1.9.3 is available. Highlights: performance improvements, new external functions, performance monitoring.
11/11/2019 ProB 1.9.2 is available. Minor bugfix release.
8/11/2019 ProB 1.9.1 is available. Maintenance release.
12/7/2019 ProB 1.9.0 is available. Highlights: improved error feedback, improved Unicode support, regular expression library, memoization.
1/10/2018 ProB 1.8.2 is available. Highlights: improved error feedback, support Jupyter kernel, first support for Alloy models.
20/03/2018 ProB 1.8.0 is available. Highlights: terminal colour support, performance improvements for displaying very large values, improved symmetry breaking and constraint solving.
5/10/2017 ProB 1.7.1 is available. Highlights: performance, non-deterministic assigned variables shown, Z improvements, export history to HTML.
11/7/2017 ProB 1.7.0 is available. Highlights: improved Latex document generation, improved XML/CSV data import and export, RULE DSL language, many improvements in constraint solver.
20/10/2016 ProB 1.6.1 is available. Highlights: Latex document generation, LET and IF-THEN-ELSE for expressions and predicates, XML logging, XML data import, performance improvements.
22/4/2016 ProB 1.6.0 is available. Highlights: directed model checking, Z3 available as backend, B line comments and unicode symbols, improved error messages, performance improvements.
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.
The full ProB release history can be found here.