system ReadersWriters {

  const MAX {
  	Readers = 2;
  	Writers = 2;
  }

  const ALLOWED {
  	Readers = 2;
  	Writers = 2;
  }

  int activeReaders := 0;
  int activeWriters := 0; 

 
  active[MAX.Readers] thread Reader() {

    loc starting: 
      when activeReaders < ALLOWED.Readers && activeWriters == 0 
      do { activeReaders := activeReaders + 1; }
      goto reading;                  

    loc reading: 
      do { }
      goto finishing;                 

    loc finishing: 
      do { activeReaders := activeReaders - 1; }
      goto done;
      
    loc done:
      do {}
      goto starting;
     
      do {}
      return;

  }

  active[MAX.Writers] thread Writer() {

    loc starting:
      when activeReaders == 0 && activeWriters == 0 
      do { activeWriters := activeWriters + 1; }
      goto writing;                

    loc writing: 
      do { }
      goto finishing;                 

    loc finishing: 
      do { activeWriters := activeWriters - 1; }
      goto done;

	loc done:
	  do {}
	  goto starting;
	  
	  do {}
	  return;
  }

}