/* Description: ------------ this program is composed of two functions executed by two different threads, one called putter, and the other getter. The putter sends a list, one cell at a time, to the getter, and eventually sends its endpoint for closing. The getter receives either a cell and delete it, or an endpoint, in which case it closes the channel. Communications are weakly synchronized by an additional acknowledgment message between any cell messages. Both threads are launched by the main send\_list function, which also allocates the two endpoints. */ message ack [emp] message cell [val|->] message close_me [val|->C{end} * val==src] contract C { initial state transfer { !cell -> wait; !close_me -> end; } state wait { ?ack -> transfer; } final state end {} } /* We assume a linked list starting at x */ putter(e,x) [e|->C{transfer} * list(x)] { local t; while(x != NULL) [e|->C{transfer} * list(x)] { /* Swapping the two lines below causes an error */ send(cell,e,x); t = x->tl; x = t; receive(ack,e); } send(close_me,e,e); } [emp] getter(f) [f|->~C{transfer}] { local x, e; e = NULL; while(e == NULL) [if e==NULL then f|->~C{transfer} else e|->C{end} * f|->~C{end},pr:e] { switch receive { x = receive(cell,f): { dispose(x); send(ack,f); } e = receive(close_me,f): {} } } close(e,f); } [emp] send_list(x) [list(x)] { local e,f; (e,f) = open(C); putter(e,x) || getter(f); } [emp]