Atomic-vs-no-atomic

atomic-silly

role Pong:
    action Init:
        self.response = None

    atomic action ReceivePing:
        recv_msg = any network[self.ID]
        send_msg = "hi " + recv_msg.name

        # Cache the first response and then always send that
        if self.response == None:
            self.response = send_msg
              
        network[recv_msg.source].add(self.response)
        network[self.ID].remove(recv_msg)

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-output

Model checking /home/jack/tmp/nonatomic/nonatomic.json
configFileName: /home/jack/tmp/nonatomic/fizz.yaml
StateSpaceOptions: options:{max_concurrent_actions:2 crash_on_yield:false} deadlock_detection:false
Nodes: 32, queued: 17, elapsed: 12.861828ms
Time taken for model checking: 12.933343ms
Writen graph dotfile: /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/graph.dot
To generate svg, run:
dot -Tsvg /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/graph.dot -o graph.svg && open graph.svg
FAILED: Model checker failed. Invariant:  AllOk
------
Init
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = None, name = \"pinger-0\", received = None)), role Ping#1 (params(ID = 1),fields(expected = None, name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = None))"}
------
Ping#0.SendPing
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = \"hello pinger-0\", name = \"pinger-0\", received = None)), role Ping#1 (params(ID = 1),fields(expected = None, name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = None))"}
------
thread-0
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = \"hello pinger-0\", name = \"pinger-0\", received = None)), role Ping#1 (params(ID = 1),fields(expected = None, name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = \"hello pinger-0\"))"}
------
Ping#1.SendPing
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = \"hello pinger-0\", name = \"pinger-0\", received = None)), role Ping#1 (params(ID = 1),fields(expected = \"hello pinger-1\", name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = \"hello pinger-0\"))"}
------
thread-1
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = \"hello pinger-0\", name = \"pinger-0\", received = None)), role Ping#1 (params(ID = 1),fields(expected = \"hello pinger-1\", name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = \"hello pinger-1\"))"}
------
thread-0
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = \"hello pinger-0\", name = \"pinger-0\", received = None)), role Ping#1 (params(ID = 1),fields(expected = \"hello pinger-1\", name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = \"hello pinger-1\"))"}
------
thread-0
--
state: {"pingers":"[role Ping#0 (params(ID = 0),fields(expected = \"hello pinger-0\", name = \"pinger-0\", received = \"hello pinger-1\")), role Ping#1 (params(ID = 1),fields(expected = \"hello pinger-1\", name = \"pinger-1\", received = None))]","ponger":"role Pong#0 (fields(response = \"hello pinger-1\"))"}
------
Writen graph json: /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/error-graph.json
Writen graph dotfile: /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/error-graph.dot
To generate an image file, run:
dot -Tsvg /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/error-graph.dot -o error-graph.svg && open error-graph.svg
Writen error states as html: /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/error-states.html
To open:
open /home/jack/tmp/nonatomic/out/run_2024-12-06_15-56-53/error-states.html

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