A forum for Spin users
You are not logged in.
Pages: 1
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.
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
I've been working for a long time to make a tranlator for Brahms code into Promela. Brahms is a human-robot teamwork simulation tool btw. I've finally got to the point of translating some decent sized Brahms code and verifying it but I'm running out of memory before I can verify anything. I'd understand if they were complex models but under simulation the same thing happens everytime because essentially the scenario is deterministic. I think the problem is I've got a lot of dead variables i.e. variables I've declared but either never use or never change. Is there anyway I can request spin to ignore these dead variables or to simply state in the promela code that these variables are constants which will never change?
Pages: 1