{
 This is a specification of an enumeration algorithm in which  
 a random number is generated independently in each node and then
 broadcast to all other nodes. Nodes store, in 'known', an arriving 
 number and forward it if it has not been received yet; otherwise the  
 number is discarded. Once the random numbers from all network nodes
 were collected in a node (stored in the array 'known'), they are
 sorted. If all numbers are different, then the algorithm terminates
 (variable 'done' is 'true' in all nodes) and the index of a node's 
 random number in the array 'known' is taken as the node name, 
 ie., my_name=i, where known[i]=my_number. If, however,
 there are nodes with equal random numbers drawn (the variable 'done'
 remains 'false' in such nodes), then the second drawing round is 
 performed, but concerning only those nodes. Drawing rounds are 
 repeated unless  all drawn numbers in the last round are different. 
 Thus, the whole algorithm always properly terminates, since the 
 probability of drawing equal numbers in consecutive n rounds is 
 converging to 0 with n growing to infinity. 
 
 In this algorithm it is assumed that each node has an unique network
 address. A node has to broadcast, together with the random number 
 selected, this unique address and the drawing attempt number (round
 number) to properly synchronize node's performance which otherwise
 is completely independent and asynchronous. Nothing, except the size 
 of the network, needs to be known to a node.
 The network (connected) graph of size 'graph_size' constant 
 is randomly created by the 'graph_creation' procedure.
}
specification graph_enumeration systemactivity;
 default common queue;
 const
   graph_size = 5;

type
   zero_one = 0..1;
   V = 1..graph_size;
   element = array[1..3] of integer; 
   {A[1]-node address; A[2]-node drawing attempt, A[3]-node random}
   neighbour_representation = array[V] of zero_one;
   graph_representation = array[V] of neighbour_representation;
   knowledge = array[V] of element;
   control = array[V] of char;

 channel link(R1,R2);
  by R1,R2: new(ele: element); 
   
 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;
 
  var
   my_name, mu, left, right, myad, 
   my_random, attempt, my_pointer: integer;
   done, new_round: boolean;
   nghs: neighbour_representation;
   known: knowledge;
   ctrl: control;
   el: element;

  procedure choice(var u: integer);
    { this procedure draws a random integer u in the interval 
      between 1 and 2147483647 +1 }
    begin u := ((16807*u) mod 2147483647)+1 end;

  function is_el(x:element; k:integer; A:knowledge):boolean;
    { this function responds 'true' if x=A[j], for some j<=k }
#include "f.is_el"

  procedure process_new_random;
    { this is the main processing procedure of the node; 
      provided a new element was received (or created by the 
      node itself), then it is appropriately placed in  
      'known' by 'find_replace'; then it is checked whether 
      the interval of 'known' between 'left' and 'right' 
      has already all results of the current round ('is_full');
      the interval contained equal random numbers 
      in the previous round (or 0's initially with 'left'=1 
      and 'right'=graph_size); if yes then elements are 
      sorted by 'sort' and control array 'ctrl' is adjusted by 
      'adjust-control'; then a test is made whether the node 
      ended current round and if so whether or not it is going 
      to participate (actively) in the next one; if yes, then 
      '(not done) and (new_round)' conditions are still valid }
#include "p.process_new_random"       

 initialize  
    var j: integer; 
    begin 
      myad:=nad; mu:=myad*377003616; nghs:=ngh;
      ctrl[1]:= '(' ; ctrl[graph_size]:= ')' ;
      for j:=2 to graph_size-1 do ctrl[j]:= '-';
      new_round:=true; attempt:=1;
    end;

  trans
    provided (not done) and (new_round)
         begin
           choice(mu); my_random:=mu; new_round:=false;
           el[1]:=myad; el[2]:=attempt; el[3]:=my_random;
           process_new_random;
           all i:V do
           if nghs[i]=1 then
             output s_neighbour[i].new(el)
         end;

  trans
      any i:V do
      when r_neighbour[i].new(ele)
       provided ele[2]=attempt
         begin
           el:=ele;
           if (not is_el(el, graph_size, known)) then
            begin
             process_new_random;
             all i:V do
             if nghs[i]=1 then
              output s_neighbour[i].new(el)
            end
         end;

       provided ele[2]<attempt
         begin end;
           
 end; {node_body}

#include "init_func"

 modvar 
  nodes: array[V] of node;

initialize
  var i,j:integer; 
  begin
    r := 0.175555987; u := 377003616;
    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}