Spinroot

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!