Which version shall I use?
The standalone version of ProB contains a richer set of features than the Rodin version and also works on other formalisms than Event-B (e.g., classical B, Z, CSP, B||CSP, Promela, ...). If you want to do animation and model checking of Event-B models, the Rodin version might be enough. The Rodin version contains a translation tool from Rodin into Event-B package files that can be used within the standalone version of ProB.
Installation Instruction for ProB (Standalone)
- Obtain your platform specific ProB distribution from Downloads. Decompress and expand the ProB directory if necessary. Do not change the location and structure of the files and directories within ProB (apart from the Machines directory) ! On Windows you just have to double-click the installer. The contents of the ProB directory should look something like this:
examples lib prob
StartProB.sh tcl
- Be sure that you have Tcl/Tk installed (see, e.g., http://www.tcl.tk/software/tcltk/). With the latest version of ProB you have to install Tcl/Tk version 8.4 (for some versions of ProB even 8.5)! For Windows you can find a correct version of Tcl/Tk at http://downloads.activestate.com/ActiveTcl/Windows/8.4.8/ The Mac version needs Tcl/Tk 8.5 or higher (http://www.tcl.tk/software/tcltk/8.5.html/).
- To load your own B machines you also need Java runtime installed (http://java.sun.com/j2se/index.jsp or directly to http://java.sun.com/javase/downloads/index.jsp to download the standard edition 5.0; on Mac and Linux Java is probably already installed).
- Note: you can skip this step if you do not wish to use the visualization commands. Install the "dot" program and "dotty" viewer from AT&T's Graphviz package (http://www.graphviz.org/ or http://www.research.att.com/sw/tools/graphviz/). By default, ProB will open the "dotty" program to visualise the graphs, but postscript viewers are also supported (such as gv). So, you do not need to install dotty if you don't want to; but it is probably easiest to install the entire Graphviz package.
- Change to the ProB directory and then start up prob. In Windows you can simply double-click on the ProBWin Application. On Mac OS X you may have to type 'limit data unlimited' (in tcsh) or 'ulimit -d unlimited' (in bash) before launching ProB using the Terminal Application. The distribution contains a script StartProB.sh which does this for you (note you may have to do chmod u+x StartProB.sh before launching it from the command-line).
- Now you should be able to open some of the B Machines in the Machines directory. You should then be able to initialise the machines and animate them. Have a look at the supplied Machines in the examples directory. Have fun ! Please report bugs!
Installation Instruction for ProB (Rodin Plugin)
The interactive movie shows hot to install the ProB Rodin Plugin.
<swf width="800" height="600">Install.swf</swf>