No edit summary |
|||

(11 intermediate revisions by 2 users not shown) | |||

Line 1: | Line 1: | ||

[[Category: | [[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 == | == Simple Inconsistency in the PROPERTIES == | ||

Line 24: | Line 26: | ||

[[file:ProB_Jukebox_DebugUnsatProp.png|center|400px]] | [[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 | 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. | ||

Line 33: | Line 35: | ||

This will result in the following | This will result in the following visualization: | ||

[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png|center]] | [[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp.png|center]] | ||

Line 63: | Line 65: | ||

We can see that ProB has found the solution <tt>limit=100</tt> for the first two properties and then got stuck. | 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 | Using the graphical viewer results the following visualization: | ||

[[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp2.png|center|600px]] | [[file:ProB_Jukebox_AnalyseGraphicallyUnsatProp2.png|center|600px]] | ||

Line 80: | Line 82: | ||

[[file:ProB_JukeboxAfterInit3.png|center||600px]] | [[file:ProB_JukeboxAfterInit3.png|center||600px]] | ||

We can now | We can now analyze the ASSERTIONS. | ||

For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu: | For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu: | ||

[[file:ProB_Jukebox_AnalyseGraphicallyUnsatAssertion3.png|center]] | [[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. | |||

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>. | |||

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. |

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.

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

This will result in the following visualization:

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:

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

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 analyze the ASSERTIONS. For this, choose the "Analyse Graphically/Assertions" in the "Analyse" menu:

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)`:

After hitting OK we obtain:

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:

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

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.