/*
 * producer / consummer 
 *
 */

system pc;

const P = 2; /* number of producers (1 or greater) */
const C = 3; /* number of consummers (1 or greater) */
const L = 3; /* size of the buffer (1 or greater) */

signal putInvoke(pid);
signal putAnswer();
signal getInvoke(pid);
signal getAnswer();

/*
 * producer
 *
 */

process producer(P);
state idle #start ;
    output putInvoke(self) to {buffer}0;
      nextstate onPut;
endstate;
state onPut;
  input putAnswer();
    nextstate idle;
endstate;
endprocess;

/*
 * consummer
 *
 */

process consummer(C);
state idle #start ;
    output getInvoke(self) to {buffer}0;
      nextstate onGet;
endstate;
state onGet;
  input getAnswer();
    nextstate idle;
endstate;
endprocess;

/*
 * buffer
 *
 */

process buffer(1);

var c integer;
var x pid;

state empty #start ;
  save getInvoke;
  input putInvoke(x);
    task c := c+1;
    output putAnswer() to x;
    nextstate dispatch;
endstate;

state normal;
  input putInvoke(x);
    task c := c+1;
    output putAnswer() to x;
    nextstate dispatch;
  input getInvoke(x);
    task c := c-1;
    output getAnswer() to x;
    nextstate dispatch;
endstate;

state full;
  save putInvoke;
  input getInvoke(x);
    task c := c-1;
    output getAnswer() to x;
    nextstate dispatch;
endstate;

state dispatch #unstable ;
  provided c = 0;
    nextstate empty;
  provided 0 < c and c < L;
    nextstate normal;
  provided c = L;
    nextstate full;
endstate;

endprocess; 

endsystem;