Epispin will accept the following program:

active proctype p1() {

goto L1;

{
	int k = 1; 

	skip;
}

L1 : skip;

}

Whereas spins complains:

spin: block1.pml:7, Error: place initialized var decl of ‘k’ at start of proctype saw ‘;’ near ‘skip’

Note that the goto and labels AND the initialization of k are essential here.

I wonder whether the problem is in Spin or in EpiSpin.

Submitted by Kees Pronk on 8 September 2011 at 23:12