APPENDIX: Dynamic Resource Allocation Algorithm in Estelle 
________________________________________________________________

{ This specification is parametrized by several constants like 'Net_Size',
  'Number_of_Resource_Types', etc., and initialization procedures that 
   define distribution of resource pools, agents and tickets, i.e., the 
   configuration of the hole system under consideration }
   
specification Dynamic_Resource_Allocation ;
 default individual queue;
 timescale milisecond;
 const
   Net_Size = any integer;
   Number_of_Resource_Types = any integer;
   Max_Number_of_Pool_Resources = any integer;
   Max_Number_of_Task_Agents = any integer;
   {maximal number of task agents in a node;maximal number of of all agents
     in a node equals Max_Number_of_Task_Agents + 1}
   Number_of_Agent_Tickets= any integer;

 type
   Zero_One = 0..1;
   N_S = 1..Net_Size;
   N_A = 0.. Max_Number_of_Task_Agents; 
   N_TA = 1.. Max_Number_of_Task_Agents; 
   P_R = 0.. Max_Number_of_Pool_Resources; 
   R_T = 1.. Number_of_Resource_Types;
   A_T = 1.. Number_of_Agent_Tickets ;
   Node_Pools = array[R_T] of P_R; 
   Net_Pools = array[N_S] of Node_Pools;
   { for a variable pool of type Net_Pools, pool[i, j] = pool[i][j]=k > 0 
     means that there is a pool of k resources of the type j in the node i; 
     pool[i, j]=0 means that there are no resources of the type j in the node i }
   NNet_Agents = array[N_S] of N_A ;
   { for a variable agent of type NN_ Agents, agent[i] denotes the number 
     of task agents in the node i }
   Agent_Tickets = array[A_T] of integer;
   Node_Tickets = array[N_TA] of Agent_Tickets;
   Net_Tickets = array[N_S] of Node_Tickets;
   { for a variable a_tickets of type Agent_Tickets, a_tickets[i] is a 
      number identifying i-th ticket assigned to an agent in a node}
   T_Plan = array[R_T] of integer;

 channel Link(A, N);
   by A, N: 
     request(sn_ad: N_S; sa_ad: N_TA; rn_ad: N_S; 
                  r_type: R_T; t_ticket, n_req: integer); 
     req_rejected(rn_ad: N_S; ra_ad: N_TA; r_type: R_T; 
                  t_ticket, n_req: integer);
     req_accepted(rn_ad: N_S; ra_ad: N_TA; r_type: R_T; 
                  t_ticket, n_req: integer);
     book(rn_ad:N_S; r_type: R_T; t_ticket:integer);
     book_confirmed(rn_ad: N_S; ra_ad:N_TA; r_type: R_T; t_ticket: integer);
     withdraw(rn_ad: N_S; r_type: R_T; t_ticket: integer);
     rrelease(rn_ad: N_S; r_type: R_T);
     broadcast_add(pl: T_Plan);
     broadcast_sub(pl: T_Plan);
     add(pl: T_Plan);
     sub(pl: T_Plan);

 module Node (ne_pools: Net_Pools; n_agents, n_ad, u_root: integer; 
                  r_root: real; n_tickets: Node_Tickets) ;
  ip node_ips: array[N_A] of Link(A);
 end; {Node header}

 body Node_Body for Node;

 module Task_Agent systemactivity (n_ad: N_S; a_ad: N_TA; ne_pools: Net_Pools; 
                                   tickets: Agent_Tickets; r_root: real);
  ip  agent_ip: Link(A);
 end;

 body Task_Agent_Body for Task_Agent;


  const InTasks = any integer;

  
   type
     Task_RInf = (white, black, red, green);
     Task = array[R_T] of Task_RInf;
     {for a variable tsk of Task: 
      - initial values of tsk shall be restricted to black and white,
      - tsk[j]=white indicates that the task needs resource of type j,
      - tsk[j]=black indicates that the task doesn't need resource of type j, 
      - tsk[j]=green indicates that resource of type j was already requested
          and the request is currently accepted (resource is available),
      - tsk[j]=red indicates that a resource of type j was already requested 
          and the request is currently rejected (resource ic not available),
     T_Plan = array[R_T] of N_S; 
      for a newly created variable tsk of Task and its associated plan of 
       T_Plan, if tsk[j]=white, than plan[j]=i indicates that the node i 
       has a pool of resources of type j, i.e. ne_pool[i, j]>0 ; 
       several different plans are possible} 
     New_Task = ^Task;
     Task_Info = record
                    ticket: integer;
                    tsk: Task;
                    tplan: T_Plan;
                    narg: R_T
                 end;
     Task_Control = array[A_T] of Task_Info;
     Ticket_Control = array[A_T] of Zero_One;
     Exec_Control = array[A_T] of Zero_One;
     Booking_Control = array[A_T] of integer;
     Req_Control = array[A_T] of integer;
     Task_Compet_Control = array[N_S, R_T] of integer;

   channel Internal(S,R);
      by S: wait(t_i: Task_Info);

   ip
      s_wait: Internal(S); r_wait: Internal(R);

   var
      dummy_task, x_task: Task; p: New_Task; t_inf: Task_Info; plan: T_Plan;
      ticket_ctrl: Ticket_Control;
      task_ctrl: Task_Control; 
      booking_ctrl: Booking_Control;
      tc_ctrl: Task_Compet_Control;
      req_ctrl: Req_Control;
      i,j, pool_ad, t_arg: integer; test: boolean; index: A_T; r: real;

