13 views

Skip to first unread message

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.

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.

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.

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

Search

Clear search

Close search

Google apps

Main menu