Readers/Writers (3)

package rw is

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

  task reader_1;
  task reader_2;
  task reader_3;

  task writer_1;
  task writer_2;
  task writer_3;

  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 reader_3 is
    done : boolean;
  begin
    loop
      control.start_read; 
      control.stop_read;
      exit when done;
    end loop;
  end reader_3;


  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 writer_3 is
    done : boolean;
  begin
    loop
      control.start_write; 
      control.stop_write; 
      exit when done;
    end loop;
  end writer_3;


  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;