Tutorial Tuning Model Checking

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.

Finding reasons for large state spaces

Use min-max values.