Spinroot

RSStocker

Member

Registered: 2012-03-06

Posts: 3

Problems verifying large but almost deterministic code

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?

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: Problems verifying large but almost deterministic code

Spin should recognize those dead variables already, and eliminate them. You can check by finding where they end up in pan.h -- it should be outside the state vector.
But, you can also force this by declaring them 'hidden'
Also, use atomics and d_steps to reduce the state space -- and try bit state storage...