public class PC {
  public static void main(String[] args) {
    Buffer   b = new Buffer(3);
    Producer p = new Producer(b);
    Consumer c = new Consumer(b);
  }
}
class HaltException extends Exception{}


interface BufferInterface {
  public void   put(Object x);
  public Object get() throws HaltException;
  public void   halt();
}

/**
 * @observable
 *   EXP Full(this): (usedSlots == size);
 *   EXP Empty(this): (usedSlots == 0);
 *   EXP putPtrRange(this): (putPtr>=0 && putPtr<=b);
 *   EXP getPtrRange(this): (getPtr>=0 && getPtr<=b);
 */

class Buffer implements BufferInterface {
  protected int SIZE;
  protected Object[] array; 
  protected int putPtr = 0; 
  protected int getPtr = 0;     
  protected int usedSlots = 0;
  protected boolean halted = false;


/**
 * @assert
 *    PRE PositiveBound: ( b>0 );
 */
    public Buffer(int b)
    {
      SIZE = b;   
      array = new Object[b];
    }


  public synchronized void put(Object x) { 
    while (usedSlots == SIZE)
      try { 
        System.out.println("producer wait");
        wait(); 
      } catch(InterruptedException ex) {}; 
    System.out.println("put at "+putPtr);
    array[putPtr] = x;
    putPtr = (putPtr + 1) % SIZE;  
    if (usedSlots == 0) notifyAll();
    usedSlots++;
  }

  public synchronized Object get() throws HaltException{ 
    while (usedSlots == 0 & !halted) 
      try {
        System.out.println("consumer wait"); 
        wait(); 
      } catch(InterruptedException ex) {}; 
    if (usedSlots == 0) {
      System.out.println("consumer gets halt exception");
      HaltException he = new HaltException();
      throw(he);
    };
    Object x = array[getPtr];
    System.out.println("get at "+getPtr);
    array[getPtr] = null;
    getPtr = (getPtr + 1) % SIZE;
    if (usedSlots == SIZE) notifyAll();
    usedSlots--;
    return x;
  }

  public synchronized void halt(){
    System.out.println("producer sets halt flag");
    halted = true;
    notifyAll();
  }
}

class Attribute{
  public int attr;

  public Attribute() { attr = 0; }
  public Attribute(int attr){
    this.attr = attr;
  }
}

class AttrData extends Attribute{
  public int data;

  public AttrData(int attr,int data){
    this.attr = attr;
    this.data = data;
  }
}

class Producer extends Thread {
  static final int COUNT = 6;
  private Buffer buffer;

  public Producer(Buffer b) {
    buffer = b;
    this.start();
  }
/**
 * @observable
 *    LOCATION[run1] ProducerRun(this);
 */
  public void run() {
    for (int i = 0; i < COUNT; i++) {
      AttrData ad = new AttrData(i,i*i);
      buffer.put(ad);
      yield();
    }
  run1:
    buffer.halt();
  }
}

class Consumer extends Thread {
  private Buffer buffer;

  public Consumer(Buffer b) {
    buffer = b;
    this.start();
  }
/**
 * @observable
 *    LOCATION[run1] ConsumerRun(this);
 */
  public void run() {
    int count = 0;
    AttrData[] received = new AttrData[10];
    try{
      while (count < 10){
        received[count] = (AttrData)buffer.get();
        count++;
      }
    }
    catch(HaltException e){};
  run1:
    System.out.println("Consumer ends");
  }
}