Spinroot

A forum for Spin users

You are not logged in.

#1 2011-03-13 10:07:37

madhukar
Member
Registered: 2011-03-13
Posts: 3

accessing embedded c code variables from the promela code

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

Offline

#2 2011-03-14 05:35:23

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

Re: accessing embedded c code variables from the promela code

you forgot a c_track statement, to track the value of "x" which holds state information.
add this at the top:

c_track "&x" "sizeof(int)"

then, also add a semicolon after the } following the call to increment(); to avoid a syntax error there.

next, add the following ltl formula:

ltl { !<> badstate }

and you'll get the counter-example as expected:

$ spin -a example.pml
ltl ltl_0: ! (<> (badstate))

$ cc -o pan pan.c
$ ./pan
warning: never claim + accept labels requires -a flag to fully verify
hint: this search is more efficient if pan.c is compiled -DSAFETY
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
pan:1: end state in claim reached (at depth 43)
pan: wrote foobar.pml.trail

(Spin Version 6.1.0 -- 3 March 2011)
Warning: Search not completed
        + Partial Order Reduction

Full statespace search for:
        never claim             + (ltl_0)
        assertion violations    + (if within scope of claim)
        acceptance   cycles     - (not selected)
        invalid end states      - (disabled by never claim)

State-vector 24 byte, depth reached 43, errors: 1
       22 states, stored
        0 states, matched
       22 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001       equivalent memory usage for states (stored*(State-vector + overhead))
    0.291       actual memory usage for states (unsuccessful compression: 34665.00%)
                state-vector as stored = 13850 byte + 16 byte overhead
    2.000       memory used for hash table (-w19)
    0.343       memory used for DFS stack (-m10000)
    2.539       total actual memory usage


pan: elapsed time 0.034 seconds
pan: rate 647.05882 states/second

Offline

#3 2011-03-15 10:28:07

madhukar
Member
Registered: 2011-03-13
Posts: 3

Re: accessing embedded c code variables from the promela code

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

Offline

#4 2011-03-15 16:15:21

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

Re: accessing embedded c code variables from the promela code

yes this is the main issue when you verify models with embedded code, and especially if there are data objects in the C code that hold state information.
there's no easy way out: you have to determine where the relevant state information is hiding and setup tracking statements for all of them.
this should cover all data objects that can influence how the code will execute.
see also this description:

[url]http://spinroot.com/spin/Doc/spin4_ch17.pdf[/url]

Offline

#5 2011-03-30 06:38:00

madhukar
Member
Registered: 2011-03-13
Posts: 3

Re: accessing embedded c code variables from the promela code

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

Offline

#6 2011-04-01 18:27:13

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

Re: accessing embedded c code variables from the promela code

c_track statements are used simply to point the model checker at the data object that must be tracked (by giving its address) and giving it the size of the object. Typically the latter is done with a "sizeof" statement, so that is also quite simple.
Internally, the data is copied into the statevector on forward moves and copied back to the object on reverse moves in the depth-first search.
I hope that helps?

Offline

#7 2011-05-25 13:36:45

sunxi
Member
Registered: 2011-05-22
Posts: 1

Re: accessing embedded c code variables from the promela code

hi!
   I have some doubts about the c_code. I have a piece of promela code with C code embedded in, but it didn't work without the -a option:
int i, j;

proctype test(int a) {
    int ilocal;
progress:
    i = 0;
    do
    :: i < a ->
        i++;
        printf("i = %d\n", i);
        c_code {
            now.i++;
            Ptest->ilocal = 1478;
            now.j = 8741;
        };
        assert(ilocal == 1478 && j == 8741);
        printf("after c_code i = %d\n", i);
    :: else -> break;
    od
}

init {
    run test(15);
}
When i simulate the code by iSpin, it reports an access violation as bellow:
7:    proc  1 (test) a.pml:15 (state 5)    [{c_code1}]
spin: a.pml:16, Error: assertion violated
spin: text of failed assertion: assert(((ilocal==1478)&&(j==8741)))
It seems that the embedded C code not run at all, please help me.
Thanks.

Offline

#8 2011-05-25 15:49:09

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

Re: accessing embedded c code variables from the promela code

embedded C code is not executed in simulations (to do so would require building in a complete C interpreter into Spin, which is a little more that we're bargaining for).
the embedded C is is executed in all verification runs though -- when you generate pan.c it is included as part of the model -- you compile it with the C compiler as before, and now it will work!

Offline

Board footer

Powered by FluxBB