Epispin accepts the following program:

init{

int i;

}

never{

int k;

}

Whereas spin will reject it with the message: error: never_0 defines local k
Note that the grammar definition is silent here.
In the manual page of the never claim it is stated that
may use almost any Spin construct except those involving a side effect such as assignment.
Well, a declaration also is a side effect so it is not unreasonable to reject this program.

Also, read the description of trace/notrace which is more explicit about what is allowed and what not.

Submitted by Kees Pronk on 24 September 2011 at 13:55

When ‘never’ is replaced by ‘trace’ or ‘notrace’, Spin thinks the program is OK ?????