diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 0a3eee4..1eaeb12 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -240,6 +240,7 @@ }, "active": "84845736e00d5c98", "lastOpenFiles": [ + "Pasted image 20250414164549.png", "Concurrent Systems/slides/class 12.pdf", "Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md", "Concurrent Systems/notes/images/Pasted image 20250414082824.png", diff --git a/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md b/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md index b185ba3..6079b4b 100644 --- a/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md +++ b/Concurrent Systems/notes/12 - CCS (che non so cosa voglia dire).md @@ -91,48 +91,35 @@ Sure Marco! Let's go step-by-step through the **CCS process transition example** --- #### Example +![](../../Pasted%20image%2020250414164549.png) + +#### Example, but explained ##### 📘 Definitions - We start with the following **process definitions**: - - $A \triangleq a.A'$ - $A' \triangleq \bar{b}.A$ - $B \triangleq b.B'$ - $B' \triangleq \bar{c}.B$ Our **initial process** is: $A \mid B$ - ##### ▶️ Step 1: Transition from A From the definition: - $A \triangleq a.A'$ - - So we can do: $A \xrightarrow{a} A'$ (A consumes ) + - So we can do: $A \xrightarrow{a} A'$ (A consumes a and becomes A') Using the **parallel rule** for the left-hand side: +$$\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B}$$ +✅ **First transition:** $A \mid B \xrightarrow{a} A' \mid B$ -A→aA′A∣B→aA′∣B\frac{A \xrightarrow{a} A'}{A \mid B \xrightarrow{a} A' \mid B} - -✅ **First transition:** - -A∣B→aA′∣BA \mid B \xrightarrow{a} A' \mid B - ---- - -## ▶️ Step 2: Synchronization: bˉ\bar{b} and bb - +##### ▶️ Step 2: Synchronization: $\bar{b}$ and $b$ We now have: - -- Left process: A′≜bˉ.AA' \triangleq \bar{b}.A - -- Right process: B≜b.B′B \triangleq b.B' - +- Left process: $A' \triangleq \bar{b}.A$ +- Right process: $B \triangleq b.B'$ From this, we can do: - -- A′→bˉAA' \xrightarrow{\bar{b}} A - -- B→bB′B \xrightarrow{b} B' - +- $A' \xrightarrow{\bar{b}} A$ +- $B \xrightarrow{b} B'$ These actions **complement each other**, so we can apply the **synchronization rule**: diff --git a/Pasted image 20250414164549.png b/Pasted image 20250414164549.png new file mode 100644 index 0000000..07defb6 Binary files /dev/null and b/Pasted image 20250414164549.png differ