Readers/Writers ( 2 )

package rw is

  n : constant integer := 2; -- number of readers/writers

  task reader_1;
  task reader_2;

  task writer_1;
  task writer_2;

  task control is
    entry start_read;
    entry stop_read;
    entry start_write;
    entry stop_write;
  end control;

end rw;

package body rw is

  task body reader_1 is
    done : boolean;
  begin
    loop
      control.start_read;   --event[{reader_1_start_read}]
      control.stop_read;

      exit when done;

    end loop;
  end reader_1;

  task body reader_2 is
    done : boolean;
  begin
    loop
      control.start_read;
      control.stop_read;

      exit when done;

    end loop;
  end reader_2;


  task body writer_1 is
    done : boolean;
  begin
    loop
      control.start_write;   --event[{writer_1_start_write}]
      control.stop_write;    --eventb[{writer_1_stop_write}]
      exit when done;
    end loop;
  end writer_1;

  task body writer_2 is
    done : boolean;
  begin
    loop
      control.start_write;   --event[{writer_2_start_write}]
      control.stop_write;    --eventb[{writer_2_stop_write}]
      exit when done;
    end loop;
  end writer_2;


  task body control is
    done : boolean;
    readers : integer range 0 .. n;
    writer  : boolean;
  begin
    readers := 0;      --event[{readers=0}]
    writer := false;   --event[{w=f}]
    loop    
      select
        when (not writer) =>
          accept start_read;        --eventb[{wis=f}]
          readers := readers + 1;   --event[{readersinc}]
          null;
        or 
          accept stop_read;
	  readers := readers - 1;   --event[{readersdec}]
          null;
        or when (not writer) and (readers = 0) =>
          accept start_write;     --eventb[{wis=f},{readersis=0}] event[{any_writer_wrote}]
	  writer := true;         --event[{w=t}]
          null;
        or
          accept stop_write;
          writer := false;        --event[{w=f}]
        null;
      end select;

      exit when done;

    end loop;
  end control;
end rw;