-- A file attempting to reproduce some of payments system behaviour
-- Attempting to add behaviour of BA sending new payment data.
-- 11/5/1998

-- Three parts: Interface, Office, Centre

-- Office waits on a port, looks up paymnets in array, outputs message. 
-- Enquires of the centre for unknown claimants

-- Centre receives and responds to enquiries from offcies.

package POCL_types is
-- A way to be able to use a pair as a parameter in a message
-- OP is a pair of integers: (Office_id, Person_id)
type OP is array ( 0 to 1) of integer; 
end POCL_types;


package body POCL_types is
end POCL_types;

use work.POCL_types.all;

-- ------------------------------------------------------------------------------
interface POCL1 is
between ALLOFFICE, OFFICE1, OFFICE2, CENTRE_PORT;

message UNKNOWN_NINO( enq: OP)             is from ALLOFFICE to CENTRE_PORT;    takes 25 ns; end;
message ACK_UNKNOWN_NINO( off_id: integer) is from CENTRE_PORT    to ALLOFFICE; takes 25 ns;  end;

message PAYMENT_AMOUNT_1( Amount : integer) is from CENTRE_PORT to OFFICE1; takes 25 ns;  end;
message PAYMENT_AMOUNT_2( Amount : integer) is from CENTRE_PORT to OFFICE2; takes 25 ns;  end;

end POCL1;

-- ******************************************************************************
entity CENTRE is
   port ( cen1 : inout boolean := false );
   interface port ( iport : CENTRE_PORT of POCL1 );
end;

architecture one of CENTRE is

type PAYMENTS is array ( 1 to 10 ) of integer;

-- the bit that actually does something
begin
  process
  variable q: OP;  
  variable amount: integer;
  variable data: PAYMENTS := ( 11,12,13,14,15,16,17,18,19,20 );
  
  begin
--    wait until cen1;
--    cen1 <= true, false after 15 ns;

    receive iport.UNKNOWN_NINO(q);
    assert false report "centre received UNKNOWN_NINO" severity note;
    send iport.ACK_UNKNOWN_NINO( q(0) );
    assert false report "CENTRE sent ACK" severity note;
    wait for 25 ns;	  -- for the office to start listening
    if  q(0) = 1 
      then  
		send iport.PAYMENT_AMOUNT_1( data( q(1) ) );
	    assert false report "CENTRE sends amount to office 1" severity note;
	  else
		send iport.PAYMENT_AMOUNT_2( data( q(1) ) );
		assert false report "CENTRE sends amount to office 2" severity note;
    end if;
  	data( q(1) ) := 0; 
  end process;
end; 
-- ----------------------------------------------------------------------------------
-- An office, OFFICE1

entity OFFICE1 is 
	port ( office1 : inout boolean := false );
	interface port ( send_port : ALLOFFICE of POCL1; 
	                 receive_port: OFFICE1 of POCL1 );
end;

architecture one of OFFICE1 is
type OFF_PAYMENTS is array ( 1 to 10 ) of integer;

signal ack : boolean:=false;
signal idno : integer;
signal who : integer:= 6;
signal how_much : integer := 0;

Activity send_enquiry( enq : inout OP ) is
serial
assert false report "Office 1 starts to send UNKNOWN_NINO" severity note;

while ack = false loop
--	assert false report "Office 1 sends unknown nino MESSAGE" severity note;
	send send_port.UNKNOWN_NINO(enq);
	end loop;
end;

Activity get_ack( off_id : inout integer) is
serial
idno <= 0;
ack <= false;

while idno /= off_id loop 
	receive send_port.ACK_UNKNOWN_NINO( idno );	
	end loop;
assert false report "  ACK of UNKNOWN_NINO received at Office 1" severity note;
ack <= true, false after 75 ns;

end;

activity sendit( e : inout OP ) is
parallel
send_enquiry(e);
get_ack(e(0));
end;