function Eq (x,y: Task): boolean;
 var i:integer; 
 begin
     Eq:=true;
     for i:=1 to Number_of_Resource_Types do
        if x[i]<>y[i] then Eq:=false
  end;

procedure draw(p: real; var test: boolean);
(* This procedure draws TRUE with a probalility p*)
 begin
  r := 16807*r-trunc(16807*r);
  if r<=p then test := true else test := false
 end;

procedure TaskCreation( var x: Task);
 var p: New_Task; i: integer; test: boolean;
 begin
   new(p); x:=p^;
   repeat
    for i:=1 to Number_of_Resource_Types do 
      begin 
        draw(0.5, test); 
        if test then x[i]:=white else x[i]:=black
      end
   until (not Eq(x, dummy_task))
 end; 

{the procedure below provides addresses of nodes posessing resources required 
 by the task t; the assumption is that for each resource type in R_T there is 
 a node posessing a pool of resources of that type}
procedure PlanCreation (t: Task; np: Net_Pools; 
                        var plan: T_Plan; var na, arg: integer);
 var i: integer;
  begin
    arg:=0;
    for i:=1 to Number_of_Resource_Types do 
      begin 
        if  t[i]=white then 
         begin
            arg:=arg+1;
            while np[na+1][i]=0 do na:=(na+1) mod Net_Size
         end;
        plan[i]:=na+1
      end
  end;

function ReqPermit (tinf: Task_Info; tc_ctrl: Task_Compet_Control; 
                    npool: Net_Pools): boolean;
 var i: integer; rp: boolean;
 begin
  rp:=true; i:=1;
  while ((rp) and (i<=Number_of_Resource_Types)) do
    if ((tinf.tplan[i]>0) and 
       (tc_ctrl[tinf.tplan[i], i]>=npool[tinf.tplan[i], i])) 
       then rp:=false else i:=i+1;
  ReqPermit:=rp
 end;


{by the procedure below a free ticket is assigned to a task and an
approriate 
 task information (of type Type_Info) is inserted into the Task_Ctrl table}
procedure TicketAssign(var inf: Task_Info);
var j: integer;
begin
  j:=1;
  while ticket_ctrl[j]=1 do j:=j+1;
   ticket_ctrl[j]:=1;
   req_ctrl[j]:=1;
   inf.ticket:=tickets[j];
   task_ctrl[j]:=inf
 end;

procedure FindTicketIndex(t: integer; var ii: A_T);
 begin
   ii:=1;
   while tickets[ii]<>t do ii:=ii+1;
 end;

procedure AddCompete(pl: T_Plan);
var i: integer;
begin
 for i:=1 to Number_of_Resource_Types do
   if pl[i]>0 then tc_ctrl[pl[i], i]:= tc_ctrl[pl[i], i]+1
end;

procedure SubCompete(pl: T_Plan);
var i: integer;
begin
 for i:=1 to Number_of_Resource_Types do
   if pl[i]>0 then tc_ctrl[pl[i], i]:= tc_ctrl[pl[i], i]-1
end;

function IsAllSame(t: Task; colour: Task_RInf): boolean;
 var i: integer;
  begin
   i:=1; 
   while (i<=Number_of_Resource_Types) and 
         ((t[i]=black) or (t[i]=colour)) do i:=i+1;
   if i= Number_of_Resource_Types+1 then IsAllSame:=true else IsAllSame:=false
  end;
    

