In the following program:

mtype = {aap, noot, mies, wim, zus};

chan s41 = [0] of {mtype};

active proctype f4() {
mtype ff1 = wim;
do
:: s41 : ff1;
od;
}

init{
skip;
}

there exist a clear error: the colon after the s41 label in the do-loop (should be an exclamation mark or a question mark).
This error is correctly pointed out by spin.
However, in Epispin, the error indicator is in the very first (blank) line.
When the blank line is deleted, the error indicator points to the mtype definition.

Submitted by Kees Pronk on 21 August 2011 at 21:54

I added the error message for labels that are used as first statements in do and if structures, which fixes the issue.