Spinroot

RSStocker

Member

Registered: 2012-03-06

Posts: 3

Reducing model depth

I've been translating an agent simulation language into Promela for Spin verification.  I've got the problem that when I perform Spin verification, it doesn't just verify my agent simulation but also the translation of the semantics.  The simulations I program are very simple but the translation is complex but deterministic.  So when I try to create a model with say 10 choice points, Spin creates this model with the 10 choice points but also several thousand deterministic choice points inbetween.  I was wondering if there was a way to declare certain If-statements and do-loops so that Spin won't create states when they appear?  An example of how they are deterministic are:

if
::(X==1)->
    /*Do something*/
::(X==2)->
    /*Do something*/
::(X==3)->
    /*Do something*/
fi /*Where x is a value predetermined by an actual choice point*/

I've looked into the use of "hidden" variables but these are write-only scratch which is of no use.  I've ran out of ideas other than performing breadth first search or compiling -DSC to stop the problem of running out of memory.  I've tried performing simulation runs with -i, the simulations takes a few minutes to run and will only prompt me at the correct choice points; which many only be a dozen times.

Many Thanks,
Richard

spinroot

forum

Registered: 2010-11-18

Posts: 694

Website

Re: Reducing model depth

Did you try wrapping those deterministic if stmnts in d_step sequences?

RSStocker

Member

Registered: 2012-03-06

Posts: 3

Re: Reducing model depth

No I've not.  I saw references to d_steps while examining possibilities such as declaring variables hidden but didn't understand what they were, should have googled them I suppose.  Thank you for the help, fingers crossed they work.