/* prod i kons, dwa lacza jednokierunkowe, 01.2018
wezel 1: wysyla 7, czyta 6,
wezel 2: czyta 7, wysyla 6,
bufor ma 5 elem,
na poczatku: w.1 ma 23 elem, w.2 ma 0 elem
!!! UWAGA: w tym przykladzie wysyla sie i czyta po 1 elem !!!
spin potrafi sobie poradzic z nieskon. egz. ?!?!

zdaje sie ze zamiast buf. cykl. elem1/2 mozna uzyc kanalu ?!?!?!

*/

chan lacze1= [5] of {byte};
chan lacze2= [5] of {byte};

byte elem1[25]= {1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,0,0};
byte c1=0, p1=23, pelne1=23, wolne1=2;

byte elem2[25];
byte c2=0, p2=0, pelne2=0, wolne2=25;

active proctype P1() {
  byte e;
  do
  :: pelne1>0 -> e=elem1[c1]; c1=(c1+1)%25; pelne1--; wolne1++; lacze1!e;
     wolne1>0 -> lacze2?e; elem1[p1]=e; p1=(p1+1)%25; pelne1++; wolne1--;
     //printf("c1=%d p1=%d c2=%d p2=%d\n", c1, p1, c2, p2);
  od;
}

active proctype P2() {
  byte e;
  do
  :: wolne2>0 -> lacze1?e; elem2[p2]=e; p2=(p2+1)%25; pelne2++; wolne2--;
     pelne2>0 -> e=elem2[c2]; c2=(c2+1)%25; pelne2--; wolne2++; lacze2!e;
     //printf("c1=%d p1=%d c2=%d p2=%d\n", c1, p1, c2, p2);
  od;
}