// Multiple Process to run alternately

mtype = { F, S};
mtype turn = F;

active [2] proctype Producer()
{
  do
    :: (turn == F) -> printf("Producer-%d\n",_pid); turn = S;
  od
}

active [2] proctype Consumer()
{
  do
    :: (turn == S) -> printf("Consumer-%d\n",_pid); turn = F;
  od
}