Vanlightly · December 6, 2024 16:06 · Dec 6, 2024 · Dec 6, 2024 · Dec 6, 2024
diff --git a/atomic-silly b/atomic-silly
@@ -0,0 +1,14 @@
+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)
diff --git a/nonatomic-output b/nonatomic-output
@@ -0,0 +1,45 @@
+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
diff --git a/atomic.fizz b/atomic.fizz
@@ -0,0 +1,43 @@
+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()
diff --git a/nonatomic.fizz b/nonatomic.fizz
@@ -0,0 +1,32 @@
+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()
diff --git a/silly-nonatomic.fizz b/silly-nonatomic.fizz
@@ -0,0 +1,35 @@
+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()