Sunday, February 13, 2011

the release of ProB for Rodin 2.1

We are happy to announce the release of 
    ProB for Rodin 2.1

Numerous improvements went into the latest release:
- constraint-based deadlock checker: finds counter-examples
to the deadlock freedom
PO using constraint-solving
- improved kernel with improved constraint solving
(in particular improved boolean
constraint solver)
- ProB can now efficiently solve integer constraints
using the finite domain solver
CLP(FD) (you can turn this feature on in 
the Preferences Dialog)
- improved LTL model checker with new counter-example display
- new, improved version of BMotionStudio to generate
graphical visualisations of
your models
- automatic record detection (when defining closed
records using Records plug-in or
manually using bijections on Cartesian products)
- 64-bit version of ProB for Mac OS X (performance
improvement; less hash collisions
in model checking; larger range for the integer 
constraint solver; ...)
- and many more.

To install ProB, first download Rodin 2.1, 
choose Help -> Install New Software and
simply choose the pre-configured ProB update site.
More detailed installation instructions and a brief 
tutorial can be found here:

We have also released the new version 1.3.3 of ProB 
Classic, a version of ProB with
a Tcl/Tk interface.
It can be obtained at:
ProB Classic, is a stand-alone application but can
be started automatically from
within Rodin by setting the ProB Classic preference.
ProB Classic provides some features which are not
yet available in the ProB for
Rodin version
(graphical visualisation of the state space, 
debugging of axioms with unsat core
computation, CSP support...).

Kind regards,
The ProB Team from Düsseldorf

No comments: