Spinroot

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......