public class RW {
  // operations -- abstract communication channels between processes.
  private static op void start_read();
  private static op void end_read();
  private static op void start_write();
  private static op void end_write();

  private static process RWAllocator {
    int nr = 0, nw = 0; // number of readers (writers) accessing database
    while (true) {
      // inni is JR's input statement, which does a multi-way receive.
      // it services one invocation of one of the given ops on each iteration
      // of the enclosing while loop.
      // the st (such that) clauses specifies the conditions
      // under which to service the particular invocation.
      inni void start_read()  st nw == 0            { nr++; }
      []   void end_read()                          { nr--; }
      []   void start_write() st nw == 0 && nr == 0 { nw++; }
      []   void end_write()                         { nw--; }
    }
  }

  // number of reader and writer processes
  // number of times they want to read and write
  private static final int READERS = 4;
  private static final int WRITERS = 3;
  private static final int RIters = 3;
  private static final int WIters = 2;

  private static process reader( (int id = 0; id < READERS; id++) ) {
    for (int iters = 1; iters <= RIters; iters++) {
      call start_read(); // call is synchronous.
                         // reader waits for the invocation to complete.
                         // so reader waits until RWAllocator gives it the OK.
      //////////////////... // read
      send end_read();  // send is asynchronous.
                        // reader continues after invocation is sent.
    }
    System.out.println("reader done "+id);
  }

  private static process writer( (int id = 0; id < WRITERS; id++) ) {
    for (int iters = 1; iters <= WIters; iters++) {
      call start_write();
      //////////////////... // write
      send end_write();
    }
    System.out.println("writer done "+id);
  }

  // main needn't do anything since have statically created processes
  public static void main(String [] args) {
  }
}