Tutorial Troubleshooting the Setup: Difference between revisions

We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in Tutorial Setup Phases.

In this lesson, we examine what can go wrong in these phases and how one can find a solution. Indeed, setting up the constants and initial values of a machine is often the most difficult step for an animator. Unfortunately, it is also the very first step an animator has to perform.

Simple Inconsistency in the PROPERTIES

First, open the machine "Jukebox.mch" which can be found in the SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples folder. The main ProB window should look more or less as follows:

Now edit the file, and type & limit>99 after PROPERTIES limit:NAT1. Save the machine and reload it. Hint: there is a "Save and reopen" command in the "File" menu for this action.

ProB should now popup the following message:

If you click "Yes" (or Ja), you will get the following window:

What ProB does is add conjuncts from the PROPERTIES (and CONSTRAINTS clause) one-by-one, until it can no longer find a solution. This can often give you an indication of what is wrong, and where the trouble (or inconsistency) stems from.

An alternate means to figure out the source of the problem is ProB's graphical formula viewer. For this, choose the "Analyse Graphically/Properties" in the "Analyse" menu:

This will result in the following visualisation:

This viewer uses another, more sophisticated algorithm to determine a maximal subset of the Properties which is satisfiable. In this case, it has determined limit=1 to make limit:NAT1 true (but which obviously does not make limit>99 true.

In any way, the problem here is that we have set MAXINT to 3, and hence NAT1={1,2,3}. To make our PROPERTIES satisfiable again, we could add for example

DEFINITIONS
 SET_PREF_MAXINT==255

to the machine and re-load it. As we can see, the problem is solved and we can proceed with animation of the machine:

A more involved inconsistency

Let us add

& !x.(x<limit => x<99)

to the PROPERTIES of the machine and then save and reopen it. We again get the error message that ProB cannot find CONSTANTS which satisfy the PROPERTIES. If click on the "Yes" button to debug the PROPERTIES we get the following picture:

We can see that ProB has found the solution limit=100 for the first two properties and then got stuck. Using the graphical viewer results the following visualisation:

Here we can see that ProB has used another partial solution, namely limit=1, which also satisfies two properties (and fails to satisfy limit>99).

If the feedback provided by ProB is not sufficient to locate the problem, one can try to comment out parts of the PROPERTIES by hand until they become satisfiable. One can also move them to the ASSERTIONS clause, which has the advantage that we can check them later. Let us move the last property into an assertion:

PROPERTIES        limit : NAT1 & limit>99
ASSERTIONS        !x.(x<limit => x<99)

Now save and reopen the machine. This time the properties are satisfiable. After selecting SETUP_CONSTANTS(100) and INITIALISATION({}) we obtain the following picture:

We can now analyse the ASSERTIONS. For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu: