Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » accessing embedded c code variables from the promela code » 2011-03-30 06:38:00

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

#2 Re: General » accessing embedded c code variables from the promela code » 2011-03-15 10:28:07

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

#3 General » accessing embedded c code variables from the promela code » 2011-03-13 10:07:37

madhukar
Replies: 7

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

Board footer

Powered by FluxBB