msgtransfer2.service.ppyΒΆ

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

class Service():
  def __init__(self):
    """Throughout j ranges over 0..1:
    - ending is true iff end(0) or end(1) has been called.
    - ongoing_send[j] is true iff a send(j,.) call is ongoing. j in 0..1
    - 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] is the sequence of messages sent in send(j,.) calls.
    - nrcvd[j] is the number of messages returned in recv(j) calls.
    """
    self.ending = False
    self.ongoing_send = [False, False]
    self.closed_send = [False, False]
    self.ongoing_recv = [False, False]
    self.closed_recv = [False, False]
    self.sent = [[], []]
    self.nrcvd = [0, 0]


  def send(self, j, msg):
    CIC:
      j in (0, 1) and                                       # call part
      not self.ongoing_send[j] and not self.closed_send[j]  #  "  "  "
    CU:                                                     #  "  "  "
      self.sent[j].append(msg)                              #  "  "  "
      self.ongoing_send[j] = True                           #  "  "  "

    RETURN(rval):                                           # return part
      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:
      (j in (0, 1) and
       not self.ongoing_recv[j] and not self.closed_recv[j])
    CU:
      self.ongoing_recv[j] = True

    RETURN((flag, msg)):
      # rval is (False,) | (True, msg)
      ROC:
       ((flag == False and self.ending) or
        (flag == True and self.nrcvd[j] < len(self.sent[1-j])
         and msg == self.sent[1-j][self.nrcvd[j]]))
      RU:
        self.ongoing_recv[j] = False
        if flag == False:
          self.closed_recv[j] = True
          return (flag,)
        else:
          self.nrcvd[j] += 1
        return (flag, msg)


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

    RETURN():
      ROC:
        True
      RU:
        pass