Tutorial Troubleshooting the Setup: Difference between revisions

No edit summary
 
(16 intermediate revisions by 2 users not shown)
Line 1: Line 1:
[[Category:User Manual]]
[[Category:Tutorial]]




We assume that you grasped the way that ProB setups up the initial states of a B machine as outlined in [[Tutorial Setup Phases]].
We assume that you have 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.
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.


We will also learn to use the various predicate analysis features provided by ProB.
== 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.
First, open the machine "Jukebox.mch" which can be found in the SchneiderBook/Jukebox_Chapter13 subdirectory of the ProB Examples folder.
Line 17: Line 20:


ProB should now popup the following message:
ProB should now popup the following message:
[[file:ProB_Jukebox_UnsatProp.png|center||300px]]
[[file:ProB_Jukebox_UnsatProp.png|center]]


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


[[file:ProB_Jukebox_DebugUnsatProp.png|center||300px]]
[[file:ProB_Jukebox_DebugUnsatProp.png|center|400px]]


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.
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 the source of the trouble (or inconsistency).


An alternate means to figure out the source of the problem is ProB's graphical formula viewer.
An alternate means to figure out the source of the problem is ProB's graphical formula viewer.
For this, choose the "Analyse Graphically"...
For this, choose the "Analyse Graphically/Properties" in the "Analyse" menu:
 
 
[[file:ProB_Jukebox_AnalyseGraphicallyCommand.png|center]]
 
 
This will result in the following visualization:
 
[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png|center]]
 
This viewer uses another, more sophisticated algorithm to determine a maximal subset of the Properties which is satisfiable. In this case, it has determined <tt>limit=1</tt> to make <tt>limit:NAT1</tt> true (but which obviously does not make <tt>limit>99</tt> true.
 
In any way, the problem here is that we have set MAXINT to 3, and hence <tt>NAT1={1,2,3}</tt>.
To make our PROPERTIES satisfiable again, we could add for example
<pre>
DEFINITIONS
SET_PREF_MAXINT==255
</pre>
to the machine and re-load it. As we can see, the problem is solved and we can proceed with animation of the machine:
 
[[file:ProB_JukeboxAfterLoad2.png|center||600px]]
 
== A more involved inconsistency ==
 
Let us add
<pre>
& !x.(x<limit => x<99)
</pre>
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:
 
 
[[file:ProB_Jukebox_DebugUnsatProp2.png|center|400px]]
 
We can see that ProB has found the solution <tt>limit=100</tt> for the first two properties and then got stuck.
Using the graphical viewer results the following visualization:
 
[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp2.png|center|600px]]
 
Here we can see that ProB has used another partial solution, namely <tt>limit=1</tt>, which also satisfies two properties (and fails to satisfy <tt>limit>99</tt>).
 
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:
<pre>
PROPERTIES        limit : NAT1 & limit>99
ASSERTIONS        !x.(x<limit => x<99)
</pre>
Now save and reopen the machine. This time the properties are satisfiable. After selecting SETUP_CONSTANTS(100) and INITIALISATION({}) we obtain the following picture:
 
 
[[file:ProB_JukeboxAfterInit3.png|center||600px]]
 
We can now analyze the ASSERTIONS.
For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu:
 
[[file:ProB_Jukebox_AnalyseGraphicallyUnsatAssertion3.png|center]]
 
The graphical viewer gives us an instance where the universally quantified formula is false: <tt>x=99</tt>, which hopefully helps us in fixing the problem, e.g., writing <tt>!x.(x<limit => x<=99)</tt>.
 
Note, that ProB also allows us to inspect custom predicates using the graphical viewer (without saving and reopening a machine).
For this, choose the "Analyse Graphically/Custom Predicate..." in the "Analyse" menu and enter <tt>!x.(x<limit => x<=99)</tt>:
[[file:ProB_Jukebox_AnalyseGraphicallyCustomCommand.png|center]]
After hitting OK we obtain:
[[file:ProB_Jukebox_AnalyseGraphicallyCustom3.png|center]]
 
As we can see, this predicate is true in that particular state of the machine.
Note, there is also the option to use  "Analyse Predicate/Custom Predicate...". This will result in a simpler (non-graphical) visualization. Use this if the graphical visualization is too large or takes too much time to compute.
The custom predicate analysis commands have one disadvantage: the formula has to be typed into a single line inside the dialog box (and parse errors are not very user-friendly). The alternatives are entering the formula into the ASSERTIONS clause as above. One can also define a special GOAL predicate in the DEFINITIONS:
<pre>
DEFINITIONS      GOAL == !x.(x<limit => x<99)
</pre>
Then one can use "Analyse Predicate/GOAL" or "Analyse Graphically/GOAL". The GOAL predicate can also be used to guide the model checker.
 
Finally, the "Analyse" commands can also be applied to the precondition and guards of operations. This is useful to find out why a particular operation is (maybe) unexpectedly disabled or enabled.
For this, choose the "Analyse Graphically/Operation PRE..." in the "Analyse" menu and select the "select" operation:
[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE.png|center]]
 
After hitting "Select" or typing return we obtain, which shows us why the operation is not enabled:
[[file:ProB_Jukebox_AnalyseGraphicallyOperationPRE3.png|center]]
 
 
== Selectively Ignoring Properties/Axioms ==
 
