Tutorial Tuning Model Checking: Difference between revisions

Page is under construction

Reducing memory usage

You can try to reduce the memory consumption of ProB's model checker by setting the COMPRESSION preference to TRUE.

You can set FORGET_STATE_SPACE and IGNORE_HASH_COLLISIONS to TRUE

You can enable operation reuse. This is useful if most operations only affect a subset of the variables.

You should move unchanged variables to constants (in B and Event-B). Constants are only stored once, variables are stored for every state.

Use SAFETY_MODEL_CHECK TRUE if you do not do LTL model checking.

Use -statistics to uncover where memory is used.

Let us use this machine for illustration:

MACHINE IncrementalStatePackingTestLarge
SETS
 ID={aa,bb,cc}
VARIABLES xx,yy,zz,ii
INVARIANT
 xx:ID & yy:ID & zz <: NATURAL & ii : 1..1000
INITIALISATION xx:=aa || yy := bb || zz := (1..1000 \/ 2000..3000) \ {2001} || ii := 1
OPERATIONS
  SetX(vv) = PRE vv:ID & vv /= xx
             THEN xx:= vv END;
  SetY(vv) = PRE vv:ID & vv /= yy
             THEN yy:= vv END;
  IncrI = PRE ii<1000 THEN ii:=ii+1 END
END

Let us run probcli on this example (note: the -memory command is new and may not be available in your version of probcli):

probcli IncrementalStatePackingTestLarge.mch -model-check -memory

ALL OPERATIONS COVERED
% All open nodes visited
Model checking time: 8994 ms (10249 ms walltime)
States analysed: 9000
Transitions fired: 44992
No counter example found. ALL nodes visited.
ProB memory used:  466.939 MB ( 362.081 MB program) 

By providing the -statistics command you can get a very detailed output of the memory consumption.

probcli IncrementalStatePackingTestLarge.mch -model-check -statistics
...
packed_visited_expression(_429,_431) :  9001 facts :  176.650 MB ( 71.792 MB program)  freed:  290.304 MB
...
transition(_429,_431,_433,_435) :  44992 facts :  166.853 MB ( 61.996 MB program)  freed:  9.796 MB
...

Here you can see that most memory is used to store the states (not the transitions). Note: you should look at the freed information for each stored fact.

One way to improve memory consumption is to use the COMPRESSION preference:

probcli IncrementalStatePackingTestLarge.mch -model-check -p COMPRESSION TRUE -memory

ALL OPERATIONS COVERED
% All open nodes visited
Model checking time: 7341 ms (8387 ms walltime)
States analysed: 9000
Transitions fired: 44992
No counter example found. ALL nodes visited.
ProB memory used:  179.199 MB ( 74.342 MB program)

As you can see, we have considerably reduced the memory consumption in this case, and as a side-benefit the runtime as well (although in general, enabling compression can increase runtime).

In case transitions take up space you can also use the SAFETY_MODEL_CHECK preference in case you do not need LTL or deadlock checking. For this model this does not result in a big decrease of memory usage. Note that you should add the -nodead flag to disable deadlock checking.

probcli IncrementalStatePackingTestLarge.mch -model-check -p COMPRESSION TRUE -memory -p SAFETY_MODEL_CHECK TRUE -nodead

ALL OPERATIONS COVERED
% All open nodes visited
Model checking time: 7333 ms (8483 ms walltime)
States analysed: 9000
Transitions fired: 9000
No counter example found. ALL nodes visited.
ProB memory used:  169.784 MB ( 64.926 MB program) 

Finding reasons for large state spaces

Use min-max values.