Revision as of 15:50, 3 February 2021 by David Geleßus (talk | contribs) (Add missing troubleshooting item from prob2-doc)
  • On macOS Catalina the Tcl/Tk menu bar is sometimes not working. Switching to another application and then back to ProB seems to solve the problem.
  • Avoid installing ProB in a path with spaces or other special characters in them. The same holds for B machines you wish to analyze 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: cannot open shared object file: No such file or directory if Tcl/Tk is not proberly installed. You can get Tcl/Tk at
  • 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
  • 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.