Skip to main content
Department of Information Technology

Provably Correct Software, Spring -10

An introduction to using ProB

This introduction shows you how to use ProB, the tool we will be using to try out our B specifications during the course. This introduction will only cover the basic (and most important) functions. You'll find full documentation on the ProB web site.

Index

Running ProB

In the department, ProB must be run on a Windows system. ProB is installed and known to work on the PC workstations in room 1313. It may work on student PC machines in other lab rooms as well.

Open the application G:\Program\ProB_Win\ProBWin, e.g. by choosing START->My computer, then successively double-clicking on G:, Program, ProB_Win and ProbWin.

You can also download ProB to your own computer. Refer to the ProB web site.

After starting ProB, you should see something like this:

snapshot1.png

Changing preference settings

ProB works by showing actual states of your B specification. In each state every enabled operation instance (that is, every operation with arguments that satisfiy the precondition of the operation) are displayed. For this to work, the state space must be kept small. ProB limits things like the sizes of deferred sets, the maximum and minimum possible integers. Frequently you want to change these settings. Select Preferences -> Animation to open the preference settings window:

snapshot2.png

Change a setting by clicking on the appropriate line and modifying the value in the box (or klicking True or false False if it is a boolean setting).

Try this by changing

  • Max number of initialisations computed to 5
  • Size of unspecified deferred sets in SETS section to 3
  • MaxInt, ...... to 4

Clicking the Finished button when you are done.

It might seem pointless to have so small sets and ranges of integers, but it turns out that in practise surpringingly small numbers are sufficient to find problems with a specification.

Loading a machine

For this example, you should use the "better" specification of stacks from the course slides. You should store it in a file called Stack.mch.

Select File -> Open and locate Stack.mch. You should get a window like the following:

snapshot3.png

The machine is now in a "pseudo-state" before initialisation. We can e.g. see in the "State properties" pane that the size of the deferred set ELEMENTS is 3. Since ELEMENTS is an abstract set, ProB will populate it with the arbitrary elements ELEMENTS1, ELEMENTS2 and ELEMENTS3.

The "Enabled operations" has five enabled "pseudo-operations" each determining a particular value for the machine constant maxsize. By double-clicking SETUP_CONSTANTS(4) we tell ProB that we want maxsize to be 4.

snapshot4.png

The machine is still in a "pseudo-state" and the next thing to do is initialising the machine. Double-click INITIALISATION({}).

If you want to change the preference settings after having loaded a machine, you must load the machine again and restart your animation for the new settings to take effect. There is a shortcut command File -> Reopen to do this without having to go through a file selection dialogue again.

ProB is not very nice about syntax error message, but it does point out where it detected the error. Look for pos in the error message. It is followed by a line and column number.

Animating a machine

The machine is now initialised and in a proper state and you can start animating it.

snapshot5.png

Note that the stack variable is empty. The invariant is satisfied, as shown by the keyword invariant_ok and the green rectangle above the "State properties" pane. ProB does not require that the machine is proved consistent, so if the invariant is ever found to be false, the little rectangle will turn red to alert you to this condition. After trying out the Stack machine, you can modify it by removing the size(stack) < maxsize part of the precondition for push and try again, pushing more than maxsize items onto the stack to see what happens.

The "Enabled operations" pane shows that the only enabled operation is push -- the preconditions of the other operations are false -- and that it can be called with any of the three elements of the set ELEMENTS. If there are many possible arguments for an enabled operation, ProB will only show a certain number of them determined by the preference settings (initially 10). If you find that some operation instance that you need has been omitted, your choice is to reduce the number of instances, e.g. by reducing the size of sets and numbers, or increasing the number of choices ProB will show you (but this will slop down the animation).

Now double-click push(ELEMENTS2) to push ELEMENTS2 onto the stack.

snapshot6.png

Note the machine state. Sequences are represented as functions, so we see that stack is now a partial function mapping 1 to ELEMENTS2.

Now all operations are enabled. We can either push a new element on the stack, pop the top element off the stack or get the top element off the stack. Note that for operations returning results (e.g. get) the result is already computed. Unless such an operation changes the state (which get does not) you do not need to choose it.

Try pushing more things onto the stack. When there are 4 elements on the stack, the push operation becomes disabled.

Play around with the machine, pushing and popping things. The "History" pane shows what operations you have used. By using the left arrow above the "Enabled operations" pane you can undo successive operations, returning the machine to a previous state. If you wish to start over with you animation, you can choose Animate -> Reset. A fun thing to try is Animate -> Random animation which performes a number of operations chosen randomly. The "History" pane will show you what was done.

Some more examples

Now you can try som more complex examples. You can for instance try the Hotel machine of page 115 in the textbook or the Registrar machine with submachines Marriage and Life from pages 168-171 of the textbook. In these cases you will most likely want to increase some preference settings. Try setting the size of deferred sets in the preference settings to 5 to make the examples a bit more interesting. In the case of the Hotel machine, you will notice that in many cases choices are missing from the enabled operations. A little box with the text "Max" will appear over the "Enabled operations" pane when this happens. This is not a major problem -- as you start checking in rooms, some choices will be disabled so other previously hidden choices will appear. You can increase the preference settings for number of computed initialisations and number of enabled operation instances too see more of them.

Regarding the Hotel machine, there are a two things you should note:

  • Atelier B (and thus ProB) does not allow the use of parameters in the PROPERTIES clause, so the machine does not work straight from the book. Strictly speaking sze is unnecessary as it is completely determined by ROOM. You can safely remove all references to sze. (I've done that in the file you can download above.)
  • The initialisation will set numbers to ROOM * {0}, a function which maps all arguments to zero. To save space, ProB will not compute this set product immediately, but instead display it as an expression. When you make the first check-in, the expression will be computed. If you want it to be computed at once, you can change the preference setting "Lazy expansion of type expressions" to false.

Restrictions in ProB

There are some restrictions to the B language that ProB accepts. The ones that you are likely to encounter are:

  • Tuples without parentheses are not supported; write (a,b,c) instead of a,b,c
  • Trees are not yet supported.
  • The VALUES clause is not yet supported (only relevant if you try to analyse an implementation using ProB).
  • Definitions (macros) have to type check and be either an expression, predicate or substitution.

Updated  2010-02-12 23:37:33 by Lars-Henrik Eriksson.