/******************************************/
/* User Guide Example: the Bounded Buffer */
/* Assertions are expected to be true.    */
/*      See Doc/jpf-guide.ps              */
/*      and Doc/jpf-translation.ps        */
/******************************************/

/*
Explanation:
------------

A producer puts values into a bounded buffer, while a consumer
takes them out and stores them in a local array. The assertions
specify that the right number of values have been received, and in the
right order. Note that there are several interleavings between
producer and consumer. Examples:

  put put put get get get ...
  put get put get ...
  put put get put ....
  ...

The size of the buffer and the number
of elements put into the buffer by the
producer are defined as constants.

import gov.nasa.jpf.jvm.Verify;

class Parameters{
  int AttrData_size = 6;
}


class HaltException extends Exception{}


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


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

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

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

  public synchronized void halt(){
    Verify.print("producer sets halt flag");
    halted = true;
    notifyAll();
  }
}

class Attribute{
  public int attr;

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

class AttrData extends Attribute{
  public int data;

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

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

  public Producer(Buffer b) {
    buffer = b;
    this.start();
  }

  public void run() {
    for (int i = 0; i < COUNT; i++) {
      AttrData ad = new AttrData(i,i*i);
      buffer.put(ad);
//      yield();
    };
    buffer.halt();
  }
}

class Consumer extends Thread {
  private Buffer buffer;

  public Consumer(Buffer b) {
    buffer = b;
    this.start();
  }

  public void run() {
    int count = 0;
    AttrData[] received = new AttrData[10];
    try{
      while (count < 10){
        received[count] = (AttrData)buffer.get();
        count++;
      }
    }
    catch(HaltException e){};
    Verify.print("Consumer ends");
    Verify.assertTrue("count != COUNT",count == Producer.COUNT);
    for (int i = 0; i < count; i++){
      Verify.assertTrue("wrong value received",received[i].attr == i);}
  }
}

public class JPFBBex {
  public static void main(String[] args) {
    Buffer   b = new Buffer();
    Producer p = new Producer(b);
    Consumer c = new Consumer(b);
  }
}