Spinroot

A forum for Spin users

You are not logged in.

#1 2011-08-03 19:52:44

Vincent
Member
Registered: 2011-08-03
Posts: 2

Patterned verifier generation?

Hi All,

I wanted to use SPIN to create a template model where the behavior of the system are almost the same (e.g., updating a few variables with a series of numbers, x=2, x=4, x=3, etc. in a specific way). After that, I would check simple properties on these variables, like <>(x==y). However I want to repeat this quite a number of times, on different sets of numbers. For example, in one run, x=2,4,3,....; in another, x=4,2,6,...., etc. I wonder if there are efficient ways for me to do so.

I now have a Promela model for one run which works well. I am storing the numbers in an array and using them in Promela. To check the properties, I generate c code and compile it and run with pan. But to do this for a large number of times, I must prepare the same number of input files, compile, run with pan, and get the result. It seems like a waste of resource since the only difference I have among each model is just the numbers.

Are there ways to to walk around this?

Thank you very much in advance!

Offline

#2 2011-08-04 04:58:59

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

Re: Patterned verifier generation?

That's a good question. Other than suggesting that you could wrap all this in a shell-script, so that you can automate the whole process, I don't think I've any good ideas.
There's no builtin support in Spin for these types of things alas.

Offline

#3 2011-08-08 06:46:59

Vincent
Member
Registered: 2011-08-03
Posts: 2

Re: Patterned verifier generation?

Thank you! I was also thinking to do it in this way. Just to make sure I didn't neglect any smarter ways if any.

Offline

Board footer

Powered by FluxBB