Tutorial Tuning Model Checking: Difference between revisions

(Created page with "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. Y...")
 
Line 13: Line 13:
Constants are only stored once, variables are stored for every state.
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 ==
== Finding reasons for large state spaces ==


Use min-max values.
Use min-max values.

Revision as of 13:46, 28 May 2021

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.