initialize
  begin
    pool_ad:=0; r:=r_root;
    all i : R_T do dummy_task[i]:=black;
    connect s_wait to r_wait
  end; 

trans
  var j: integer;
  name T0: 
    begin
     for j:=1 to InTasks do
       begin
        TaskCreation(x_task); 
        PlanCreation(x_task, ne_pools, plan, pool_ad, t_arg);
        t_inf.ticket:=0; t_inf.tsk:=x_task; 
        t_inf.tplan:=plan; t_inf.narg:=t_arg;
        output s_wait.wait(t_inf)
       end
    end;

trans
  when r_wait.wait(t_i)
   provided (exist i:A_T suchthat (ticket_ctrl[i]=0)) and 
            (ReqPermit(t_i, tc_ctrl, ne_pools))
   name T1: 
     begin
      TicketAssign(t_i); 
      all i: R_T do 
        if t_i.tsk[i]=white then 
           output agent_ip.request(n_ad, a_ad, t_i.tplan[i], i, t_i.ticket, 1);
      AddCompete(t_i.tplan);
      output agent_ip.broadcast_add(t_i.tplan);
     end;

   when agent_ip.req_accepted(rn_ad, ra_ad, r_type, t_ticket, n_req)

   name T2:
      begin
        FindTicketIndex(t_ticket, index);
        if n_req=req_ctrl[index] then
         begin
          task_ctrl[index].tsk[r_type]:=green;
          if IsAllSame(task_ctrl[index].tsk, green) then
           all i:R_T do 
            if (task_ctrl[index].tsk[i]=green) then 
             output agent_ip.book(task_ctrl[index].tplan[i], i, 
                                  task_ctrl[index].ticket)
         end
       end;

   when agent_ip. req_rejected(rn_ad, ra_ad, r_type, t_ticket, n_req)
    name T3:
     begin
        FindTicketIndex(t_ticket, index);
        if n_req=req_ctrl[index] then
         begin
           task_ctrl[index].tsk[r_type]:=red;
           req_ctrl[index]:=req_ctrl[index]+1;
           SubCompete(task_ctrl[index].tplan);
           all i: R_T do
            if ((task_ctrl[index].tsk[i]=white) or 
               (task_ctrl[index].tsk[i]=green)) then 
               begin
                task_ctrl[index].tsk[i]:=red;
                output agent_ip.withdraw(task_ctrl[index].tplan[i], i, 
                                         task_ctrl[index].ticket)
               end
          end
     end;

   when agent_ip. book_confirmed(rn_ad, ra_ad, r_type, t_ticket)
    name T4:
      begin
         FindTicketIndex(t_ticket, index);
         booking_ctrl[index]:=booking_ctrl[index]+1;
         if (booking_ctrl[index]=task_ctrl[index].narg) then
          begin
           all j: R_T do
            if (task_ctrl[i].tsk[j]=green) then 
              begin
                task_ctrl[i].tsk[j]:=white;
                output agent_ip.rrelease(task_ctrl[i].tplan[j], j)
              end;
           ticket_ctrl[i]:=0; booking_ctrl[i]:=0;
           SubCompete(task_ctrl[index].tplan);
           output agent_ip.broadcast_sub(task_ctrl[index].tplan)
          end
      end;



   when agent_ip.add(pl)
     name T6:
      begin
        AddCompete(pl);
      end;

    when agent_ip.sub(pl)
     name T7:
      begin
        SubCompete(pl);
      end;

trans
  {repeat resource requests being previously withdrawn}
  any i: A_T do
   provided (IsAllSame(task_ctrl[i].tsk, red)) and 
            (ReqPermit(task_ctrl[i], tc_ctrl, ne_pools))
    name T5:
      begin
        AddCompete(task_ctrl[i].tplan);
        all j: R_T do 
          if task_ctrl[i].tsk[j]=red then 
            begin
             task_ctrl[i].tsk[j]:=white;
             output agent_ip.request(n_ad, a_ad, task_ctrl[i].tplan[j], j, 
                                     task_ctrl[i].ticket, res_ctrl[i])
            end
       end;


end; {Task_Agent_Body}

module Resource_Agent systemactivity (n_pools: Node_Pools);
  ip  agent_ip: Link(A);
