{ EP3 ARCHITECTURE

   This Estelle specification of  EP3 architecture is the same as that
   of EP1. (see Appendix 1). The minor differences are described in 
   Sections 3 and 4 and concern channel messages and the way information
   is organized (pointers!).
}
specification EP3 systemactivity;
 default common queue;
 
 const   
   graph_size = any integer;
   maxint = any integer; {maximal available integer value}
 type
   zero_one = 0..1;
   V = 1..graph_size;
   neighbour_representation = array[V] of zero_one;
   graph_representation = array[V] of neighbour_representation;
   L_set = set of  0..graph_size;
   K_el = record
            ng : integer;
            known: L_set;
            stamp: integer
          end;
   K_set = ^KK_el;
   KK_el = record
            kel: K_el;
            next: K_set
           end;

 channel link(R1,R2);
  by R1,R2: done; 
            request(ad:V); 
            new_knowledge(el: K_el); 
            response(el: K_el); 
            trans_knowledge(ad:integer; el: K_el);

 module node activity (ngh: neighbour_representation; nad:V) ;
  ip s_neighbour: array[V] of link(R1);
     r_neighbour: array[V] of link(R2);
 end; {node header}

 body node_body for node;
#include"body1"
 end; {node_body}

#include"init_func"

 modvar 
  nodes: array[V] of node;

initialize
  var i,j:integer; 
  begin
    r := 0.175555987; u := 377003616;  {random generator initial values}
    graph_creation( graph );
    for i:=1 to graph_size do
      init nodes[i] with node_body( graph[i], i );
    for i:=2 to graph_size do
      for j:=1 to i-1 do
        if graph[i,j] = 1 then 
         begin
          connect nodes[i].s_neighbour[j] to nodes[j].r_neighbour[i];
          connect nodes[i].r_neighbour[j] to nodes[j].s_neighbour[i];
         end
  end;

end. {enumeration protocol EP1}

{********************************************************************}
{ EP3 PROCESS (MODULE) BEHAVIOR

   Below  is an Estelle specification of the process behavior 
   as described informally in Sections 3 and 4. 
}
{body node_body for node}
  state 
   idle, wait_response, wait_new_knowledge, termination;    

  var
   known_names: L_set;
   knowledge: K_set;
   own_name: integer;
   own_stamp: integer;
#include"auxiliaries1"

 initialize to idle  
    var i:integer;
    begin
     nghs :=ngh; myad:=nad;
     connect s_pending to r_pending;
     init_node_var     
    end;

  trans
    from idle to termination
     any i: V do
          when r_neighbour[i].done
           name terminal_i:
           begin
             all j:V do
             if ngh[j]=1 then output s_neighbour[j].done
           end;

    from idle to termination
       provided own_name=graph_size
          name terminal:
          begin
             all j:V do
             if ngh[j]=1 then output s_neighbour[j].done
           end;

    from idle to wait_new_knowledge
      priority high
       when r_pending.request(ad)
         name response_to_p_request:
         begin
         el1.ng:=own_name; el1.known:=known_names;
         output s_neighbour[ad].response(el1); 
         requesting:=ad
        end;    
 
      priority medium
        any i: V do
          when r_neighbour[i].request(ad)
          name response_to_request_i:
             begin
             el1.ng:=own_name; el1.known:=known_names;
             output s_neighbour[ad].response(el1); 
             requesting :=ad        
            end;
 
   from idle to wait_response
     provided (own_name=0) or (rename_cond)
         name sending_requests:
         begin
          all i: V do
            if nghs[i]=1 then output s_neighbour[i].request(myad);
        end;

   from idle, wait_new_knowledge, wait_response to same
     any i:V do
      when r_neighbour[i].trans_knowledge(ad, el) {el in K_el}
        name transiting_knowledge_i:
        begin
         is_el(el, knowledge, test);
         if (not test) then
          begin
           add_el(el, knowledge);
           all j:V do
            if (nghs[j]=1) and (j<>ad) then 
               output s_neighbour[j].trans_knowledge(myad, el);
           test_cond(own_name,own_stamp,known_names,knowledge,rename_cond)
           end
        end;

   from wait_new_knowledge to idle
        when r_neighbour[requesting].new_knowledge(el)
         name absorbing_new_knowledge:
         begin
          known_names := known_names + [el.ng]; 
          add_el(el, knowledge); 
          all i:V do
           if (nghs[i]=1) then 
             begin
              el1.ng:=own_name; el1.known:=known_names; el1.stamp:=own_stamp;
              output s_neighbour[i].trans_knowledge(myad, el1);
              if i<>requesting then
                 output s_neighbour[i].trans_knowledge(myad, el)
             end;
          requesting := 0;
          test_cond(own_name,own_stamp,known_names,knowledge,rename_cond)
         end;

   from wait_new_knowledge to same
       any i: V do
        when r_neighbour[i].request(ad)
           name storing_request_i:
           begin
            output s_pending.request(ad)
         end;

   from wait_response to idle
     provided count=ngh_number
      name creating_and_distributing_knowledge:
      begin
       count := 0;
       maxn:=max_resp(resp); 
       if own_name<maxn 
         then own_name:=maxn+1 else own_name:=own_name+1;
       el1.ng:=own_name; el1.known:=known_names;
       choice(maxint, own_stamp); el1.stamp:=own_stamp;
       all i:V do 
         if nghs[i]=1 then
            output s_neighbour[i].new_knowledge(el1);
       test_cond(own_name,own_stamp,known_names,knowledge,rename_cond)
      end;

  from wait_response to same
      any i:V do
       when r_neighbour[i].response(el)
         provided count < ngh_number
          name receiving_responses:
          begin
           resp[i] := el; count := count+1
          end;
                        
 {
end  body node_body
}
{*************************************************************}
{ EP3 AUXILIARY FUNCTIONS AND PROCEDURES

   Below is a detailed description of function and procedures 
   used above. They are internal to the module 'node'  i.e., 
   it is a definition of the part represented by 
   #include"auxiliries1" above.
}

