how to reduce the memory consumption of model checking ?
14 views
Skip to first unread message
r0ur...@gmail.com
May 13, 2017, 9:44:45 AM5/13/17
to ProB Users
Hi,
im trying to execute the model checking, but i end up with out of memory.
i have tried various methods such as reducing the number of elements in the
sets and limit the number of element by defining scope for each set.
However, i still face the same problem. So, below is my questions :-
1) May I know, what are other possible things that I can do in order to reduce the memory consumption ?
2) Is there any way to calculate the total memory consumption for model checking ?
Thank you.
im trying to execute the model checking, but i end up with out of memory.
i have tried various methods such as reducing the number of elements in the
sets and limit the number of element by defining scope for each set.
However, i still face the same problem. So, below is my questions :-
1) May I know, what are other possible things that I can do in order to reduce the memory consumption ?
2) Is there any way to calculate the total memory consumption for model checking ?
Thank you.
Michael Leuschel
May 18, 2017, 12:45:54 PM5/18/17
to r0ur...@gmail.com, ProB Users
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
--
You received this message because you are subscribed to the Google Groups "ProB Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
To post to this group, send email to prob-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/3e641b7c-726e-4564-8201-75c92cb94723%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
r0ur...@gmail.com
May 23, 2017, 6:36:15 AM5/23/17
to ProB Users, r0ur...@gmail.com
Hi,
Thank you for your recommendation. I have further questions.
1) why does the percentage of the checked states sometimes decreasing and remains fixed ? For example, from 15% to 10%. Is it because the number of states
keeps increasing thus, reducing the percentage ?
2) based on my understanding, the model checking will check for any possible invariant violations in all the states. but, since state explosion can occur, it will
be hard to determine if there are any error. so, if i perform ltl model checking, is it possible for me still possible for me to determine whether the specification
is correct ?
Thank you.
Thank you for your recommendation. I have further questions.
1) why does the percentage of the checked states sometimes decreasing and remains fixed ? For example, from 15% to 10%. Is it because the number of states
keeps increasing thus, reducing the percentage ?
2) based on my understanding, the model checking will check for any possible invariant violations in all the states. but, since state explosion can occur, it will
be hard to determine if there are any error. so, if i perform ltl model checking, is it possible for me still possible for me to determine whether the specification
is correct ?
Thank you.
Michael Leuschel
May 24, 2017, 7:52:06 AM5/24/17
to r0ur...@gmail.com, ProB Users
Hi,
On 23 May 2017, at 12:36, r0ur...@gmail.com wrote:Hi,
Thank you for your recommendation. I have further questions.
1) why does the percentage of the checked states sometimes decreasing and remains fixed ? For example, from 15% to 10%. Is it because the number of states
keeps increasing thus, reducing the percentage ?
Yes, indeed.
The percentage describes the fraction of the known states so far which have already been processed.
Processing amounts to checking the invariant, and computing all successor states.
Adding the successor states can result in new states being added, and hence percentage decreasing.
2) based on my understanding, the model checking will check for any possible invariant violations in all the states. but, since state explosion can occur, it will
be hard to determine if there are any error. so, if i perform ltl model checking, is it possible for me still possible for me to determine whether the specification
is correct ?
In general, the only way to determine that an infinite state system is correct, is via proof (Atelier-B, Rodin).
Some LTL formulas can be determined, without constructing the entire state space.
Ideally, you should set the LTL preference “With Safety Check” to true:
(which requires that you also choose “Download and Install LTL2BA Tool…” in the Help menu)
Greetings,
Michael
Reply all
Reply to author
Forward
0 new messages