A forum for Spin users
You are not logged in.
Pages: 1
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
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
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
Pages: 1