You can use a pragma to tell ProB to ignore a certain property:


<pre>
MACHINE Log2
DEFINITIONS SET_PREF_USE_IGNORE_PRAGMAS == TRUE
ABSTRACT_CONSTANTS log2
PROPERTIES
log2 : NATURAL1 --> INTEGER &
!(x,y).(x:NATURAL1 & y:NATURAL1 => log2(x*y) = log2(x)+log2(y))
  /*@desc prob-ignore */
END
</pre>
The second property will be ignored during property setup, but will still be shown in the evaluation view for example.


[[file:ProB_Jukebox_AnalyseGraphicallyCommand.png|center||300px]]
This feature is available as of version 1.11.0 when the preference <tt>USE_IGNORE_PRAGMAS</tt> is set to TRUE (currently it is FALSE by default).
Under these circumstances a conjunct of the PROPERTIES will then be ignored:
* when it is followed by the  <tt>/*@desc prob-ignore */</tt> pragma
* when it is preceded by a label which contains prob-ignore in its name, such as <tt>/* @label="axm2-prob-ignore" */</tt>.


This will result in the following visualisation:
The latter thus also works within Rodin for Event-B contexts.


[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png|center||300px]]
An alternative can also be to move a predicate from PROPERTIES to the ASSERTIONS clause.
The latter will not be used during the constant setup.

Latest revision as of 16:09, 6 October 2021


We assume that you have 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.

We will also learn to use the various predicate analysis features provided by ProB.

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:

ProB JukeboxAfterLoad.png


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:

ProB Jukebox UnsatProp.png

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

ProB Jukebox DebugUnsatProp.png

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 the source of the trouble (or inconsistency).

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:


ProB Jukebox AnalyseGraphicallyCommand.png


This will result in the following visualization:

ProB Jukebox AnalyseGraphicallyUnsatProp.png

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:

ProB JukeboxAfterLoad2.png

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:


ProB Jukebox DebugUnsatProp2.png

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 visualization:

ProB Jukebox AnalyseGraphicallyUnsatProp2.png

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:


ProB JukeboxAfterInit3.png

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

ProB Jukebox AnalyseGraphicallyUnsatAssertion3.png

The graphical viewer gives us an instance where the universally quantified formula is false: x=99, which hopefully helps us in fixing the problem, e.g., writing !x.(x<limit => x<=99).

Note, that ProB also allows us to inspect custom predicates using the graphical viewer (without saving and reopening a machine). For this, choose the "Analyse Graphically/Custom Predicate..." in the "Analyse" menu and enter !x.(x<limit => x<=99):

ProB Jukebox AnalyseGraphicallyCustomCommand.png

After hitting OK we obtain:

ProB Jukebox AnalyseGraphicallyCustom3.png

As we can see, this predicate is true in that particular state of the machine. Note, there is also the option to use "Analyse Predicate/Custom Predicate...". This will result in a simpler (non-graphical) visualization. Use this if the graphical visualization is too large or takes too much time to compute. The custom predicate analysis commands have one disadvantage: the formula has to be typed into a single line inside the dialog box (and parse errors are not very user-friendly). The alternatives are entering the formula into the ASSERTIONS clause as above. One can also define a special GOAL predicate in the DEFINITIONS:

DEFINITIONS       GOAL == !x.(x<limit => x<99)

Then one can use "Analyse Predicate/GOAL" or "Analyse Graphically/GOAL". The GOAL predicate can also be used to guide the model checker.

Finally, the "Analyse" commands can also be applied to the precondition and guards of operations. This is useful to find out why a particular operation is (maybe) unexpectedly disabled or enabled. For this, choose the "Analyse Graphically/Operation PRE..." in the "Analyse" menu and select the "select" operation:

ProB Jukebox AnalyseGraphicallyOperationPRE.png

After hitting "Select" or typing return we obtain, which shows us why the operation is not enabled:

ProB Jukebox AnalyseGraphicallyOperationPRE3.png


Selectively Ignoring Properties/Axioms

You can use a pragma to tell ProB to ignore a certain property:

MACHINE Log2
DEFINITIONS SET_PREF_USE_IGNORE_PRAGMAS == TRUE
ABSTRACT_CONSTANTS log2
PROPERTIES
 log2 : NATURAL1 --> INTEGER &
 !(x,y).(x:NATURAL1 & y:NATURAL1 => log2(x*y) = log2(x)+log2(y))
  /*@desc prob-ignore */
END

The second property will be ignored during property setup, but will still be shown in the evaluation view for example.

This feature is available as of version 1.11.0 when the preference USE_IGNORE_PRAGMAS is set to TRUE (currently it is FALSE by default). Under these circumstances a conjunct of the PROPERTIES will then be ignored:

  • when it is followed by the /*@desc prob-ignore */ pragma
  • when it is preceded by a label which contains prob-ignore in its name, such as /* @label="axm2-prob-ignore" */.

The latter thus also works within Rodin for Event-B contexts.

An alternative can also be to move a predicate from PROPERTIES to the ASSERTIONS clause. The latter will not be used during the constant setup.