Spinroot

A forum for Spin users

You are not logged in.

#1 2011-02-21 01:59:35

Jenny
Member
Registered: 2011-02-21
Posts: 1

Local variable scoping

I have the following code:

byte pid1, pid2;

proctype p1()
{
    byte x;
    do
        :: atomic { x++ ; x++ }
    od
}

proctype p2()
{
    byte y;
    do
        :: atomic { y++ ; y++ }
    od
}

init {
    atomic {
        pid1 = run p1();
        pid2 = run p2();
    }
}

never {
    do
    :: skip
    :: (p1:x==2)&&(p2:y == 232) -> break
    od
}


But it will always emit error after compiling:
spin -O3 -a local_var.pml
gcc -O pan pan.c
In file included from pan.c:5353:
pan.m: In function ‘do_transit’:
pan.m:40: error: ‘P0’ has no member named ‘x’
pan.m:40: error: ‘P1’ has no member named ‘y’

I have searched the reference, but still not quite sure how to reference the local variables outside......

Offline

#2 2011-02-21 07:32:40

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

Re: Local variable scoping

That's a side-effect of the new scope rules. Note that refering to local process variables from within a global never claim is frowned upon by the gods.
You can make it work though, and side-step those same gods, by generating the pan.c code as follows (suppressing the new scope rules):
   spin -O -a local_var.pml
   gcc -O3 -o pan pan.c

I'm not sure what you meant to do with the spin flag -O3?  You may have meant -o3 (lower case oh) to disable statement merging ?

Offline

Board footer

Powered by FluxBB