const N 3

scalar PID[N]

proctype :system: {
   bytes flag[PID];
   PID turn[byte];
}

proctype user[PID] {
   PID i;
   PID j;
}