Tutorial Understanding ProB's Constraint Solver: 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, and have understood why animation is difficult as outlined in Tutorial Understanding the Complexity of B Animation.

First, it is important to understand that as of version 1.3, ProB uses two representations for sets and relations:

• a classical list representation
• a representation using AVL-trees.

The second representation allows ProB to deal with larger sets and relations (starting at around 100,000 elements performance will start to slow down). However, this representation can only be used if the constraint solver knows exactly all elements of a set or relation. The list representation will be used if only part of the set or relation is known.

To give an idea about the performance related to the new AVL-based representation, take the substitution

numbers := numbers - ran(%n.(n:cur..limit/cur|cur*n))

• For limit=10,000 this takes 0.2 seconds (on a 2008 laptop); with the list representation this operation ran out of memory after 2 minutes in ProB 1.2.x.
• For limit=100,000 this takes 2.1 seconds. (An encoding of this problem in Kodkod took 363 seconds on the same hardware.)
• For limit=1,000,000 this takes about 21.9 seconds.

For example, if the PROPERTIES contains the following predicates

• x = {1,2}
• y = {1|-2, 3|->4, 4|->5}
• a = 1 & b=2 & d = {a|-b}

then all values will be fully known and the new AVL-based representation will be used. However, for example for

• card(x) = 2 & dom(x) = {1,2}

we would only have partial information about x (which the constraint solver will encode using the list [1|->_, 2|->_] where the underscore marks as of yet unknown bits.

Basically, the ProB constraint solver works as follows:

• while interpreting the predicates, it will first try to "execute" predicates (or sub-predicates) which result in information which can be stored in AVL-form
• after having interpreted the whole predicate, it will then perform deterministic propagation
• only after all deterministic propagation has been performed, will the constraint solver start enumerating possibilities. For this it maintains a priority queue of enumerations and choice points.

The priority is a rough estimate of the number of possible solutions; predicates with the lowest estimate will be "executed" first.

The following picture provides a very rough picture of this process:

A simple example

Let us use the following B machine as starting point:

MACHINE Propagation
CONSTANTS low,up,f,fi,invert
PROPERTIES
 f:low..up --> 0..1 &
 invert: 0..1 --> 0..1 &
 fi = (f ; invert) &
 invert = {0|->1,1|->0} &
 low = 0 & up = 3 &
 f = {0 |-> 1, 1|->1, 2|->0, 3|->1}
VARIABLES xx
INVARIANT
 xx:low..up
INITIALISATION xx:=low
OPERATIONS
  val <-- Sense = BEGIN val := f(xx) END;
  Inc = IF xx<up THEN xx := xx+1 ELSE xx := low END
END

After loading the file, we get offered one possible way to setup the constants:

In this case, ProB performed no enumeration at all. It could immediately determine the values of all constants. We can inspect the behaviour of the constraint solver by choosing "Advanced Preferences..." in the Preferences menu and the turning the "Provide various tracing information on the terminal/console" on. If we now reopen the machine, the following information will be printed (amongst others) on the console:

...
% checking_properties

 ====> low = 0
-->> low
     val/1: int(0)

 ====> up = 3
-->> up
     val/1: int(3)

 ====> invert = {0 |-> 1,1 |-> 0}
-->> invert
     val/1: AVL.size=2

 ====> f = {0 |-> 1,1 |-> 1,2 |-> 0,3 |-> 1}
-->> f
     val/1: AVL.size=4

 ====> f : low .. up --> 0 .. 1

 ====> invert : 0 .. 1 --> 0 .. 1

 ====> fi = f ; invert
-->> fi
     val/1: AVL.size=4

-->> SUCCESS; all constants valued

% start_enumerating_constants
% grounding_wait_flags_for_constants(wfx(_57893,_66619,_56937))
% found_enumeration_of_constants(10)
...

The arrow -->> shows us when an AVL-representation was found for a constant. The ====> tells us when a predicate is interpreted. You can also see that all constants have been valued before enumeration was started. You can also see that ProB does not treat the predicates in the same order as you have typed them in the PROPERTIES clause: indeed, ProB sorts the properties (e.g., moving equalities earlier) before starting the interpretation.

After selecting SETUP_CONSTANTS and INITIALISATION, we obtain the following state, and we can ensure ourselves that the values found for f and fi are correct (by looking at the "State Properties" pane):