Download: Difference between revisions

Tag: Manual revert
 
(246 intermediate revisions by 2 users not shown)
Line 4: Line 4:
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).
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.
Note: please use the provided start scripts (StartProB.sh or StartProBWin.bat) to start ProB.
The list of changes can be found in the [[ProB_Release_History | ProB release history]].


Details of the [[ProBLicence| ProB Licence can be found here]].
Details of the [[ProBLicence| ProB Licence can be found here]].
ProB is free to use and open source. For commercial support contact the spin-off company [http://www.formalmind.com Formal Mind] or [http://www.stups.uni-duesseldorf.de/~leuschel/ 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 [http://de.wikipedia.org/wiki/EN_50128 EN50128].
ProB is free to use and open source. For commercial support contact  [https://www.stups.uni-duesseldorf.de/~leuschel/ 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 [https://de.wikipedia.org/wiki/EN_50128 EN50128].


{| border="1"  cellpadding="30"
{| class="table table-bordered wikitable" <!-- table and table-bordered for Bootstrap (ProB skin), wikitable for MediaWiki (Vector, MonoBook, etc. skins) -->
! Platform &nbsp;&nbsp;
! Platform
! Release Date &nbsp;&nbsp;
! Release Date
! Download (64 bit)&nbsp;&nbsp;
! Download
! Dependencies
! Dependencies
|-
|-
| colspan="4" style="background-color:lightgrey;" | 1.9.0-release
| colspan="4" style="background-color:lightgrey;" | 1.13.0
|-
|-
| Linux  
| Linux  
| 12.7.2019
| 20.2.2024
| [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.9.0/ProB.linux64.tar.gz Tarball]<br/>
| [https://stups.hhu-hosting.de/downloads/prob/tcltk/releases/1.13.0/ProB.linux64.tar.gz Tarball]<br/>
| [http://java.com/en/ Java Runtime Environment (7.0 or newer)] or [https://adoptopenjdk.net Adopt JDK],<br/>
| Java 8 or newer ([[#Java Requirements for B parser|see below]]), Tcl/Tk 8.5 or 8.6 ([[#Tcl/Tk on Linux|see below]]), [https://www.graphviz.org/download/ GraphViz]
Tcl/Tk 8.5, [http://www.graphviz.org/ GraphViz]
|-
| colspan="4" style="background-color:lightgrey;" style="height:20px; | 
|-
|-
| Windows
| Windows
| 12.7.2019 
| 20.2.2024
| [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.9.0/ProB.windows64.zip Zipfile] (Tcl/Tk 8.6), <br/>[http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.9.0/ProB.windows64-tcltk85.zip Zipfile] (Tcl/Tk 8.5) <br/>
| [https://stups.hhu-hosting.de/downloads/prob/tcltk/releases/1.13.0/ProB.windows64.zip Zipfile] (Tcl/Tk 8.6), <br/> [https://stups.hhu-hosting.de/downloads/prob/tcltk/releases/1.13.0/ProB.windows64-tcltk-85.zip Zipfile] (Tcl/Tk 8.5)
| [http://downloads.activestate.com/ActiveTcl/releases/ Tcl/Tk for Windows],
| Tcl/Tk 8.5 or 8.6 ([[#Tcl/Tk on Windows|see below]]), Java 8 or newer ([[#Java Requirements for B parser|see below]]), [https://www.graphviz.org/download/ GraphViz], [[Windows Installation Instructions]]
[http://java.com/en/ Java Runtime Environment (7.0 or newer)] or [https://adoptopenjdk.net Adopt JDK],<br/>
[http://www.graphviz.org/Download_windows.php GraphViz], <br/>
[[Windows Installation Instructions]]
|-
| colspan="4" style="background-color:lightgrey;" style="height:20px; | 
|-
|-
| OS X
| macOS
| 12.7.2019
| 20.2.2024
| [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.9.0/ProB.mac_os.x86_64.tar.gz Tarball] <br/>
| [https://stups.hhu-hosting.de/downloads/prob/tcltk/releases/1.12.2/ProB.macos.zip Zipfile] (Universal ARM/Intel 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, [http://www.activestate.com/activetcl/downloads/ Tcl/TK 8.5] (e.g., [http://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ 8.5.18.0]),
| macOS 10.14 (Mojave) or newer, Tcl/Tk ([[#Tcl/Tk on macOS|see below]]), Java 8 or newer ([[#Java Requirements for B parser|see below]]), [https://www.graphviz.org/download/ Graphviz] ([[#Graphviz_Requirements|see below]])
[http://java.com/en/ Java Runtime Environment] or better [http://www.oracle.com/technetwork/java/javase/downloads/index.html Java JDK] or  [https://adoptopenjdk.net Adopt JDK], <br/>
[http://www.pixelglow.com/graphviz/ Graphviz for Mac OS X]
|}
|}


The B parser of ProB requires [http://java.com/en/ 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 B parser of ProB requires Java 8 or newer. More details [[#Java Requirements for B parser|are available below]].
The Graphical User Interface of ProB Tcl/Tk requires Tcl/Tk 8.5 unless stated otherwise.
 
All releases include the command-line version <b>probcli</b> which does not require Tcl/Tk.
The Graphical User Interface of ProB Tcl/Tk requires Tcl/Tk 8.5 or 8.6. More details [[#Tcl/Tk Requirements for ProB Tcl/Tk|are available below]].
All releases are compiled for <b>64-bit</b> architectures.
The default Tcl/Tk on macOS is broken and will result in <b>black windows</b>, and you have to [[#Tcl/Tk Requirements for ProB Tcl/Tk|install another version of Tcl/Tk]].
Note: If you wish to use ProB on Windows XP you need the service pack SP3 installed.
All releases include the command-line version <b>probcli</b> which does <b>not</b> require Tcl/Tk.


Releases are compiled for the '''x86_64''' architecture (64-bit Intel).
macOS releases of ProB 1.12.0 and later also support '''aarch64''' (64-bit ARM/Apple Silicon).
The last version built for x86 (32-bit Intel) is ProB 1.8.0 (see [[DownloadPriorVersions|prior versions]]).
If you are using an unsupported architecture or system, you may still be able to [[Running ProB from source|run ProB from source]].
Note that: on <b>macOS</b> 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.
=== Latest Beta Release ===
=== Latest Beta Release ===


The latest beta release is [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/1.9.1-beta2 1.9.1-beta2].
The latest beta release is [https://stups.hhu-hosting.de/downloads/prob/tcltk/releases/1.13.1-beta1 1.13.1-beta1].
An official beta release always passes all of ProB's tests.
An official beta release always passes all of ProB's tests.
However, we do not follow the stringent checklist for final releases
However, we do not follow the stringent checklist for final releases
Line 58: Line 56:
Also, we do not store coverage reports and other information necessary for T2 certification.
Also, we do not store coverage reports and other information necessary for T2 certification.


More current [http://www3.hhu.de/stups/downloads/prob/tcltk/nightly/ nightly integration releases] are also available [[#Nightly Builds| below]].
=== Nightly Builds ===
These releases are not stored and usually updated every night.
 
More current [https://stups.hhu-hosting.de/downloads/prob/tcltk/nightly/ nightly integration builds] are also available.
These releases are usually updated every night and old versions are not stored.
 
Note for macOS users: Nightly builds of ProB are not signed or notarized, so macOS 10.15 and later (Catalina, Big Sur or Monterey, Ventura) will refuse to run them.
As a workaround, you will need to run <code>xattr -r -d com.apple.quarantine *</code> inside the ProB directory before launching ProB.
The stable and beta releases listed above are signed and notarized, so they will run without extra steps.
 
Automatically generated test [https://stups.hhu-hosting.de/internal/coverage/html/ coverage reports are also available].
They are usually updated once per week.
 
=== Sourcecode ===
 
You can download the latest Prolog sourcecode snapshot from: https://stups.hhu-hosting.de/downloads/prob/source/
 
The source code for the ProB parsers (B, LTL, ...) can be obtained from: https://github.com/hhu-stups/probparsers
 
=== Prior Versions ===
 
Prior Versions of ProB going back to 1.3.1 [[DownloadPriorVersions|are available for download here]].
If you are interested in still earlier releases, please have a look at the [https://stups.hhu-hosting.de/downloads/prob/tcltk/releases/ Download directory].
 
== Other ProB tools ==


=== ProB Jupyter Kernel ===
=== ProB Jupyter Kernel ===


You can now create Jupyter Notebooks in B using the [https://gitlab.cs.uni-duesseldorf.de/dgelessus/prob2-jupyter-kernel ProB Jupyter Kernel].
You can now create Jupyter Notebooks in B using the ProB Jupyter kernel.
Downloads, instructions, and source code can be found on [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel its own page].
 
You can [https://mybinder.org/v2/git/https%3A%2F%2Fgitlab.cs.uni-duesseldorf.de%2Fgeneral%2Fstups%2Fprob2-jupyter-kernel.git/master?filepath=notebooks try out the ProB Jupyter kernel in your browser] without installing it first.
Note that '''notebooks are not saved permanently in this online version!'''
To keep your notebooks, you ''must'' download them before closing the page.


=== ProB for Rodin ===
=== ProB for Rodin ===
To install ProB for Rodin, first download Rodin 2.8, [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/ Rodin 3.3] or [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.4/ Rodin 3.4], choose Help -> Install New Software and simply choose the pre-configured ProB update site.
To install ProB for Rodin, first download a current version of Rodin (e.g., [https://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.8/ Rodin 3.8]). Inside Rodin, choose Help -> Install New Software and choose the pre-configured ProB update site.
(The pre-configured update site is [http://www.stups.uni-duesseldorf.de/prob_updates http://www.stups.uni-duesseldorf.de/prob_updates]  for Rodin 2.8 and [http://www.stups.hhu.de/prob_updates_rodin3 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 https://www3.hhu.de/stups/rodin/prob1/nightly].)
 
More [[Tutorial_Rodin_First_Step|detailed installation instructions and a brief tutorial are available]].
More [[Tutorial Rodin First Step|detailed installation instructions and a brief tutorial]] are available.
 
* Nightly builds of ProB for Rodin 3 can be obtained from within Rodin by using the update site https://stups.hhu-hosting.de/rodin/prob1/nightly.
 
=== ProB2-UI (based on JavaFX)===
 
Version 1.2.1 of the new JavaFX-based [[ProB2-UI]] is available.
See the [https://github.com/hhu-stups/prob2_ui/blob/develop/doc/prob2ui_release_history.md release history] for what's new.
You can use these stand-alone versions which come bundled with the right Java runtime environment:
* [https://stups.hhu-hosting.de/downloads/prob2/1.2.1/ProB%202%20UI-1.2.1.exe Windows installer]
* [https://stups.hhu-hosting.de/downloads/prob2/1.2.1/ProB%202%20UI-aarch64-1.2.1.dmg macOS (Apple Silicon) application DMG] (not signed/notarized yet! [[#macOS issues|see below]])
* [https://stups.hhu-hosting.de/downloads/prob2/1.2.1/ProB%202%20UI-x86_64-1.2.1.dmg macOS (Intel) application DMG] (not signed/notarized yet! [[#macOS issues|see below]])
* [https://stups.hhu-hosting.de/downloads/prob2/1.2.1/prob2-ui_1.2.1-1_amd64.deb Debian package]
 
You can also download a [https://stups.hhu-hosting.de/downloads/prob2/1.2.1/prob2-ui-1.2.1-multi.jar multi-platform jar], which works Java 11 or later (and with Java 8 versions which have JavaFX included) on all platforms (Windows, macOS, Linux).
 
Details about new features and improvements can be found in the [[ProB2-UI Release History|release history]], along with download links for older versions.
 
Snapshot builds of the current ''development'' version of ProB2-UI (1.2.2-SNAPSHOT) are also available:
* [https://stups.hhu-hosting.de/downloads/prob2/snapshot/ProB%202%20UI-1.2.2.exe Windows installer snapshot]
* [https://stups.hhu-hosting.de/downloads/prob2/snapshot/ProB%202%20UI-aarch64-1.2.2.dmg macOS (Apple Silicon) application DMG snapshot] (not signed/notarized! [[#macOS issues|see below]])
* [https://stups.hhu-hosting.de/downloads/prob2/snapshot/ProB%202%20UI-x86_64-1.2.2.dmg macOS (Intel) application DMG snapshot] (not signed/notarized! [[#macOS issues|see below]])
* [https://stups.hhu-hosting.de/downloads/prob2/snapshot/prob2-ui_1.2.2-1_amd64.deb Debian package snapshot]
* [https://stups.hhu-hosting.de/downloads/prob2/snapshot/prob2-ui-1.2.2-SNAPSHOT-multi.jar Multi-platform jar snapshot]
 
The source code for ProB2-UI is available at https://github.com/hhu-stups/prob2_ui and can be built by following [https://github.com/hhu-stups/prob2_ui#running-from-source these instructions].


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 underlying [[ProB Java API]] of ProB2-UI (aka the ProB 2 kernel) is available to Java developers via [https://central.sonatype.com/artifact/de.hhu.stups/de.prob2.kernel Maven Central].
The issue is  solved in the latest nightly build of ProB for Rodin ([https://www3.hhu.de/stups/rodin/prob1/nightly https://www3.hhu.de/stups/rodin/prob1/nightly]). The issue is not present in [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.3/ Rodin 3.3].
Its source code can be obtained from: https://github.com/hhu-stups/prob2_kernel.


=== ProB2 UI using Java FX ===
==== macOS issues ====


Version 1.0.0 and the snapshot of 1.0.1 of the new [[ProB2_JavaFX_UI|Java FX UI (aka ProB2 FX)]] is available at [https://www3.hhu.de/stups/downloads/prob2/ https://www3.hhu.de/stups/downloads/prob2/]:
When you run the macOS app for the first time, you might have to open the app ''twice'' for ProB 2 UI to start properly.
* [https://www3.hhu.de/stups/downloads/prob2/prob2-ui-1.0.0-all.jar Version 1.0.0 as a JAR file for all platforms]
This should only happen once.
* [https://www3.hhu.de/stups/downloads/prob2/prob2-ui-1.0.0-mac.zip Version 1.0.0 bundled as a Mac application]
* [https://www3.hhu.de/stups/downloads/prob2/prob2-ui-1.0.0-all.jar Version 1.0.0 as a Zip archive for Windows] (with a .bat script to start the UI)


It is tested with Java 8.
The ProB 2 UI macOS app releases are signed and notarized, so they should run without issues on current macOS versions.
We recommend using [https://adoptopenjdk.net Adopt OpenJDK].
However, the multi-platform jar and snapshot app builds are ''not'' signed or notarized, so newer macOS versions will refuse to run them or say that the application is damaged.
With Java 11 you have to [https://openjfx.io/openjfx-docs/#install-javafx install JavaFX] in addition to Java itself and start ProB2-UI using the command like the following:
As a workaround, right-click the app, select "Open", and confirm the security dialog.
  java --module-path ..../javafx-sdk-11.0.2/lib --add-modules=javafx.controls -jar prob2-ui-1.0.0-all.jar
If the dialog still doesn't give you an option to open the app, click "Cancel" and do the same thing again.
<!--
As a workaround, run this command in the folder where ''ProB 2 UI.app'' is located:


We also provide a plugin for SVG-based visualization called [[VisB]] at [https://www3.hhu.de/stups/downloads/prob2/plugins/ https://www3.hhu.de/stups/downloads/prob2/plugins/].
<pre>
xattr -r -d com.apple.quarantine "ProB 2 UI.app"
</pre>


The underlying API [[ProB_Java_API|ProB2]] of ProB2UI  is available to Java developers via [https://search.maven.org/search?q=a:de.prob2.kernel Maven Central].
The multi-platform jar can also be started from the command line, which bypasses the signing/notarization check:


=== Editor Support ===
<pre>
java -jar prob2-ui-1.2.1-multi.jar
</pre>
-->


A [https://github.com/bivab/prob.vim VIM plugin for ProB is available].
To run the multi-platform jar on macOS, we recommend using Java 15 or later.
It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].
Older Java/JavaFX versions may lead to an incorrect system font resulting in gibberish text display.
Alternatively, use the macOS app build, which comes with Java 17 and does not have this issue.


There is a package [https://atom.io/packages/language-b-eventb language-b-eventb] available for the Atom editor.
=== Editor Support ===
It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom.
It integrates with [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]] to obtain error markers for syntax and type errors.


Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available; these do not use [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]].
* A [https://github.com/bivab/prob.vim VIM plugin for ProB is available]. It shows a quick fix list of parse and type errors for classical B machines (.mch) using the [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]]. VIM has builtin syntax highlighting support for [https://github.com/vim/vim/blob/master/runtime/syntax/b.vim B].


== Nightly Builds ==
* There is a [https://github.com/hhu-stups/b-language-extension B/ProB Language Support] extension for the VSCode editor. It integrates with [[Using the Command-Line Version of ProB|command line tool probcli]] to obtain error markers for syntax and type errors. It can also be used for [[Well-Definedness Checking#VSCode|well-definedness checking]].


* You can download our [http://www3.hhu.de/stups/downloads/prob/tcltk/nightly/ nightly integration build from here].  Note: on Windows you will need [https://www.activestate.com/products/activetcl/downloads/ Tcl/Tk 8.6.6 or newer] to use the regular version of ProB (we currently also provide a version compiled for Tcl/Tk 8.5.x using an older SICStus Prolog version).
* Some [https://github.com/leuschel/bbedit-prob BBedit Language modules for B, TLA+, CSP and Prolog] are available; these do not use [[Using_the_Command-Line_Version_of_ProB|command line tool probcli]].
* Automatically generated test [https://www3.hhu.de/stups/internal/coverage/html/ coverage reports are also available].
* Nightly builds of ProB for Rodin 3 can be obtained from within Rodin by using the update site [https://www3.hhu.de/stups/rodin/prob1/nightly https://www3.hhu.de/stups/rodin/prob1/nightly].
* Nightly builds of ProB 2 (experimental) for Rodin 3 can be obtained from within Rodin using the update site [https://www3.hhu.de/stups/rodin/prob2/nightly/ https://www3.hhu.de/stups/rodin/prob2/nightly/] (this will probably be replaced by a Java FX version in the future)


== Prior Versions ==
== Java Requirements for B Parser ==
The B parser of ProB requires Java 8 or newer. Java 11, 17, etc. are also fully supported.
ProB 1.9.3 is the last version to support Java 7. ProB 1.5.0 is the last version to support Java 6.


Prior Versions of ProB going back to 1.3.1  [[DownloadPriorVersions|are available for download here]].
You can install a Java Runtime Environment (JRE) from various sources, such as [https://adoptium.net/ Eclipse Adoptium], [https://www.azul.com/downloads/?version=java-8-lts&package=jre-fx Azul Zulu], or your system package manager.
If you are interested in still earlier releases, please have a look at the [http://www3.hhu.de/stups/downloads/prob/tcltk/releases/ Download directory].


== Java  Requirements for B parser ==
Note: on some systems (macOS) you may have to install the full Java Development Kit (JDK), and not just the JRE, so that Java 8 becomes available to the command-line tools.
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.
Type <code>java -version</code> to check which version is used by default for command-line tools; see also [http://stackoverflow.com/questions/21964709/how-to-set-or-change-the-default-java-jdk-version-on-os-x this discussion on StackOverflow].
Note: on some systems (Mac OS X) you may have to install a JDK such as the [https://adoptopenjdk.net Adopt OpenJDK] or the [http://www.oracle.com/technetwork/java/javase/downloads/index.html Oracle JDK/JSE] (and not just the JRE) so that Java 7 or 8 becomes available to the command-line tools (type <tt>java -version</tt> to check which version is used by default for command-line tools; see also [http://stackoverflow.com/questions/21964709/how-to-set-or-change-the-default-java-jdk-version-on-os-x this discussion on StackOverflow]).
In case you have trouble starting the Java parser you can now set the <code>JAVA_PATH</code> preference of ProB to point to the <code>java</code> tool (or java.exe on Windows).
In case you have trouble starting the Java parser you can now set the <tt>JAVA_PATH</tt> 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):
To check whether ProB can correctly use its Java parser you can type the following (using probcli.exe on Windows):
Line 121: Line 172:
This will try and start the parser and obtain the parser version.
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.
In case Java is not correctly installed you should get an error message.
On Windows, you may see the error message
<tt>Error occurred during initialization of VM</tt>
on the console. This means you should probably [http://stackoverflow.com/questions/11808829/jre-1-7-returns-java-lang-noclassdeffounderror-java-lang-object re-install the Java JRE with admin rights] and try again.
If you see the error message
If you see the error message
  <tt>Unsupported major.minor version 51.0</tt>
  <tt>Unsupported major.minor version 52.0</tt>
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:
this means you do not have Java 8 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
  probcli -p JAVA_PATH path/to/java -version -v


== Tcl/Tk Requirements for ProB Tcl/Tk==
== Tcl/Tk Requirements for ProB Tcl/Tk ==
 
ProB Tcl/Tk requires an installation of Tcl/Tk 8.5 or Tcl/Tk 8.6. The command-line tool probcli does <b>not</b> require this.
 
=== Tcl/Tk on macOS ===
Important note: macOS comes pre-installed with a version of Tcl/Tk which is broken.
This may result in the display of unreadable <b>black windows</b> or crashes in the standard file dialogs.
There are various options to install Tcl/Tk:
* with Homebrew using the [https://formulae.brew.sh/formula/tcl-tk tcl-tk formula]
* with [https://ports.macports.org/port/tcl/ MacPorts]
* use the  [http://www.activestate.com/activetcl/downloads/ ActiveTcl version of Tcl/Tk]
You should probably start ProB using the <tt>StartProB.sh</tt> script: it will auto-detect Tcl/Tk versions and set the SP_TCL_DSO environment variable.
Below are more details:
 
==== Tcl/Tk from Homebrew or MacPorts ====
 
You can install a newer Tcl/Tk (e.g., 8.6.13) using [https://brew.sh <b>Homebrew</b>] or [https://www.macports.org <b>MacPorts</b>].
Note: In the earlier release 8.6.11 [https://bugs.python.org/issue44828 file open and file save dialogs will not work].
For Homebrew the command to install the[https://formulae.brew.sh/formula/tcl-tk tcl-tk formula] is:
<pre>
brew install tcl-tk
</pre>


ProB Tcl/Tk requires an installation of Tcl/Tk 8.5. The command-line tool probcli does <b>not</b> require this.
However, as the location of the libraries is not standard, you have to define the variable <tt>SP_TCL_DSO</tt>.
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).
The <tt>StartProB.sh</tt> script should set SP_TCL_DSO automatically.
You can also define and export this variable yourself 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):
<pre>
export SP_TCL_DSO=/usr/local/Cellar/tcl-tk/8.6.13_5/lib/libtcl8.6.dylib
</pre>
If you have uses MacPorts the path is probably <tt>/opt/local/lib/libtcl.dylib</tt>.
You can also set the variable by adding <tt>-DSP_TCL_DSO=/usr/local/Cellar/tcl-tk/8.6.12/lib/libtcl8.6.dylib</tt> to the command starting ProB. You may also have to install <tt>tk-table</tt> package yourself (it is bundled with Active Tcl).


=== Tcl/Tk on Mac OS/X ===
==== Active Tcl ====
Note:  for Mac OS you may have to install [http://www.activestate.com/activetcl/downloads/ the ActiveTcl version of Tcl/Tk] (e.g., [http://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ 8.5.18.0]) 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 [http://bugs.python.org/issue15853 8.5.12 has a serious bug related to copying text], see also [http://sourceforge.net/tracker/?func=detail&aid=3555211&group_id=12997&atid=112997_type here]).
 
This issue has been fixed in version 8.5.13 or later.
The [http://www.activestate.com/activetcl/downloads/ the ActiveTcl version of Tcl/Tk] is automatically recognised by ProB and you do not have to set <tt>SP_TCL_DSO</tt>.
 
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.
The older ersion [http://bugs.python.org/issue15853 8.5.12 has a bug related to copying text], see also [http://sourceforge.net/tracker/?func=detail&aid=3555211&group_id=12997&atid=112997_type here]).
 
 
==== Other Notes ====
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 "<tt>macOS 11 or later required !</tt>"  in the terminal when launching <tt>prob</tt> you should re-install Tcl/Tk as described above.


=== Tcl/Tk on Windows ===
=== Tcl/Tk on Windows ===
Starting with ProB 1.3.5 you can now use ProB with Tcl/Tk 8.5 on Windows. If you have the older
We currently provide two downloads of ProB, one for Tcl/Tk 8.6 (which we recommend)
version of Tcl/Tk 8.4 you have to install the newer one
and a version for Tcl/Tk 8.5.
8.5 (you should be able to also keep the older version). For Windows we recommend installing [http://downloads.activestate.com/ActiveTcl/releases/ ActiveTcl-8.5] (e.g., [http://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ 8.5.18.0]).  
You can use for example the [https://www.activestate.com/products/tcl/ ActiveTcl releases].
Note: For the 64 bit version of ProB for Windows, you have to install the 64 bit Tcl/Tk 8.5 version!
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.
ProB 1.12 (currently available as nightly build) works with both Tcl/Tk 8.5 and 8.6.
You may have to point the environment variable SP_TCL_DSO to the correct DLL before starting ProB. For Tcl/Tk 8.5 this is typically
base-tcl8.5-thread-win32-x86_64.dll.
You can either go to System -> Settings -> Advanced -> Environment Variables
or use the setx command for this:
<pre>
setx SP_TCL_DSO C:\Tcl\bin\base-tcl8.5-thread-win32-x86_64.dll
</pre>


=== Tcl/Tk on Linux ===
=== Tcl/Tk on Linux ===
On Linux you can typically install Tcl/Tk using <tt>sudo apt-get install tcl8.5 tk8.5</tt>.
On Linux you can typically install Tcl/Tk using <tt>sudo apt-get install tcl8.5 tk8.5</tt>.
On very recent Linux systems (such as Ubuntu 20.04) you may want to download (and compile) [https://www.tcl.tk/software/tcltk/downloadnow85.html Tcl/Tk 8.5] or use [https://ubuntu.pkgs.org/18.04/ubuntu-universe-amd64/tcl8.5_8.5.19-4_amd64.deb.html packages from earlier releases].
On Linux OpenSuse (12.3) you may have to perform the following for ProB to work:
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/libtk8.5.so /usr/lib/libtk8.5.so.0
Line 155: Line 249:
Finally, support for .png ANIMATION_IMG declarations requires the Img package:
Finally, support for .png ANIMATION_IMG declarations requires the Img package:
  sudo apt install libtk-img
  sudo apt install libtk-img


== Graphviz Requirements ==
== Graphviz Requirements ==


If you wish to view various visualizations generated by ProB Tcl/Tk or probcli you will need [http://www.graphviz.org/ GraphViz]. ProB may use the command-line tool <tt>dot</tt>, a dot-file viewer such as <tt>dotty</tt> or more recently the command-line tool <tt>sfdp</tt>.
If you wish to view various visualizations generated by ProB Tcl/Tk or probcli you will need [http://www.graphviz.org/ GraphViz].
ProB may use the command-line tool <tt>dot</tt> and a dot-file viewer such as <tt>dotty</tt> (optionally in ProB Tcl/Tk).


On Mac you can now install the latest version of Graphviz using brew:
On Mac, the only working application to view dot files is [https://ports.macports.org/port/graphviz-gui/ graphviz-gui] by [https://www.macports.org MacPorts]. To install the application do this
* <tt>sudo port install graphviz-gui</tt>
The viewer can now be found in /Applications/MacPorts/Graphviz.app (you may have to set the ProB graphical viewer preference <tt>dot_viewer</tt> to this path).
Some ProB commands work directly with the command-line tool <tt>dot</tt> which you can install with MacPorts like this:
* <tt>sudo port install graphviz</tt>
On Mac you can now install the latest version of Graphviz using [https://brew.sh HomeBrew]:


  1. <tt>brew uninstall graphviz</tt>
  1. <tt>brew uninstall graphviz</tt>
Line 171: Line 270:
This is probably better than using the [http://www.pixelglow.com/graphviz/ older version from Pixelglow].
This is probably better than using the [http://www.pixelglow.com/graphviz/ 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).
On macOS you should probably select Preferences -> Graphical Viewer -> PDF within ProB Tcl/Tk, as currently all GraphViz viewer applications seem to crash on current macOS systems.
ProB 1.8.1 only uses the dot binary, making use of the -Ksfdp option.


== Sourcecode ==
You can also manually set the DOT (path_to_dot) preference if ProB cannot find the Graphviz dot binary you have installed.  
You can download the latest Prolog sourcecode snapshot from: [http://www3.hhu.de/stups/downloads/prob/source/ http://www3.hhu.de/stups/downloads/prob/source/]


The source code for the ProB parsers (B, LTL, ...) can be obtained from: [https://github.com/bendisposto/probparsers https://github.com/bendisposto/probparsers].
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.


The ProB2-Java-API source code can be obtained from: [https://github.com/bendisposto/prob2 https://github.com/bendisposto/prob2].
== Short Release History ==


The ProB2-Java-FX UI source code can be obtained from:
The full  [[ProB_Release_History | ProB release history can be found here]].
[https://github.com/bendisposto/prob2-ui https://github.com/bendisposto/prob2-ui].


== Short Release History ==
'''2024-02-20'''
[[Download|ProB 1.13.0]] is available. Better Rodin theory support. Template strings. Unicode improvements. READ_JSON and other new external functions. VisB support for groups and "use" element. [[Monte_Carlo_Tree_Search_Game_Play|MCTS game play]].
 
'''2024-02-03'''
[[Download|ProB 1.12.2-fix1]] is available.
 
'''2023-08-10'''
[[Download|ProB 1.12.2]] is available. [[VisB#VisB_DEFINITIONS_2 |VisB]] improvements.
 
'''2023-04-04'''
[[Download|ProB 1.12.0]] is available. Call stack infos, performance improvements in parser and solver,  new [[LTL_Model_Checking#Supported_Syntax |LTL]] operators, [[VisB#VisB_Additional_SVG_Objects|VisB]] improvements, reals/floats for [[Event-B_Theories|Rodin theories]].
 
'''2021-12-29'''
[[Download|ProB 1.11.1]] is available. Highlights: identifiers between backquotes, flexible JSON trace replay, DPLLT solving command, improvements to Z3 backend.
 
'''2021-10-06'''
[[Download|ProB 1.11.0]] is available. Highlights: 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.
 
'''2020-12-15'''
[[Download|ProB 1.10.0]] is available. Highlights: well-definedness prover, REAL datatype, -lint comand for VSCode and Atom, improved unsat core and error messages.
 
'''2020-02-19'''
[[Download|ProB 1.9.3]] is available. Highlights: performance improvements, new external functions, performance monitoring.
 
'''2019-11-11'''
[[Download|ProB 1.9.2]] is available. Minor bugfix release.
 
'''2019-11-08'''
[[Download|ProB 1.9.1]] is available. Maintenance release.


'''12/7/2019'''
'''2019-07-12'''
[[Download|ProB 1.9.0]] is available. Highlights: improved error feedback, improved Unicode support, regular expression library, memoization.
[[Download|ProB 1.9.0]] is available. Highlights: improved error feedback, improved Unicode support, regular expression library, memoization.


'''1/10/2018'''
'''2018-10-01'''
[[Download|ProB 1.8.2]] is available. Highlights: improved error feedback, support [https://gitlab.cs.uni-duesseldorf.de/dgelessus/prob2-jupyter-kernel Jupyter kernel], first [[Alloy|support for Alloy models]].
[[Download|ProB 1.8.2]] is available. Highlights: improved error feedback, support [https://gitlab.cs.uni-duesseldorf.de/general/stups/prob2-jupyter-kernel Jupyter kernel], first [[Alloy|support for Alloy models]].


'''20/03/2018'''
'''2018-03-20'''
[[Download|ProB 1.8.0]] is available. Highlights: terminal colour support, performance improvements for displaying very large values, improved symmetry breaking and constraint solving.
[[Download|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'''
'''2017-10-05'''
[[Download|ProB 1.7.1]] is available. Highlights: performance, non-deterministic assigned variables shown, Z improvements, export history to HTML.
[[Download|ProB 1.7.1]] is available. Highlights: performance, non-deterministic assigned variables shown, Z improvements, export history to HTML.


'''11/7/2017'''
'''2017-07-11'''
[[Download|ProB 1.7.0]] is available. Highlights: improved [[Generating_Documents_with_ProB_and_Latex |Latex document generation]], improved XML/CSV data import and export, RULE DSL language, many improvements in constraint solver.
[[Download|ProB 1.7.0]] is available. Highlights: improved [[Generating_Documents_with_ProB_and_Latex |Latex document generation]], improved XML/CSV data import and export, RULE DSL language, many improvements in constraint solver.


'''20/10/2016'''
'''2016-10-20'''
[[Download|ProB 1.6.1]] is available. Highlights: [[Generating_Documents_with_ProB_and_Latex |Latex document generation]], LET and IF-THEN-ELSE for expressions and predicates, XML logging, XML data import, performance improvements.
[[Download|ProB 1.6.1]] is available. Highlights: [[Generating_Documents_with_ProB_and_Latex |Latex document generation]], LET and IF-THEN-ELSE for expressions and predicates, XML logging, XML data import, performance improvements.


'''22/4/2016'''
'''2016-04-22'''
[[Download|ProB 1.6.0]] is available. Highlights: [[Tutorial_Directed_Model_Checking|directed model checking]], [[Using_ProB_with_Z3|Z3 available as backend]], B line comments and unicode symbols, improved error messages, performance improvements.
[[Download|ProB 1.6.0]] is available. Highlights: [[Tutorial_Directed_Model_Checking|directed model checking]], [[Using_ProB_with_Z3|Z3 available as backend]], B line comments and unicode symbols, improved error messages, performance improvements.


'''19/2/2015'''
'''2015-02-19'''
[[Download|ProB 1.5.0]] is available. Highlights: improved random enumeration, MACE/SEM style static symmetry reduction for deferred set elements, [[State_Space_Coverage_Analyses|MC/DC coverage]] analysis for guards and invariants, [[TLC|improved TLC interface]], bug fixes and improvements including but not limited to the constraint solver.
[[Download|ProB 1.5.0]] is available. Highlights: improved random enumeration, MACE/SEM style static symmetry reduction for deferred set elements, [[State_Space_Coverage_Analyses|MC/DC coverage]] analysis for guards and invariants, [[TLC|improved TLC interface]], bug fixes and improvements including but not limited to the constraint solver.


'''29/8/2014'''
'''2014-08-29'''
[[Download|ProB 1.4.1]], a small bugfix-only release is available. For a list of new features in 1.4.0 see below.
[[Download|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'''
'''2014-08-18'''
[[Download|ProB 1.4.0]] is available. Highlights: CLP(FD)-based constraint solver enabled by default, kernel can handle more operations symbolically, [[TLC|integration of the TLC model checker]], bug fixes and performance improvements.
[[Download|ProB 1.4.0]] is available. Highlights: CLP(FD)-based constraint solver enabled by default, kernel can handle more operations symbolically, [[TLC|integration of the TLC model checker]], bug fixes and performance improvements.


'''4/3/2013'''
'''2013-03-04'''
[[Download|ProB 1.3.6]] is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, [[Using_ProB_with_KODKOD | improved Kodkod backend]] and use within REPL, and many more.
[[Download|ProB 1.3.6]] is available. Highlights: improved constraint propagation for division, modulo, intervals, model checking progress bar, performance improvements, [[Using_ProB_with_KODKOD | improved Kodkod backend]] and use within REPL, and many more.


'''8/10/2012'''
'''2012-10-08'''
[[Download|ProB 1.3.5]] is available. Highlights: support for external and recursive functions, optional Kodkod backend, [[TLA|TLA+ support]], performance improvements, pragmas, units inference, and many more.
[[Download|ProB 1.3.5]] is available. Highlights: support for external and recursive functions, optional Kodkod backend, [[TLA|TLA+ support]], performance improvements, pragmas, units inference, and many more.


'''30/03/2012'''
'''2012-03-30'''
A first prototype of an online [[ProB_Logic_Calculator|ProB Logic Calculator]] is available.
A first prototype of an online [[ProB_Logic_Calculator|ProB Logic Calculator]] is available.


'''21/11/2011'''
'''2011-11-21'''
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.
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'''
'''2011-02-10'''
ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more.
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'''
'''2010-07-30'''
ProB 1.3.2 is available. Highlights: improved performance, constraint solving over integers (enable in Advanced Preferences), much improved Z support, and many more.
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'''
'''2009-12-07'''
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.
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'''
'''2009-03-20'''
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.
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 | ProB release history can be found here]].

Latest revision as of 10:31, 1 July 2024

Latest Release

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. The list of changes can be found in the ProB release history.

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 Dependencies
1.13.0
Linux 20.2.2024 Tarball
Java 8 or newer (see below), Tcl/Tk 8.5 or 8.6 (see below), GraphViz
Windows 20.2.2024 Zipfile (Tcl/Tk 8.6),
Zipfile (Tcl/Tk 8.5)
Tcl/Tk 8.5 or 8.6 (see below), Java 8 or newer (see below), GraphViz, Windows Installation Instructions
macOS 20.2.2024 Zipfile (Universal ARM/Intel notarized)

Homebrew Tap

macOS 10.14 (Mojave) or newer, Tcl/Tk (see below), Java 8 or newer (see below), Graphviz (see below)

The B parser of ProB requires Java 8 or newer. More details are available below.

The Graphical User Interface of ProB Tcl/Tk requires Tcl/Tk 8.5 or 8.6. More details are available below. The default Tcl/Tk on macOS is broken and will result in black windows, and you have to install another version of Tcl/Tk. All releases include the command-line version probcli which does not require Tcl/Tk.

Releases are compiled for the x86_64 architecture (64-bit Intel). macOS releases of ProB 1.12.0 and later also support aarch64 (64-bit ARM/Apple Silicon). The last version built for x86 (32-bit Intel) is ProB 1.8.0 (see prior versions). If you are using an unsupported architecture or system, you may still be able to run ProB from source.

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.

Latest Beta Release

The latest beta release is 1.13.1-beta1. 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.

Nightly Builds

More current nightly integration builds are also available. These releases are usually updated every night and old versions are not stored.

Note for macOS users: Nightly builds of ProB are not signed or notarized, so macOS 10.15 and later (Catalina, Big Sur or Monterey, Ventura) will refuse to run them. As a workaround, you will need to run xattr -r -d com.apple.quarantine * inside the ProB directory before launching ProB. The stable and beta releases listed above are signed and notarized, so they will run without extra steps.

Automatically generated test coverage reports are also available. They are usually updated once per week.

Sourcecode

You can download the latest Prolog sourcecode snapshot from: https://stups.hhu-hosting.de/downloads/prob/source/

The source code for the ProB parsers (B, LTL, ...) can be obtained from: https://github.com/hhu-stups/probparsers

Prior Versions

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.

Other ProB tools

ProB Jupyter Kernel

You can now create Jupyter Notebooks in B using the ProB Jupyter kernel. Downloads, instructions, and source code can be found on its own page.

You can try out the ProB Jupyter kernel in your browser without installing it first. Note that notebooks are not saved permanently in this online version! To keep your notebooks, you must download them before closing the page.

ProB for Rodin

To install ProB for Rodin, first download a current version of Rodin (e.g., Rodin 3.8). Inside Rodin, choose Help -> Install New Software and choose the pre-configured ProB update site.

More detailed installation instructions and a brief tutorial are available.

ProB2-UI (based on JavaFX)

Version 1.2.1 of the new JavaFX-based ProB2-UI is available. See the release history for what's new. You can use these stand-alone versions which come bundled with the right Java runtime environment:

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 (Windows, macOS, Linux).

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 (1.2.2-SNAPSHOT) are also available:

The source code for ProB2-UI is available at https://github.com/hhu-stups/prob2_ui and can be built by following these instructions.

The underlying ProB Java API of ProB2-UI (aka the ProB 2 kernel) is available to Java developers via Maven Central. Its source code can be obtained from: https://github.com/hhu-stups/prob2_kernel.

macOS issues

When you run the macOS app for the first time, you might have to open the app twice for ProB 2 UI to start properly. This should only happen once.

The ProB 2 UI macOS app releases are signed and notarized, so they should run without issues on current macOS versions. However, the multi-platform jar and snapshot app builds are not signed or notarized, so newer macOS versions will refuse to run them or say that the application is damaged. As a workaround, right-click the app, select "Open", and confirm the security dialog. If the dialog still doesn't give you an option to open the app, click "Cancel" and do the same thing again.

To run the multi-platform jar on macOS, we recommend using Java 15 or later. Older Java/JavaFX versions may lead to an incorrect system font resulting in gibberish text display. Alternatively, use the macOS app build, which comes with Java 17 and does not have this issue.

Editor Support

Java Requirements for B Parser

The B parser of ProB requires Java 8 or newer. Java 11, 17, etc. are also fully supported. ProB 1.9.3 is the last version to support Java 7. ProB 1.5.0 is the last version to support Java 6.

You can install a Java Runtime Environment (JRE) from various sources, such as Eclipse Adoptium, Azul Zulu, or your system package manager.

Note: on some systems (macOS) you may have to install the full Java Development Kit (JDK), and not just the JRE, so that Java 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. If you see the error message

Unsupported major.minor version 52.0

this means you do not have Java 8 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

Tcl/Tk Requirements for ProB Tcl/Tk

ProB Tcl/Tk requires an installation of Tcl/Tk 8.5 or Tcl/Tk 8.6. The command-line tool probcli does not require this.

Tcl/Tk on macOS

Important note: macOS comes pre-installed with a version of Tcl/Tk which is broken. This may result in the display of unreadable black windows or crashes in the standard file dialogs. There are various options to install Tcl/Tk:

You should probably start ProB using the StartProB.sh script: it will auto-detect Tcl/Tk versions and set the SP_TCL_DSO environment variable. Below are more details:

Tcl/Tk from Homebrew or MacPorts

You can install a newer Tcl/Tk (e.g., 8.6.13) using Homebrew or MacPorts. Note: In the earlier release 8.6.11 file open and file save dialogs will not work. 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. The StartProB.sh script should set SP_TCL_DSO automatically. You can also define and export this variable yourself 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.13_5/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).

Active Tcl

The the ActiveTcl version of Tcl/Tk is automatically recognised by ProB and you do not have to set SP_TCL_DSO.

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. The older ersion 8.5.12 has a bug related to copying text, see also here).


Other Notes

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.

Tcl/Tk on Windows

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! ProB 1.12 (currently available as nightly build) works with both Tcl/Tk 8.5 and 8.6. You may have to point the environment variable SP_TCL_DSO to the correct DLL before starting ProB. For Tcl/Tk 8.5 this is typically base-tcl8.5-thread-win32-x86_64.dll. You can either go to System -> Settings -> Advanced -> Environment Variables or use the setx command for this:

setx SP_TCL_DSO C:\Tcl\bin\base-tcl8.5-thread-win32-x86_64.dll

Tcl/Tk on Linux

On Linux you can typically install Tcl/Tk using sudo apt-get install tcl8.5 tk8.5.

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.

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

Graphviz Requirements

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

  • sudo port install graphviz-gui

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:

  • sudo port install graphviz

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.

On macOS you should probably select Preferences -> Graphical Viewer -> PDF within ProB Tcl/Tk, as currently all GraphViz viewer applications seem to crash on current macOS systems.

You can also manually set the DOT (path_to_dot) preference if ProB cannot find the Graphviz dot binary you have installed.

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.

Short Release History

The full ProB release history can be found here.

2024-02-20 ProB 1.13.0 is available. Better Rodin theory support. Template strings. Unicode improvements. READ_JSON and other new external functions. VisB support for groups and "use" element. MCTS game play.

2024-02-03 ProB 1.12.2-fix1 is available.

2023-08-10 ProB 1.12.2 is available. VisB improvements.

2023-04-04 ProB 1.12.0 is available. Call stack infos, performance improvements in parser and solver, new LTL operators, VisB improvements, reals/floats for Rodin theories.

2021-12-29 ProB 1.11.1 is available. Highlights: identifiers between backquotes, flexible JSON trace replay, DPLLT solving command, improvements to Z3 backend.

2021-10-06 ProB 1.11.0 is available. Highlights: 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.

2020-12-15 ProB 1.10.0 is available. Highlights: well-definedness prover, REAL datatype, -lint comand for VSCode and Atom, improved unsat core and error messages.

2020-02-19 ProB 1.9.3 is available. Highlights: performance improvements, new external functions, performance monitoring.

2019-11-11 ProB 1.9.2 is available. Minor bugfix release.

2019-11-08 ProB 1.9.1 is available. Maintenance release.

2019-07-12 ProB 1.9.0 is available. Highlights: improved error feedback, improved Unicode support, regular expression library, memoization.

2018-10-01 ProB 1.8.2 is available. Highlights: improved error feedback, support Jupyter kernel, first support for Alloy models.

2018-03-20 ProB 1.8.0 is available. Highlights: terminal colour support, performance improvements for displaying very large values, improved symmetry breaking and constraint solving.

2017-10-05 ProB 1.7.1 is available. Highlights: performance, non-deterministic assigned variables shown, Z improvements, export history to HTML.

2017-07-11 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.

2016-10-20 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.

2016-04-22 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.

2015-02-19 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.

2014-08-29 ProB 1.4.1, a small bugfix-only release is available. For a list of new features in 1.4.0 see below.

2014-08-18 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.

2013-03-04 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.

2012-10-08 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.

2012-03-30 A first prototype of an online ProB Logic Calculator is available.

2011-11-21 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.

2011-02-10 ProB 1.3.3 and ProB for Rodin 2.3 is available. Highlights: improved performance, constrained-based deadlock checking, record detection, and many more.

2010-07-30 ProB 1.3.2 is available. Highlights: improved performance, constraint solving over integers (enable in Advanced Preferences), much improved Z support, and many more.

2009-12-07 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.

2009-03-20 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.