always assertion AllOk:
    for pinger in pingers:
        if pinger.received != None and pinger.received != pinger.expected:
            return False
    return True

role Ping:
    action Init:
        self.name = "pinger-" + str(self.ID)
        self.expected = None
        self.received = None

    atomic action SendPing:
        require self.expected == None

        msg = record(source = self.ID,
                     name = self.name)
        network[ponger.ID].add(msg)
        self.expected = "hello " + self.name

    atomic action ReceivePong:
        recv_msg = any network[self.ID]
        self.received = recv_msg

role Pong:
    atomic action ReceivePing:
        recv_msg = any network[self.ID]
        send_msg = "hello " + recv_msg.name
              
        network[recv_msg.source].add(send_msg)
        network[self.ID].remove(recv_msg)

action Init:
    network = {}
      
    pingers = bag()
    for id in range(2):
        pinger = Ping(ID=id)
        pingers.add(pinger)
        network[pinger.ID] = genericset()

    ponger = Pong(ID=100)
    network[ponger.ID] = genericset()