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;
}