Hi,
maybe you can send us the model, so that we can help you better.
There are several options:
1) try and reduce the amount of memory ProB uses per state:
For probcli you can set the COMPRESSION preference to true, e.g., in the following way:
probcli MyMachine.mch --model-check -p COMPRESSION TRUE
See
for probcli switches.
You could also add a DEFINITION
SET_PREF_COMPRESSION == TRUE
to your B machine to set the preference.
There is also the possibility to forget the state space of already visited states by setting the preferences FORGET_STATE_SPACE and IGNORE_HASH_COLLISIONS to TRUE.
2) you can try reduce the state space, e.g., via symmetry:
Hash symmetry typically works best.
Another possibility is partial order reduction:
3) sometimes bounded model checking works much better than explicit state model checking, especially when the branching factor is very high.
4) You could try and use our TLC backend
It will not work for refinements and only has limited support for machine inclusion,… but it can be very fast and the state space is kept on disk.
Greetings,
Michael