General Presentation (tcl/tk)

The ProB Main Window

The menu bar contains the various commands to access the features of ProB. It includes the traditional File menu, with a submenu Recent Files to quickly access the files previously opened in ProB. Notice the two couples of commands Open\Save and Reopen\Save and Reopen, the latter reopening the currently opened file and reinitialising completely the state of the animation and the model checking processes. The About menu provides help on the tool, including a command to check if an update is available on the ProB website. By default, ProB starts with a limited set of commands in the Beginner mode. The Normal mode gives access to more features and can be set in the menu Preferences|User Mode.

Under the menu bar, the main window contains four panes:

• In the top pane, the specification of the B machine is displayed with syntax highlight, and can also be edited by typing directly in this pane;
• At the bottom, the animation window is composed of three panes which display, at the current point during the animation:

1. The current state of the B machine (State Properties), listing the current values of the machine variables;
2. The enabled operations (Enabled Operations), listing the operations whose preconditions and guards are true in this state;
3. The history of operations leading to this state (History).