Spinroot

A forum for Spin users

You are not logged in.

#1 2018-11-22 12:17:49

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Minimized Automaton optimization drops after small change in model

Hello,

I have a simple_model that required about 3e+08 states and 7GB memory using collapse compression and minimized automaton (MA) with about 1e+06 nodes.

complex_model makes simple_model a bit more complex: I expected the number of states and memory requirements to increase by a factor of 2 to 3, which would not cause an out-of-memory on my machine.

But instead, I do get out-of-memory (>30GB) after traversing about 6e+08 states. I guess the much higher memory requirements come from now having  11e+06 MA nodes when out-of-memorying (instead of the expected 2e+06 MA nodes).

Are there specific reasons for suddenly getting a 5 times higher number of MA nodes in relation to the number of states? If not, is there a way to find the cause? How can I avoid the cause?


Thanks
David

Last edited by DavidFarago (2018-11-22 12:19:54)

Offline

#2 2018-11-22 18:40:10

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Minimized Automaton optimization drops after small change in model

It is very hard to predict complexity. The number of nodes in the MA depends on variable ordering,
just like it does with BDDs -- so the change you made could have had both a positive and a negative
impact. Not easy to predict in this case.  You could try rearranging things (order of proctypes,
order of variables, channels, etc.) But this then devolves into random guessing pretty much -- not
the space you'd want to be in.  Try bitstate?

Offline

#3 2018-11-25 21:05:54

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Minimized Automaton optimization drops after small change in model

Thanks for the explanation.

I did come from bitstate, where no error was found and the verification had 3e+08 states stored (5e+08 states matched). For MA, the verification did not find any error either, but caused an out-of-memory after 6e+08 states stored (only 5e+07 states matched).

Do you have any experience/statistics how good bitstate really is? I wonder if I only need to reach another 1.5e+08 states in MA (to reach all states matched in bitstate), or if there are likely completely new subgraphs not reached via bitstate.


Best
David

Offline

#4 2018-11-25 21:12:40

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Minimized Automaton optimization drops after small change in model

Oh, one more thing: complex_model makes simple_model only more complex by initializing certain variables differently. Those variables, however, influence the control flow. Can that already cause variables being reordered?

Thanks a lot for your help!
David

Offline

#5 2018-11-25 22:23:19

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Minimized Automaton optimization drops after small change in model

Take a look at: http://spinroot.com/gerard/pdf/vmcai2016.pdf for how you can reach 100% coverage by using repeated bitstate runs...

Offline

Board footer

Powered by FluxBB