A forum for Spin users
You are not logged in.
Pages: 1
I have read the chapter that you suggested me to read. However, I am still unclear on "c_track". If you could tell me exactly how these "track" statements work internally, it would be of immense help.
I know it is only with experience that I'll be able to gain further intuition on this. But I feel I lack the knowledge itself. Please help.
Regards,
Madhukar
Thanks a lot. That was really helpful.
However, I have some doubts about the variables that I need to "track".
In the sample code that I had put above, I had just tried to replicate the behavior of my code. The actual code is a bit more involved and the value of x in modified depending on a lot of other factors (an integer array, amongst other things). When I "track" x alone, the verification does not work fine. Although when I "track" the array as well, I do get the counterexample as expected.
How would I figure out, in general, the set of variables that I need to "track"?
Regards,
Madhukar
Hi,
I have a very simple piece of c code which looks like this :
int x = 0;
void increment()
{
x++;
return;
}
I have embedded this in a promela code. Essentially, I call this 'increment' function from my promela code. And at the same time, I want an assertion violation (or a never claim violation) when x reached a particular value, 5 let's say. The promela code I have written looks something like this :
c_code{
#include "ccode.c" /* the c code written above */
}
bool badstate = false;
active proctype driver()
{
do
:: (1) ->
c_code{
increment();
}
if
:: c_expr{ x == 5 } ->
badstate = true;
:: else ->
skip;
fi;
od;
}
I have added the never claim for the LTL formula "<>badstate", but it does not seem to work.
I think my code has a problem in accessing the variables defined in the code from my promela code. I can't seem to find a way to figure this out. Please help.
Thanks and Regards.
Madhukar
Pages: 1