const
   high = 0;   {transition priorities}
   medium = 1;

 ip 
    s_pending: link(R1) individual queue; 
     r_pending: link(R2) individual queue;

type
   NK_el = array[V] of K_el;

  var
   i, j, count,ngh_number, 
   requesting, myad, maxn: integer;
   nghs: neighbour_representation;
   resp: NK_el;
   el1: K_el;


  function maxim(l:L_set): integer;
   var i,max1:integer;
   begin
    max1:=0;
    for i:=1 to graph_size do
     if (i in l) then max1:=i;
    maxim:=max1
   end;

  function max_resp(re:NK_el): integer;
   var i,m,max1,max2:integer;
   begin
    max2:=0;
    for i:=1 to graph_size do
     begin
      m:=maxim(re[i].known);
      if re[i].ng<m 
       then max1:=m
       else max1:=re[i].ng;
      if max1>max2 then max2:=max1     
     end;
    max_resp:=max2
   end;

  function r_cond(el: K_el; l:L_set): boolean;
    var max1,max2:integer; 
     begin
      r_cond:=false;
      max1:=maxim(l-el.known);
      max2:=maxim(el.known-l);
      if max1<max2 then r_cond:=true
     end;

  procedure test_cond(m,st:integer;ls:L_set;k:K_set;var test:boolean);
    var r,s:K_set;
     begin
      test:=false;
      r:=k; 
      while (r<>nil) or (not test) do
       begin
        if ((r^.kel.ng=m) and (r_cond(r^.kel, ls))) or
           ((r^.kel.ng=m) and (r^.kel.known=ls) and (r^.kel.stamp>st))
          then test:= true;
        r:=r^.next
       end
     end;

  procedure is_el(el:K_el; k:K_set; var test: boolean);
    var r:K_set;
     begin
      test:=false;
      r:=k;
      while (r<>nil) or (not test) do 
        begin
         if ((r^.kel.ng=el.ng) and 
             (r^.kel.known=el.known) and (r^.kel.stamp=el.stamp))
           then test:= true;
          r:=r^.next
        end
     end;

  procedure add_el(el:K_el; var k:K_set);
    var r,s:K_set; test: boolean;
     begin
      is_el(el, k, test);
      if (not test) then
       begin
        r:=k;
        while (r^.next<>nil) do
        r:=r^.next;
        new(s); s^.kel.ng:=el.ng; 
        s^.kel.known:=el.known;
        s^.kel.stamp:=el.stamp;
        s^.next:=nil;
        r^.next:=s
       end
     end;

  procedure init_node_var;
      var i:integer;
      begin
       own_name:=0;known_names:=[];
       ngh_number:=0; new(knowledge); 
       knowledge^.kel.ng:=0;knowledge^.kel.known:=[];
       knowledge^.next:=nil;
       for i:=1 to graph_size do
         if nghs[i] = 1 then ngh_number := ngh_number+1;
      end;
  
{***************************************************************}
{ Graph creation procedure and random selection functions are 
  the same as in EP1 (see Appendix 1).
}