vault backup: 2025-04-29 09:13:47

.obsidian/workspace.json

@@ -215,6 +215,7 @@
   "lastOpenFiles": [
     "Concurrent Systems/slides/class 14.pdf",
     "Concurrent Systems/notes/14.md",
+    "Pasted image 20250429091029.png",
     "Pasted image 20250429085319.png",
     "Pasted image 20250429084950.png",
     "Pasted image 20250429084921.png",
@@ -226,7 +227,6 @@
     "Pasted image 20250429082812.png",
     "Concurrent Systems/notes/13 - Weak Bisimilarity.md",
     "Concurrent Systems/slides/class 13.pdf",
-    "Pasted image 20250428175449.png",
     "Concurrent Systems/notes/12 - Calculus of communicating system.md",
     "Concurrent Systems/slides/class 12.pdf",
     "Concurrent Systems/notes/12b - CCS cose varie.md",

Concurrent Systems/notes/14.md

@@ -36,4 +36,15 @@ replacing one by one every continuation with its standard form, obtaining standa
 ![](../../Pasted%20image%2020250429085319.png)
 
 ### Axioms & Rules for Weak Bisimilarity
+![](../../Pasted%20image%2020250429091029.png)
 
+#### Example
+A server for exchanging messages, in its minimal version, receives a request for sending messages and delivers the confirmation of the reception
+
+Specification: $$Spec \triangleq send.\overline{rcv}$$
+The behavior of such a server can be implemented by three processes in parallel:
+- one handles the button for sending
+- another one effectively sends the message (through the restricted action *put*) and waits for the signal of message reception (through the restricted action *go*)
+- the last one gives back to the user the outcome of the sending
+
+$$S \triangleq send.\overline{put} \quad M \triangleq send.\overline{put}$$