Handbook/General

Revision as of 11:50, 14 June 2021 by David Geleßus (talk | contribs) (Created page with "__TOC__ = Installation = {{:Installation}} = Windows Installation Instructions = {{:Windows Installation Instructions}} = Editors for ProB = {{:Editors for ProB}}")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Installation

Which version should I use?

See our homepage for an overview of the available versions of ProB. All ProB tools can be downloaded from our Download page.

The standalone version Tcl/Tk 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. Use the probcli version if you want to write batch scripts or prefer working from the command-line.

Installation Instruction for ProB (Standalone)

Note: we have specific Windows_Installation_Instructions. These here are the generic instructions.

  • 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

On Windows, you will also have a subfolder called "Microsoft.VC80.CRT" containing the DLLs for the C runtime. Also, the binary is called "ProBWin" and not "prob".

With the latest version of ProB, you have to install Tcl/Tk version 8.5. For example, you can find a correct version of Tcl/Tk athttp://downloads.activestate.com/ActiveTcl/releases/8.5.18.0/ .

  • To load your own B machines you also need Java 7 or newer runtime or better JDK.
  • 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 visualize the graphs, but postscript viewers (such as gv) are also supported. 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 initialize the machines and animate them. Have a look at the supplied Machines in the examples directory. Have fun ! Please report bugs!

Checklist/Troubleshooting

  • Java: be sure to have Java 7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.
  • Tcl/Tk: be sure to have a suitable version of TclTk installed. In

general you should install at least 8.5. You also need the 64 bit version of Tcl/Tk for 64 bit versions of ProB.

  • GraphViz: in order to make use of the graphical visualization features, you need to install a version of GraphViz suitable for your architecture. Then use the command "Graphical Viewer Preferences..." in the Preferences Menu to set or check the following preferences:
    • Path/Command for dot program
    • Path/Command for dot viewer (e.g., dotty)

Note: you can use the "Pick" button to locate the dot program and the dot viewer. See more information about the Graphical Viewer here.

Windows Installation Instructions

Windows Specific Download Instructions


Go to the ProB Downloads site

  • Go to the page Download, this should look as follows:
ProBWindowsDownload.png

Install Tcl/Tk 8.5

If Tcl/Tk 8.5 is already installed you can skip this step.

  • Click on the "Tcl/Tk 8.5 for Windows," link provided in the "Dependencies" column and the "Windows" row above
  • Choose the most recent Tcl/Tk 8.5 distribution available for windows; be sure to choose a version matching ProB, e.g. a 32-bit version (the file highlighted in blue below) if you want to use the 32-bit version of ProB.
  • Download and follow the installation instructions
TkWindowsDownload.png

Install Java

If Java 7 or newer is already installed you can skip this step.

Download the ProB for Windows Zipfile

  • Click on the "Zipfile (with probcli)" link in the Download column and Windows row
  • 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)! The contents of the ProB directory should look something like this:
ProBWindowsFolder.png

The subfolder called "Microsoft.VC80.CRT" contains the DLLs for the Microsoft C runtime.

Optionally Download GraphViz

Start ProB

  • Start ProB by double-clicking on the ProBWin icon above
  • Try to open some of the examples provided in the Examples folder shown above
  • Contact us if you have problems

Checklist/Troubleshooting

  • Java: be sure to have Java 1.7 or newer installed. Otherwise you will not be able to parse your own classical B machines as our parser is written in Java.
  • Tcl/Tk: be sure to have a matching version of TclTk 8.5 installed
  • Try starting ProBWin or probcli from the Windows Command Prompt; the error messages may help you or us uncover the problem
  • You can also try and obtain information from the main Windows Event/Error Log, by following these steps:
    • Click Start, and then click Control Panel.
    • Click Performance and Maintenance, then click Administrative Tools, and then double-click Computer Management. Or, open the MMC containing the Event Viewer snap-in.
    • In the console tree, expand Event Viewer, and then click the log that contains the event that you want to view.
    • In the details pane, double-click the event that you want to view.
    • The Event Properties dialog box containing header information and a description of the event is displayed.

Editors for ProB

ProB Tcl/Tk Editor

ProB Tcl/Tk contains an editor in which syntax errors are displayed and which can be used to edit B, CSP, Z and TLA+ models. The editor of Tcl/Tk, however, has a few limitations:

  • it can become very slow with long or very long lines
  • the syntax highlighting can become slow with very large files. Hence, syntax highlighting is automatically turned off in some circumstances (when more than 50,000 characters are encountered or when a line is longer than 500 characters).

It is possible to open the files in an external editor. You can setup the editor to be used by modifying the preference "Path to External Text Editor" in the "Advanced Preferences" list (available in the "Preferences" menu). You can then use the command "Open FILE in external editor" in the "File" menu to open your main specification file with this editor. You can also use the command-key shortcut "Cmd-E" for this.

Launching the editor in probcli

The probcli REPL (read-eval-print-loop) supports the command :e to open the current file in the external editor, as specified in the "EDITOR" preference. You can set this preference using

probcli -repl -p EDITOR PATH

In case errors occurred with the last command, this will also try and move the cursor to the corresponding location in the file.

External Editors

VIM

A VIM plugin for ProB is available. It shows a quick fix list of parse and type errors for classical B machines (.mch) using the command line tool probcli. VIM has builtin syntax highlighting support for B.

VSCode

There is a package called B/ProB Language Support available for the VSCode editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to VSCode. It integrates with probcli to obtain error markers for syntax and type errors. It can also be used for well-definedness checking.

Atom

There is a package language-b-eventb available for the Atom editor. It adds syntax highlighting and snippets for the specification languages B and Event-B to Atom. It integrates with probcli to obtain error markers for syntax and type errors.

With the Atom plugin you can now also visualize WD (well-definedness) issues in your B machines. See this small demo video.

Note that Atom is no longer being updated as of December 2022.

BBEdit

Some BBedit Language modules for B, TLA+, CSP and Prolog are available.

Emacs

A package File:B-mode.el.zip is available.