It seems Epispin is more strict(!) that spin on the following program.

Shall I send the problem to Gerard Holzmann?

…

active proctype A(){
printf(“this is process: %d\n”, _pid);
_pid = _pid + 1;
printf(“this is process: %d\n”, _pid);
_pid++;
printf(“this is process: %d\n”, _pid);
}

. ..

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

In the book it is literally stated that _pid is read only, so that’s why this gives an error on EpiSpin. But may be you can post a message on the Spin forum to see if it is really a bug in Spin.

http://spinroot.com/fluxbb/viewtopic.php?id=422 discusses this issue on the Spin forum. Awaiting the actions of the Spin developers, no changes are made in EpiSpin.