--
-- Basic types
--

type NetID is integer;
type NodeID is integer;
-- These are the two components of an address.
--
-- Global counters:     
--     
-- These constants define the number of entities to be created.
num_enclaves : integer is get_number("Number of enclaves: ");
num_ws	     : integer is num_enclaves*2;
num_messages : integer is get_number("Number of messages per workstation: "); 
--
-- These counters keep track of the number of nodes etc. 
-- that have been created.
-- They are used to ensure unique network addresses, etc.
--
node_number : array [NetID] of ref(integer) is
					  (0 .. num_enclaves, 
					  default is ref_to(integer, 0));
COTS_workstation_number : ref(integer) is ref_to(integer, 0);
user_number     : ref(integer) is ref_to(integer, 0);
firewall_number : ref(integer) is ref_to(integer, 0);
WAN_net_no      : integer is 0;
lan_number      : ref(integer) is ref_to(integer, 0);
enclave_number  : ref(integer) is ref_to(integer, 0);

function randomNet() return NetID is
begin
    return (randomNumber() mod ($lan_number))+1;
end;

type Address is interface
-- An adress object represents the address of a node on a network
-- Defines an equality function, and the address itself as a pair of IDs
-- If inheritance were supported then we would simply include the equality type
provides
    function =  ( RHS : Address ) return boolean;
    net_no: NetID;
    node_no: NodeID;
end;

module randomAddress() return Address is
-- Every call to this module generator results in an address.
-- Which address will be returned is unknown
    net_no : NetID is randomNet();
    node_no : NodeID is (randomNumber() mod $(node_number[net_no]))+1;
    function = (RHS: Address) return boolean is
    begin
	return (net_no = RHS.net_no and node_no = RHS.node_no);
    end;
end randomAddress;

module newAddress (net : NetID) return Address is
-- Generates a new address for a node on the net given as a parameter.
-- Increments the global counter for the number of nodes on this net.
    net_no : NetID is net;
    node_no : NodeID is $(node_number[net_no])+1;
    function = (RHS: Address) return boolean is
    begin
	return (net_no = RHS.net_no and node_no = RHS.node_no);
    end;
initial
    node_number[net_no] := node_no;
end;

--     
--  data     
--     

type Data is integer;
-- Simple data for now.

function newData() return Data is
begin
   return randomNumber();
end;