prom.txt

channel in1 = [4] of { int };
channel in2 = [4] of { int };
channel out = [8] of { int };
int turn;
int t1, t2;

proctype read() {
  do
  ::
    if 
    :: turn == 1 -> 
      if
      :: !empty(in1) ->
        atomic {
          in1?t1
          out!!t1
        }
      fi
      turn = 2

    :: else ->
      if
      :: !empty(in2) ->
        atomic {
          in1?t2
          out!!t1
        }
      fi
      turn = 1
    fi

  od;
}

init {
  atomic {
    turn = 1;
    in1!!1;
    in1!!2;
    in1!!3;
    in1!!4;
    
    in2!!5;
    in2!!6;
    in2!!7;
    in2!!8;

    run read();
  }
}