Epispin does(!) accept the following illegal program.

The error made by the programmer is that the lower case a in the never claim should be an upper case A.

Spin detects the error.

book page 377

…

active [3] proctype A() {
printf(“this is process: %d\n”, _pid);
L: printf(“it terminates after two steps\n”);

}

never {
do
:: a[0] @L -> break
od;

}

…

Submitted by Kees Pronk on 29 August 2011 at 12:02

Fixed.