A forum for Spin users

You are not logged in.

#1 2011-02-01 11:44:48

Registered: 2011-01-31
Posts: 4

Question about embedded c code in Spin6

I have one more question.
I tried to use 'embedded c code' in SPIN version 6.

active proctype ex1()
{    int x;

    :: c_expr { Pex1->x < 10 } ->
        c_code { Pex1->x++; }
    :: x < 10 -> x++
    :: else -> break
% spin -a -v ccode.pml 
% gcc -o pan pan.c
In file included from pan.c:5259:
pan.m: In function ‘do_transit’:
pan.m:22: error: ‘P0’ has no member named ‘x’
pan.m:31: error: ‘P0’ has no member named ‘x’

In pan.h file, variable x is prefixed by '_1_'.

typedef struct P0 { /* ex1 */
    unsigned _pid : 8;  /* 0..255 */
    unsigned _t   : 2; /* proctype */
    unsigned _p   : 5; /* state    */
    int _1_x;
} P0;

That is effected by the new scoping rule, I'm just guessing.
When SPIN runs with the option -O, it compiles successfully.

Is such a reference 'Pex1->x' in c_code unavailable in SPIN6's new scoping rule?


#2 2011-02-02 07:51:34

Registered: 2010-11-18
Posts: 691

Re: Question about embedded c code in Spin6

yes -- good observation
you can either use the name of x as it is disambiguated in the pan.h file,
or, perhaps better in this case, revert to the original scope rules, using
spin -O -a model.pml
(where the O is a capital O, not a zero)


Board footer

Powered by FluxBB