msgtransfer.service.ppy

# pseudo-Python module msgtransfer.service.ppy
# class Service is msgtransfer service (abstract version)

class Service():
  def __init__(self, num_nodes):
    """Throughout j ranges over 0..num_nodes-1:
    - ending is true iff end(j) has been called for some j.
    - ongoing_send[j] is true iff a send(j,.) call is ongoing.
    - closed_send[j] is true iff a send(j,.) call has returned False.
    - ongoing_recv[j] is true iff a recv(j) call is ongoing.
    - closed_recv[j] is true iff a recv(j) call has returned (False,).
    - sent[(j,k)] is the sequence of messages sent in send(j,k,.) calls.
    - nrcvd[(j,k)] is the number of messages received from j in recv(k) calls.
    """
    self.num_nodes = num_nodes
    self.ending = False
    self.ongoing_send = [False for k in range(num_nodes)]
    self.closed_send = [False for k in range(num_nodes)]
    self.ongoing_recv = [False for k in range(num_nodes)]
    self.closed_recv = [False for k in range(num_nodes)]
    self.sent = {(j,k) : []
                 for k in range(num_nodes)
                 for j in range(num_nodes) if k != j}
    self.nrcvd = {(j,k) : 0
                  for k in range(num_nodes)
                  for j in range(num_nodes) if k != j}


  def send(self, j, k, msg):
    CIC:
      0 <= j < self.num_nodes and 
      0 <= k < self.num_nodes and j != k and
      not self.ongoing_send[j] and not self.closed_send[j]
    CU:
      self.sent[(j,k)].append(msg)
      self.ongoing_send[j] = True

    RETURN(rval):
      ROC:
        rval == True or (rval == False and self.ending)
      RU:
        self.ongoing_send[j] = False
        if not rval:
          self.closed_send[j] = True
        return rval


  def recv(self, j):
    CIC:
       0 <= j < self.num_nodes and
       not self.ongoing_recv[j] and not self.closed_recv[j])
    CU:
      self.ongoing_recv[j] = True

    RETURN((flag, msg, k)):
      # rval is (False,) | (True, msg)
      # Note: parameter k is an "internal" parameter, not part of rval
      ROC:
        (flag == False and self.ending)  or
        (flag == True and self.nrcvd[(k,j)] < len(self.sent[(k,j)])
         and msg == self.sent[(k,j)][self.nrcvd[(k,j)]])
      RU:
        self.ongoing_recv[j] = False
        if flag == False:
          self.closed_recv[j] = True
          return (flag,)
        else:
          self.nrcvd[(k,j)] += 1
          return (flag, msg)


  def end(self, j):
    CIC:
       0 <= j < self.num_nodes and not self.ending
    CU:
      self.ending = True

    RETURN():
      ROC:
        True
      RU:
        pass