Epispin accepts the following program.

active proctype p2(){

{
int k;
// skip;
L3: skip;

goto L3;

}

}

Spin however states:

error: (goto1a.pml:6) label L3 placed incorrectly

=====> instead of “{ Label: statement … }”

=====> always use “Label: { statement … }”

The reason being of course that the state at L3 is precisely the state at the beginning of the block.
Note that inserting the skip, now commented out, makes this a correct program.

Submitted by Kees Pronk on 9 September 2011 at 17:21