Atomic-vs-no-atomic

atomic.fizz

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()

nonatomic.fizz

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

   action DoPing:
       require self.expected == None

       self.expected = "hello " + self.name
       result = ponger.ProcessPing(self.name)
       self.received = result

role Pong:
   func ProcessPing(name):
       response = "hello " + name
       return response

action Init:
   pingers = bag()
   for id in range(2):
       pinger = Ping(ID=id)
       pingers.add(pinger)

   ponger = Pong()

silly-nonatomic.fizz

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

    action DoPing:
        require self.expected == None

        self.expected = "hello " + self.name
        result = ponger.ProcessPing(self.name)
        self.received = result

role Pong:
    action Init:
        self.response = None
        
    func ProcessPing(name):
        self.response = "hello " + name
        return self.response

action Init:
    pingers = bag()
    for id in range(2):
        pinger = Ping(ID=id)
        pingers.add(pinger)

   ponger = Pong()