Source code for msgtransfer2.imp_0.checker

# sesf module: msgtransfer2.imp_0.checker

import argparse

class Checker():
  """
  Maintain the global state of a distributed system of msgtransfer.imp0
  nodes and check some assertions. Created by msgtransfer2.servicetester
  when testing the distributed system. Maintains the following variables:

  - tester: the tester object that started this checker object
  - sent: sent state maintained by tester (actually tester.service) object
  - rcvd_counts: list of two integers initially both 0.
    rcvd_counts[j] is number of packets received at node j, for j in 0..1.

  Has a function ``handle_event(e)`` that takes an event ``e`` reported
  by a node, updates the global state, and checks whether an assertion
  still holds.

  - RPC-called by an node to report an event ``e`` at the node.
    ``e`` is a ``('checker','rcvd',j,msg)`` tuple, indicating the arrival
    at node j of packet whose data is ``msg`` serialized.

  - Assertion checked:
    for every event ('checker', 'rcvd', j, msg):
    sent[1-j][rcvd_counts[j]] == msg

 """

  def __init__(self, servicetester, argv):
    self.servicetester = servicetester
    parser = argparse.ArgumentParser()
    parser.add_argument("num_nodes", type=int, help="number of nodes")
    args = parser.parse_args(argv[1:])
    self.num_nodes = args.num_nodes
    self.sent = servicetester.serviceparts.sent
    self.rcvd_counts = [0, 0]


  def handle_event(self, event):
    """
    events: ('checker', ''rcvd', j, msg): msg recvd at node j
    """
    # print("handle_event called:", event, flush=True)   # DEBUG
    
    # import pdb; pdb.set_trace()
    event = event[2:]
    # event: (j, msg)
    j, msg = event
    # check msgtransfer2.imp_0.imp assertion
    if self.sent[1-j][self.rcvd_counts[j]] != msg:
      print("node", j, "recv event invalid", flush=True)
    else:
      print("node", j, "recv event valid", flush=True)
    self.rcvd_counts[j] += 1
    # currently nothing to check for 'linkup' and 'linkdown' events

###### END class Checker of module msgtransfer2.imp_0.checker ############