{************************************************************************}
{
   This is Estelle specification of the architecture of enumeration 
   protocol EP1, for a graph of size given by 'graph_size' constant and
   generated by 'graph_creation' procedure in 'initialize' part of the
   specification. The procedure creates the graph in form of a two-
   dimension and binary array, where (i, j) has value 1 iff nodes 
   represented by i and j are in the graph relation. Each row i of the 
   array defines i-th neighbourhood.

   Each process (node) of the network (graph) is defined by module 'node' 
   with its input and output ports specified by vectors of  length 
   'graph_size' of interaction points (ip). These proceses are 
   represented by instances of module 'node' and accessed by module 
   variables ('modvar' declaration), nodes[i].  Ports of the instances 
   are then connected in  part 'initialize' of the specification, by
   communication channels of type 'link(R1, R2)' and according to the 
   edge structure of the graph. Messages circulate through channels. 
   Allowed messages are defined within channel 'link'.
   
   Sets of names ('L_set') are defined as sets of integers from the set 
   'V = 1 .. graph_size', while pairs composed of a name and a set of 
   names and being elements of each node knowledge, have record 'K_el'
   definition.

   Knowledge itself is represented by an array of 'max' length and is
   actual contents is reduced to that 'K_el' elements that are not equal
   to (max, empty). This not very elegant solution is chosen because of
   the Estelle restrictions that do not tolerate dynamic arrays (the same
   concern array of interaction points) and forbid pointers in messages.

   #include"body" refers to the part of the specification, which 
   describes process behavior as described informally in Section 2.

   #include"init_func0" contains definitions of some global random 
   selection functions as well as 'graph_creation' procedure if one 
   wants create a graph automatically.

   Both 'includes' are specified separately below.

   To run the specification all constants have to be initialized to 
   specific values (e.g.,  'any integer' shoud be replaced by a concrete
   value).

   'systemactivity' attribute of the specification means that behavioral
   semantics are given by interleaving.
}
{***********************************************************************}

specification EP1 systemactivity;
 default common queue;
 const
   graph_size = any integer;
   max = any integer;      {greater than graph_size, eg. graph_size^2}

 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;
          end;
   K_set = array[1..max] of K_el;

 channel link(R1,R2);
   by R1,R2: request(ad:V);
                     new_knowledge(l:L_set; k:K_set); 
                     response(l:L_set; k:K_set; n:integer) ;

 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"body0"
 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}


