Revision as of 17:17, 18 January 2010 by Jens Bendisposto(talk | contribs)(Created page with 'Category:User Manual * Avoid installing ProB in a path with spaces or other special characters in them. The same holds for B machines you wish to analyse with ProB. * You ne…')
Avoid installing ProB in a path with spaces or other special characters in them. The same holds for B machines you wish to analyse with ProB.
You need Tcl/Tk (preferably 8.4 or newer) installed on your machine. On Linux you will get the error message: ./prob: error while loading shared libraries: libtk.so: cannot open shared object file: No such file or directory if Tcl/Tk is not proberly installed. You can get Tcl/Tk at http://www.tcl.tk/software/tcltk/.
For the very latest version of ProB (1.2.0 or newer) you need a Java 1.5 Runtime environment or newer (you will get a message "Could not execute parser." with "Error: java.lang.UnsupportedClassVersionError" when opening a machine). You can obtain Java at http://java.sun.com/j2se/index.jsp.
On Mac OS X, if you have trouble opening larger B machines this may be due to Mac OS X giving too little memory to ProB. Use 'limit data unlimited' (in tcsh) or 'ulimit -d unlimited' (in bash) before launching ProB from the command line.
ProB prior to version 1.3.0 may require more typing information than AtelierB, B4Free or the BToolkit. It is usually good style to explicitly type all variables and parameters. Hint: avoid using the same variable name for different variables (e.g., in two different set comprehensions). This way you will know which variable ProB is referring to in error messages. As of version 1.3.0 ProB performs full type inference and checking, using a unification based algorithm, which is more powerful than the type inference in the other B tools.