Pseudocode for node i:

Initialize:

for all nodes i do:
ST^i_j := passive for all j\in (N^i + {i})
ST^i_{jk} := passive for all k \in N^i and all j \in (N^i + {i})
SQ^i_j := 0 for all j \in (N^i + {i})
s^i_j = nil

all other fields are undefined!


Start:
source node j checks if ST^j_j = passive. If yes, then
  - send a message (the latest one) for source j to every k \in N^j
  - ST^j_j := active
  - s^j_j := j
  - ST^j_{jk} := active for all k \in N^j
  - SQ^i_j := SQ^i_j + 1


Terminate:
when node j receives acks from all k\in N^j

Algorithm for node i other than j:


Receive msg_m for source j from node p:

if p \in N^i
   if SQ^i_j = m 
      /* no condition on ST^i_j, i.e., 
      /* ST^i_j = passive or active or not defined
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      send ack_m to p for source j 

   if (SQ^i_j < m or SQ^i_j is not defined) 
      /* no condition on ST^i_j, i.e., 
      /* ST^i_j = passive or active or not defined
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      s^i_j := p
      SQ^i_j := m
      ST^i_{jp} := passive
      if i has at least one more neighbor other than p
         ST^i_j := active 
         ST^i_{jk} := active for all k\in N^i-{p}
         send message m for source j to all k\in N^i-{p}
      if N^i = {p} 
         ST^i_j := passive
         send ack_m for source j to p

   if ST^i_j = active and SQ^i_j > m 
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      ST^i_{jp} := active
      send message SQ^i_j for source j to p
   if ST^i_j = passive and SQ^i_j > m
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not 
      ST^i_j := active 
      s^i_j := i
      ST^i_{jp} := active
      send message SQ^i_j for source j to p

if not(p \in N^i)
   /* no conditions on any other attribute
   consume msg, no response



Receive ack_m for source j from node q:

if q \in N^i
   if SQ^i_j < m
      /* no condition on ST^i_j, i.e., 
      /* ST^i_j = passive or active or not defined
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      ack_{SQ^i_j} for source j to q


   if SQ^i_j = m and ST^i_j = passive
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      receive/consume the ack_m, do nothing else

   if SQ^i_j = m and ST^i_j = active and ST^i_{jq} is defined (either
                                                      passive or active)
      if s^i_j is defined 
         if ST^i_{jk} = passive or not defined 
                        for all k \in (N^i - (s^i_j + q))
            ST^i_j := passive
            ST^i_{jq} := passive
            if s^i_j # i
               send ack_m for source j to s^i_j

         if ST^i_{jk} = active for at least one k \in (N^i - (s^i_j + q))
            ST^i_{jq} := passive

      if s^i_j is undefined
      /* this case should not occur, nevertheless, the current Maude
      /* spec deals with it in the following way
         if ST^i_{jk} = passive or not defined 
                        for all k \in (N^i - q)
            ST^i_j := passive
            ST^i_{jq} := passive

         if ST^i_{jk} = active for at least one k \in (N^i - q)
            ST^i_{jq} := passive
   

   if SQ^i_j = m and ST^i_j is not defined
   /* this case should not occur, nevertheless, the current Maude
   /* spec deals with it in the following way
      consume ack, no response


   if SQ^i_j > m and ST^i_j = active 
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      ST^i_{jq} := active
      send message SQ^i_j for source j to q

   if SQ^i_j > m and ST^i_j = passive 
      /* no condition on s^i_j, i.e., might be defined or not
      /* no conditions on the status of neighbors ST^i_{jk},
      /* i.e., might be defined or not
      ST^i_j := active
      s^i_j := i
      ST^i_{jq} := active
      send message SQ^i_j for source j to q

  
   if SQ^i_j is not defined
      /* only condition: q is neighbor
      /* no condition on any other attribute
      N^i := N^i + q
      ST^i_j := passive
      SQ^i_j := 0
      ST^i_{jk} := passive for all k \in (N^i + q)
      ack_0 for source j to q



For new link (i,b):

For all nodes j for which i has a defined value SQ^i_j do:

if ST^i_j = active and SQ^i_j is defined
   /* no condition on s^i_j, i.e., might be defined or not
   /* no conditions on ST^i_{jk} 
   /* no conditions on N^i
   N^i := N^i + b
   ST^i_{jb} := active
   send message SQ^i_j for source j to b
   if ST^i_b is not defined 
      ST^i_b := passive 
   if SQ^i_b is not defined
      SQ^i_b := 0 /* the initialized state
   if ST^i_{bk} not defined
      ST^i_{bk} := passive for all k \in {N^i + b}
   
if ST^i_j = passive and SQ^i_j is defined
   N^i := N^i + b
   ST^i_j := active
   s^i_j := i
   ST^i_{jb} := active
   send message SQ^i_j for source j to b
   if ST^i_b is not defined 
      ST^i_b := passive 
   if SQ^i_b is not defined
      SQ^i_b := 0 /* the initialized state
   if ST^i_{bk} not defined
      ST^i_{bk} := passive for all k \in {N^i + b}
   



For failure of link (i,b):

For all nodes j for which i has a defined value SQ^i_j do:

if ST^i_j = active and s^i_j is defined
   /* no conditions on ST^i_{jk} 
   /* no conditions on N^i
   if ST^i_{jk} = passive or not defined 
                  for all k \in (N^i - s^i_j) , k # b
      N^i := N^i - b 
      ST^i_j := passive
      if s^i_j = b then delete it from parent-set
      if ST^i_{jb} is defined then delete if from neighbor-status-set
      if s^i_j # i
         ack_m for source j to s^i_j

   if ST^i_{jk} = active for at least one  k \in (N^i - s^i_j) , k # b
      N^i := N^i - b 
      if s^i_j = b then delete it from parent-set
      if ST^i_{jb} is defined then delete if from neighbor-status-set


   if ST^i_j = active and s^i_j is not defined
   /* this case should not occur, nevertheless the current Maude
   /* spec deals with it in the following way
      consume linkDown, no response   


if ST^i_j = passive 
   /* no condition on s^i_j, i.e., might be defined or not
   /* no conditions on ST^i_{jk} 
   /* no conditions on N^i
   /* no condition on SQ^i_j
   N^i := N^i - b 
   if s^i_j = b then delete it from parent-set
   if ST^i_{jb} is defined then delete if from neighbor-status-set

if ST^i_j is not defined
   /* no condition on s^i_j
   /* no condition on N^i
   /* no condition on ST^i_jk
   /* all theses attributes can be defined or not
   N^i := N^i - b 
   if s^i_j = b then delete it from parent-set
   if ST^i_{jb} is defined then delete if from neighbor-status-set