begin
-- the bit that does things

process
variable off_data: OFF_PAYMENTS := ( 11,12,13,14,15, -1,-1,-1,-1,-1 );
variable nino : integer;
variable benefit : integer;
variable mess : OP;

    begin

	wait until office1;
	office1 <= true, false after 15 ns;
	nino := who;

	if off_data(nino) /= -1
	  then  -- its here
	  
	  assert false report "Nino known, pay out from OFFICE1 local data" severity note;
	  how_much <= off_data(nino);
	  off_data(nino) := 0;
	  
	  else  -- get data from the centre
	  
	  mess(0) := 1;
	  mess(1) := nino;
	  sendit( mess );

	  receive receive_port.PAYMENT_AMOUNT_1( benefit );
	  
	  assert false report "OFFICE1 receives data from centre" severity note;	  
	  how_much <= benefit;
	end if;
	
	end process;
end;
--  *****************************************************************1
-- Another office, OFFICE2

entity OFFICE2 is 
	port ( office2 : inout boolean := false );
	interface port ( send_port : ALLOFFICE of POCL1; 
	                 receive_port: OFFICE2 of POCL1 );
end;

architecture one of OFFICE2 is
type OFF_PAYMENTS is array ( 1 to 10 ) of integer;

signal ack : boolean:=false;
signal idno : integer;
signal who : integer:= 2;
signal how_much : integer := 0;

Activity send_enquiry( enq : inout OP ) is
serial
assert false report "Office 2 starts to send UNKNOWN_NINO" severity note;
while ack = false loop
	send send_port.UNKNOWN_NINO(enq);
	end loop;
end;

Activity get_ack( off_id : inout integer) is
serial
idno <= 0;
ack <= false;

while idno /= off_id loop 
	receive send_port.ACK_UNKNOWN_NINO( idno );	
	end loop;
assert false report "  ACK of UNKNOWN_NINO received at Office 2" severity note;
ack <= true, false after 75 ns;

end;

activity sendit( e : inout OP ) is
parallel
send_enquiry(e);
get_ack(e(0));
end;

begin
-- the bit that does things

process
variable off_data: OFF_PAYMENTS := ( -1,-1,-1,-1,-1, 16, 17, 18, 19, 20 );
variable nino : integer;
variable benefit : integer;
variable mess : OP;

    begin

	wait until office2;
	office2 <= true, false after 15 ns;
	nino := who;

	if off_data(nino) /= -1
	  then  -- its here
	  
	  assert false report "Nino known, pay out from OFFICE2 local data" severity note;
	  how_much <= off_data(nino);
  off_data(nino) := 0;
	  
	  else  -- get data from the centre
	  
	  mess(0) := 2;
	  mess(1) := nino;
	  sendit( mess );

	  receive receive_port.PAYMENT_AMOUNT_2( benefit );
	  
	  assert false report "OFFICE 2 receives data from centre" severity note;	  
	  how_much <= benefit;
	end if;
	
	end process;
end;


-- ******************************************************************1
entity atestpoc2 is 
end atestpoc2;

Architecture one of atestpoc2 is

interface signal i1: POCL1;

component CENTRE
 port ( cen1 : inout boolean := false );
 interface port ( iport : CENTRE_PORT of POCL1 );
end component;

component OFFICE1
  port( office1 : inout boolean := false );
  interface port ( send_port : ALLOFFICE of POCL1; 
                   receive_port: OFFICE1 of POCL1 );
end component;



component OFFICE2
  port( office2 : inout boolean := false );
  interface port ( send_port : ALLOFFICE of POCL1; 
                   receive_port: OFFICE2 of POCL1 );
end component;




begin

first_centre : CENTRE
  interface map ( iport => i1 );

first_office : OFFICE1
  interface map ( send_port => i1, receive_port => i1 );


second_office : OFFICE2
  interface map ( send_port => i1, receive_port => i1 );


end;