{********************************************************************}
{ 
   Below  is an Estelle specification of the process behavior. 
   An Estelle guarded command is called transition and consists of 
   clauses (begining with 'when', 'from', provided', etc.) describing
   guards and followed by actions (starting with 'name' and described
   by statements between 'begin' and 'end'). 

   In 'initialize' certain values are initialized.

   Transition priorities gives a possibility of excluding the
   non-determinism. 
}
{********************************************************************}


{body node_body for node}
 state 
  idle, wait_response, wait_new_knowledge, termination;

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

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

  trans
    from idle to termination
      provided (exist i:1..max suchthat (knowledge[i].ng=graph_size))
        priority highest
         name terminal:
         begin end;

    from idle to wait_new_knowledge
      priority medium
       when r_pending.request(ad)
        name response_to_p_request:
        begin
         output s_neighbour[ad].response(known_names,knowledge,own_name); 
         requesting:=ad
        end;    
 
    from idle to wait_new_knowledge
     any i: V do
      priority low
       when r_neighbour[i].request(ad)
        name response_to_request_i: 
        begin
         output s_neighbour[ad].response(known_names,knowledge,own_name);
         requesting :=ad        
        end;
 
    from idle to wait_response
        name sending_requests:
        begin
          all i: V do
            if nghs[i]=1 then output s_neighbour[i].request(myad);
        end;

    from termination to termination
     priority medium
      when r_pending.request(ad)
       name terminal_response:
       begin
        output s_neighbour[ad].response(known_names, knowledge, own_name)
       end;

    from termination to termination
     any i: V do
      when r_neighbour[i].request(ad)
       name terminal_response_i:
       begin
        output s_neighbour[ad].response(known_names, knowledge, own_name)
       end;

    from termination to termination
         any i: V do
          when r_neighbour[i].new_knowledge
            name ignoring:
            begin end;

    from wait_new_knowledge to idle
        when r_neighbour[requesting].new_knowledge(l, k)
          name absorbing_new_knowledge:
          begin
            known_names := l; knowledge := k; requesting := 0
          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;
           if (own_name=0) or 
              (exist j:1..max suchthat 
                 rename_cond(knowledge[j], known_names, own_name))
             then 
              begin
               maxname(maxn); new_know(maxn); own_name:=maxn+1
              end;
           all i:V do 
            if nghs[i]=1 then 
               add(resp_k[i], knowledge);
           all i:V do
            if nghs[i]=1 then
               output s_neighbour[i].new_knowledge(resp_l[i], knowledge);
         end;
                 
   from wait_response to same
      any i:V do
       when r_neighbour[i].response(l, k, n)
         provided count < ngh_number
           name receiving_responses:
           begin
              resp_l[i] := l; resp_k[i] := k;
              resp_n[i] := n; count := count+1
            end;

{end  body node_body}


{*********************************************************************}
{
  Below is a detailed description of function and procedures used
  above and internal to the module 'node'  i.e., the part represented 
  by #include"auxiliries0"
}
{*********************************************************************}

const
   highest = 0;   {transition priorities}
   medium = 1;
   low = 2;

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

var
    i,j,count,ngh_number, requesting, myad,maxn: integer;
    nghs: neighbour_representation;
    resp_l : array[V] of L_set;
    resp_k : array[V] of K_set;
    resp_n : array[V] of integer;            

  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 rename_cond(el: K_el; l:L_set; m:integer): boolean;
    var max1,max2:integer; rc:boolean;
     begin
      rc:=false;
      if el.ng=m then
        begin
          max1:=maxim(l-el.known);
          max2:=maxim(el.known-l);
          if max1<max2 then rc:=true
        end;
      rename_cond:=rc
     end;

  function is_el(el:K_el; k:K_set): boolean;
   var j:integer; cc:boolean;
   begin
    j:=1; cc:=false;
    while (j<=max) and (not cc) do
     if (k[j].ng=el.ng) and (k[j].known=el.known) 
      then cc:=true else j:=j+1;
    is_el:=cc
   end;

  procedure add_el(el:K_el; var k:K_set);
   var i:integer;
   begin
    if (not is_el(el, k)) then
     begin
      i:=1;
      while k[i].ng<>max do i:=i+1;
      k[i].ng:=el.ng; k[i].known:=el.known
     end
   end;

  procedure add(k1:K_set; var k2:K_set);
   var i,j:integer; cc:boolean;
   begin
     for i:=1 to max do
       add_el(k1[i], k2);
   end;

  procedure maxname(var m:integer);
   var i,j:integer;
   begin
      m:=own_name;
      for i:=1 to graph_size do
        begin
         if (nghs[i]=1) and (m<resp_n[i]) then m:=resp_n[i];
         j:= maxim(resp_l[i]);
         if m<j then m:=j
        end
    end;

  procedure new_know(m:integer);
    var el:K_el; i:integer;
    begin
      el.ng:=m+1; el.known:= known_names;
      add_el(el, knowledge);
      for i:=1 to graph_size do
       if nghs[i]=1 then
        begin
         if (own_name in resp_l[i])then resp_l[i]:=resp_l[i]-[own_name];
         resp_l[i]:=resp_l[i]+[m+1];
         el.ng:=resp_n[i]; el.known:=resp_l[i];
         add_el(el, resp_k[i]);
        end;
    end;

  procedure init_node_var;
      var i,j:integer;
      begin
       known_names:=[]; own_name:=0; ngh_number:=0;
       for j:=1 to max do
        begin
         knowledge[j].ng:=max; knowledge[j].known:=[]
        end;
       for i:=1 to graph_size do
        begin
         if nghs[i] = 1 then ngh_number := ngh_number+1;
         resp_n[i]:=0; resp_l[i]:=[];        
         for j:=1 to max do
          begin
            resp_k[i][j].ng:=max; resp_k[i][j].known:=[]
          end
        end
      end;



{***************************************************************}
{
   Below are global random selection functions and 'graph_creation',
   i.e., those represented by #include"init_func0".

   The 'graph_creation' procedure creates the graph in form of a
   two-dimension and binary array, where (i, j) has value 1 iff nodes
   represented by i and j are in the graph relation. Each row i of
   the array defines i-th neighbourhood. The procedure defines a 
   random graph (of a given number of nodes) in that the binary value
   assigned to the pair (i, j) is randomly selected. In principle, 
   arbitrary connected graph can be created that way. If one wants to 
   obtain a particular graph, then it can be initialized by hand 
   replacing the 'graph_creation' call. For example, to create the 
   graph in Fig. 4.1. the following is the replacement (it is enough
   to make appropriate assignment of 1):
 
   graph[1,2]:=1; graph[1,6]:=1; 
   graph[2,1]:=1; graph[2,3]:=1;  
   graph[3,2]:=1; graph[3,4]:=1;  
   graph[4,3]:=1; graph[4,5]:=1; 
   graph[5,4]:=1; graph[5,6]:=1;
   graph[6,1]:=1; graph[6,5]:=1; 
}
{***************************************************************}

var
   r : real;
   u : integer;
   graph : graph_representation;

  procedure choice(m: integer; var j: integer);

  { This procedure draws a random integer in the interval <0, m>}

   begin
    u := (16807*u) mod 2147483647;
    j := u mod m
   end;

  procedure draw(p: real; var test: boolean);

  { This procedure draws TRUE or FALSE value with a probalility p}

   begin
    r := 16807*r-trunc(16807*r);
    if r<=p then test := true else test := false
   end;

  procedure graph_creation ( var g : graph_representation);

    { This procedure creates a representation of a graph that is}
    { connected, free of self-loops, and of size 'graph_size'}

    var i,j,k : integer; test: boolean;
    begin
     for i:=2 to graph_size do
       begin 
        choice(i-1, k); k:=k+1;
        for j:=1 to i-1 do
          begin
           draw(0.5, test);          
           if (j=k) or test then begin g[i,j]:=1; g[j,i]:=1 end
          end
       end
    end;

{***************************************************************}