Page is under construction
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)
Use min-max values.