A forum for Spin users
You are not logged in.
Hi, I'm using embed c with Promela in my project, but I have a problem to combine
In my program, I use a sequence of if statements block to exhaustively generate different combinations of inputs and then call functions in embed c codes. Since those input variables are also included in embed c codes, I use c_track syntax and it works well. But those input variables are not related to the properties that I want to verify, therefore I want to use them outside state vector to reduce the search tree. The problem is, if I don't declare those variables for verifiers and just define them at the embed c codes, SPIN would consider those combinations as redundant cases and trim them immediately before calling the functions in c. Could anyone let me know how it can be solved?
Right now I have tried c_state with hidden to declare those input variables, but the results are same to defining those variables at c codes only. I also have tried c_state with global property. It works well but it doesn't save time, since those variables will still be inside state vectors. Right now I have a simplest method, which uses just one if statement block and explicitly write down each combination of those input variables values. In each combination, we call the functions in embed c program in the same c_code statement so SPIN is not able to trim the redundant states. But since there are hundreds of such combinations, I hope there would be some other ways.
Thanks in advance.
Offline
not sure i fully understand the specifics, but in this paper
http://spinroot.com/gerard/pdf/spin04.pdf
it is described how you can trim the state space with an abstraction function,
which in effect means that you can store and track different things than what appears
on the search stack: the search stack stores concrete values, and the state space abstracted values.
maybe this can be used here?
Offline
Thanks for your response. I have read your referred link, which is very interesting.
Unfortunately I haven't described my problem clearly. Take one example at section 2.2 in your referred link.
If we use "if statement block" as follows, both even and odd cases would be generated.
if
:: c_code { x=0; y=0; abstraction(); }
:: c_code { x=1; y=0; abstraction(); }
fi
But if we use "if statement block" in a different way, SPIN would consider the other cases redundant immediately after if statement.
if
:: c_code {x=0; y=0; }
:: c_code {x=1; y=0; }
fi
c_code {abstraction();}
The reason I want to use the second way is that I have much more variables instead of just two. Therefore, I don't want to explicitly write down all possible combinations in one "if statement block". Do you know if there's any way to solve this issue or any suggestions? Thanks a lot!
Offline
yes, that makes it difficult because now you have an intermediate state right after those variables are set.
i'm afraid that there's no way around computing the abstraction at the end of each of those c_code blocks -- inside the c_code block
Offline