A forum for Spin users
You are not logged in.
Pages: 1
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
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
Pages: 1