diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index d2bafaa..e4a5aea 100644 --- a/.obsidian/workspace.json +++ b/.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", diff --git a/Concurrent Systems/notes/14.md b/Concurrent Systems/notes/14.md index 661d80e..e9f069c 100644 --- a/Concurrent Systems/notes/14.md +++ b/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}$$ diff --git a/Pasted image 20250429091029.png b/Pasted image 20250429091029.png new file mode 100644 index 0000000..8beab91 Binary files /dev/null and b/Pasted image 20250429091029.png differ