Download: Difference between revisions

No edit summary
Line 37: Line 37:
The Graphical User Interface of ProB Tcl/Tk requires Tcl/Tk 8.5.
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.
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 [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/3.1/ Rodin 3.1], choose Help -> Install New Software and simply choose the pre-configured ProB update site.
More [[http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_Rodin_First_Step | detailed installation instructions and a brief tutorial are available]].


== Prior Versions ==
== Prior Versions ==

Revision as of 14:01, 19 February 2015

Latest Release

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 is provided by the spin-off company Formal Mind. In particular, Formal Mind can also 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. 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

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.

Java Requirements for B parser

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).

Tcl/Tk Requirements for ProB Tcl/Tk

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. There is a version of ProB available for Tcl/Tk 8.6 on Mac OS X Lion.

Tcl/Tk on Mac OS/X

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.

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 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.

Tcl/Tk on Linux

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


Nightly Build

You can download our nightly integration build from here.

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://nightly.cobra.cs.uni-duesseldorf.de/rodin3/updatesite/.

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/.

Timed-CSP Simulator

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/

Sourcecode

You can download the latest sourcecode snapshot from: http://nightly.cobra.cs.uni-duesseldorf.de/source/

Short Release History

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.