end;

 body Resource_Agent_Body for Resource_Agent;

 type

   P_Queue = ^Q_Task;
   Q_Task = record
             tnad, taad, ticket: integer; {return address and ticket number}
             accept: boolean; {accept=true means that 'req_accepted' sent}
             next: P_Queue
            end;
   Pool_Control = array[R_T] of P_Queue;
   Free_Res_Control = array[R_T] of P_R;

var
  qt_elem: Q_Task;
  pool_ctrl: Pool_Control;
  free_res_ctrl: Free_Res_Control;
  s, pq: P_Queue; found: boolean;
  rnad, raad, count, qlength, tick, nreq: integer;

procedure Append(qe: Q_Task; var q: P_Queue);
var p,s: P_Queue; i: integer;
begin
  new(s); s^:=qe;
  if q=nil then q:=s
   else
     begin
       p:=q;
       while p^.next<>nil do p:=p^.next;
       p^.next:=s
     end
end;

procedure Remove(tick: integer; var q: P_Queue);
var p,s: P_Queue; i: integer;
begin
  if q^.ticket=tick then q:=q^.next
    else
      begin
        p:=q; s:=p^.next;
        while tick<>s^.ticket do begin p:=s; s:=s^.next end;
        p^.next:=s^.next
      end
end;

procedure Find(q: P_Queue; tick: integer; var p: P_Queue; var found: boolean);
begin
   p:=q; found:=false;
   while ((p<>nil) and (tick<>p^.ticket)) do p:=p^.next;
   if p<>nil then found:=true
end;


procedure Qtest(q: P_Queue; tick: integer; var count, qlength: integer);
var p,s: P_Queue; 
begin
       p:=q; count:=0; qlength:=0;
       repeat
         if p<>nil then 
          begin
            s:=p^.next;
            qlength:=qlength+1;
            if p^.ticket>tick then count:=count+1;
            p:=s
          end;
       until p=nil
end;

procedure AdjustQ(var p,q: P_Queue);
begin
      p:=q;
      while ((p^.accept) and (p^.next<>nil)) do p:=p^.next;
      if not (p^.accept) then p^.accept:=true
end;

initialize
   begin
     all i:R_T do 
      begin 
       free_res_ctrl[i]:=n_pools[i];
       new(pq); pq:=nil; pool_ctrl[i]:=pq 
      end
   end;

trans
   when agent_ip.request(sn_ad, sa_ad, rn_ad, r_type, t_ticket, n_req)
    name R1:
      begin
       QTest(pool_ctrl[r_type], t_ticket, count, qlength);
       if count<free_res_ctrl[r_type] then
        begin
          qt_elem.tnad:=sn_ad; qt_elem.taad:=sa_ad; qt_elem.ticket:=t_ticket; 
          qt_elem.n_r:=n_req; qt_elem.accept:=false; qt_elem.next:=nil;
          if qlength<free_res_ctrl[r_type] then
           begin
            output agent_ip.req_accepted(sn_ad, sa_ad, r_type, t_ticket, n_req);
            qt_elem.accept:=true
           end;
          Append(qt_elem, pool_ctrl[r_type])
        end
        else
         output agent_ip.req_rejected(sn_ad, sa_ad, r_type, t_ticket, n_req)
       end;

   when agent_ip.book(rn_ad, r_type, t_ticket)
     name R2:
      begin
        free_res_ctrl[r_type]:=free_res_ctrl[r_type]-1;
        Find(pool_ctrl[r_type], t_ticket, pq, found);
        rnad:=pq^.tnad; raad:=pq^.taad; nreq:=pq^.n_r;
        output agent_ip.book_confirmed(rnad, raad, r_type, t_ticket);
        Remove(t_ticket, pool_ctrl[r_type])
      end;

   when agent_ip.withdraw(rn_ad, r_type, t_ticket)
     name R3:
      begin
        Find(pool_ctrl[r_type], t_ticket, pq, found);
        if found then
         begin
         if ((pq^.next<>nil) and (pq^.accept)) then 
          begin
             AdjustQ(s, pq);
             rnad:=s^.tnad; raad:=s^.taad; nreq:=s^.n_r; tick:=s^.ticket;
             output agent_ip.req_accepted(rnad, raad, r_type, tick, nreq)
           end;
          Remove(t_ticket, pool_ctrl[r_type])
         end
      end;

   when agent_ip.rrelease(rn_ad, r_type)
     name R4:
      begin
        free_res_ctrl[r_type]:=free_res_ctrl[r_type]+1;
        if (pool_ctrl[r_type]<>nil) then
         if not (pool_ctrl[r_type]^.accept) then 
          begin
           pool_ctrl[r_type]^.accept:=true;
           rnad:= pool_ctrl[r_type]^.tnad; raad:= pool_ctrl[r_type]^.taad;         
           tick:= pool_ctrl[r_type]^.ticket; nreq:=pool_ctrl[r_type]^.n_r;
           output agent_ip.req_accepted(rnad, raad, r_type, tick, nreq)
          end;
       end;


 end; {Resource_Agent_Body}
 

 modvar
   t_agent_var: array[N_TA] of Task_Agent;
   r_agent_var: Resource_Agent;

 initialize
  var m : integer;
  begin
    if n_agents<>0 then
      for m:=1 to n_agents do
        begin
          init t_agent_var[m] with Task_Agent_Body(n_ad, m, ne_pools, 
                                                   n_tickets[m], (1/m)*r_root);
          attach node_ips[m] to t_agent_var[m].agent_ip
        end;
    if (exist j: R_T suchthat (ne_pools[n_ad, j]>0)) then
        begin
          init r_agent_var with Resource_Agent_Body(ne_pools[n_ad]);
          attach node_ips[0] to r_agent_var.agent_ip
        end
  end;


 end; {Node_Body}

