Epispin does not correctly detect xr/xs channels that are not used exclusively by the processes.

…

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

chan s11 = [1] of {mtype}; // sending and receiving to/from yourself

chan s12 = [1] of {mtype}; // sending s1 to/from s2

//
active proctype f1() {
byte ff1 = aap;
xr s11;
xr s12;
}

active proctype f2() {
byte ff2 = noot;
xr s12;
}

init{
skip; ;
}
…

Submitted by Kees Pronk on 28 August 2011 at 14:14

Fixed, although I made it somewhat stricter than the SPIN syntax checker. With SPIN, the following is allowed:

 active proctype f1(){
   xr s11;
   xr s11;
 }

whereas this double exclusive statement will not be allowed in EpiSpin.