_monitor(Reader_Writer)
   op Start_Read(i : int), End_Read(i : int)
   op Start_Write(i : int), End_Write(i : int)
_body(Reader_Writer)
   var Readers: int := 0
   var Writing: bool := false
   _condvar(OK_to_Read); _condvar(OK_to_Write)

   _proc(Start_Read(i))
      if Writing -> _wait(OK_to_Read)
      [] not _empty(OK_to_Write) ->
         write("   age=", age(), "reader", i, "has to WAIT")
         _wait(OK_to_Read) /* new incoming readers cannot starve writers */
      fi
      Readers := Readers + 1
      write("   age=", age(), "reader", i, "has begun reading, Readers=",
         Readers)
      _signal(OK_to_Read)  /* when a writer finishes, all waiting readers start */
   _proc_end
  
   _proc(End_Read(i))
      Readers := Readers - 1
      write("   age=", age(), "reader", i, "finished reading, Readers=",
         Readers)
      if Readers = 0 -> _signal(OK_to_Write) fi
   _proc_end
  
   _proc(Start_Write(i))
      if Readers != 0 or Writing -> _wait(OK_to_Write) fi
      Writing := true
      write("      age=", age(), "WRITER", i, "has begun Writing,")
   _proc_end
  
   _proc(End_Write(i))
      Writing := false
      write("   age=", age(), "WRITER", i, "has finished Writing")
      if not _empty(OK_to_Read) -> _signal(OK_to_Read)
      [] else -> _signal(OK_to_Write)  /* nor do writers starve readers */
      fi
   _proc_end
_monitor_end