Spinroot

A forum for Spin users

You are not logged in.

#1 2017-10-08 19:41:47

bebyond
Member
Registered: 2017-09-28
Posts: 2

How to enumerate all inputs while variables r not inside state vector

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

#2 2017-10-09 17:23:01

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

Re: How to enumerate all inputs while variables r not inside state vector

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

#3 2017-10-09 19:53:12

bebyond
Member
Registered: 2017-09-28
Posts: 2

Re: How to enumerate all inputs while variables r not inside state vector

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

#4 2017-10-10 20:52:13

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

Re: How to enumerate all inputs while variables r not inside state vector

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

Board footer

Powered by FluxBB