module Network systemactivity;
  ip net_ips: array[N_S, N_A] of Link(N);
end; {Network header}

body Network_Body for Network;

initialize begin end;

trans
 any i:N_S; j : N_TA do
  when net_ips[i,j].request(sn_ad, sa_ad, rn_ad, r_type, t_ticket, n_req)
   begin
    output net_ips[rn_ad, 0].request(sn_ad, sa_ad, rn_ad, 
                                     r_type, t_ticket, n_req)
   end;

  when net_ips[i,0].req_rejected(rn_ad, ra_ad, r_type, t_ticket, n_req)
   begin
    output net_ips[rn_ad, ra_ad]. req_rejected(rn_ad, ra_ad, 
                                               r_type, t_ticket, n_req)
   end;

  when net_ips[i,0]. req_accepted(rn_ad, ra_ad, r_type, t_ticket, n_req)
   begin
    output net_ips[rn_ad, ra_ad]. req_accepted(rn_ad, ra_ad, 
                                               r_type, t_ticket, n_req)
   end;

  when net_ips[i,j].book(rn_ad, r_type, t_ticket)
   begin
    output net_ips[rn_ad, 0].book(rn_ad, r_type, t_ticket)
   end;

  when net_ips[i,0]. book_confirmed(rn_ad, ra_ad, r_type, t_ticket)
   begin
    output net_ips[rn_ad, ra_ad].book_confirmed(rn_ad, ra_ad, 
                                                r_type, t_ticket)
   end;

  when net_ips[i,j].withdraw(rn_ad, r_type, t_ticket)
   begin
    output net_ips[rn_ad, 0].withdraw(rn_ad, r_type, t_ticket)
   end;

  when net_ips[i,j]. rrelease(rn_ad, r_type)
   begin
    output net_ips[rn_ad, 0]. rrelease(rn_ad, r_type)
   end;

  when net_ips[i,j].broadcast_add(pl)
   begin
    all k: N_S; l: N_TA do
        if ((k<>i) or (l<>j)) then output net_ips[k,l].add(pl)
   end;

  when net_ips[i,j].broadcast_sub(pl)
   begin
    all k: N_S; l: N_TA do
        if ((k<>i) or (l<>j)) then output net_ips[k,l].sub(pl)
   end;

end; {Network_Body}

var
 r: real; 
 u: integer;
 ne_pools: Net_Pools; 
 ne_agents: NNet_Agents;
 ne_tickets: Net_Tickets;

 modvar 
  nodes: array[N_S] of Node; 
  medium : Network;

initialize
  var i,j:integer; 
  begin
  r := 0.175555987; u := 377003616;
 { PoolsDitribution (ne_pools); }
 { AgentsDistribution (ne_agents);}
 { TicketDistribution (ne_tickets);}
   init medium with Network_Body;
   for i:=1 to Net_Size do
      begin
        init nodes[i] with Node_Body( ne_pools, ne_agents[i], i, 
                                      i*u, (1/i)*r, ne_tickets[i]);
        for j:=0 to ne_agents[i] do
        connect nodes[i].node_ips[j] to medium.net_ips[i,j]
      end
  end;

end. { Dynamic_Resource_Allocation }