Spinroot

A forum for Spin users

You are not logged in.

#1 2012-03-06 23:40:57

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?

Offline

#2 2012-03-07 08:56:59

spinroot
forum
Registered: 2010-11-18
Posts: 691
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...

Offline

Board footer

Powered by FluxBB